I am trying to do a forward proof using  hypothetical syllogism
of this form:     ~q v r, q |- r
but get an alpha-conversion error.
(sorry for the hard to read format here, but I know I can't post images or
pdf files here, so what other way is there to show the extended chars of
ProofPower?  I did
ascii-conv to get this format)

 val L1 = p %thm% p: THM
 val L2 = p %implies% q %thm% p %implies% q: THM
 val L3 = p %implies% q, p %thm% q: THM
 val L4 = %not% q %or% r %thm% %not% q %or% r: THM

 Exception Fail * ³ q ² r ô ³ q ² r and p ´ q, p ô q are not of the form:
`‡1 ô
 t1 ² t2' and `‡2 ô ³t3' where ¬t3® is Á-convertible to ¬t1® or ¬t2®
 [²_cancel_rule.7050] * raised
Proofpower mailing list

Reply via email to