I am trying to prove a goal P knowing:
a implies P ; b implies P ; c implies P ; a \/ b \/ c
Each term a, b and c are of the form u /\ v.
The conclusion P is of the form u /\ (x \/ y \/ z ...).
But this should not matter for the proof.
With small formulae, auto or force work. But otherwise they both never
Does anyone know what I should use instead of "auto" or "force" to solve
this kind of goal ?
I tried safe but it is not better.
Thanks a lot,
Julien Schmaltz Saarland University
Computer Science Department Institute for Computer Architecture
Phone: +49 (0)681 302 2419 Fax: +49 (0)681 302 4290
Email: julien at cs.uni-sb.de WWW: http://www-wjp.cs.uni-sb.de/
This archive was generated by a fusion of
Pipermail (Mailman edition) and