I don't quite understand what you are trying to do here.
On the face of it you want a rule:

------ false-intro

But this is not possible, because it is not sound.

As far as I can see Woodcock does not have a false-intro rule,
he has only a false-elim rule, is that what you want to reproduce?
Woodcock, so far as I can see, introduces false by using ¬-elim.

Could you clarify what you are looking for?


On 14/08/2016 01:21, David Topham wrote:
Roger (or Rob), I have been studying "UsingZ" by Jim Woodcock and JIm Davies. They use the "sequent" method and show a proof that derives "false". In looking through the inference rules in USR029 I don't see a rule that matches "false-intro". Can you suggest how to approach this type of proof (it is for my Discrete Match course). -Dave
i.e. What rule would I replace  ??? with for L6


Proofpower mailing list

Reply via email to