Email Gateway (Aug 18 2022 at 11:40): Email Gateway (Aug 18 2022 at 11:40):From: Tom Ridge <tjr22@cam.ac.uk>
Dear All,
I am trying to prove the following trivial first order theorem:
lemma "[|
ALL x y z.
(X x | Y x | Z x | W x) &
(X y | Y y | Z y | W y) & (X z | Y z | Z z | W z) -->
R x y & R y z --> R x z;
R x y;
R y z;
X x; X y; X z |]
==> R x z"
(* apply(metis) *)
apply(blast)
done
It works fine. But if I change blast to metis, the proof fails. Why?
Thanks
Tom
Email Gateway (Aug 18 2022 at 11:41):From: Lawrence Paulson <lp15@cam.ac.uk>
During the conversion to clause form, the first assumption is ignored
because it would yield 64 clauses.
Larry
Email Gateway (Aug 18 2022 at 11:41):From: Lawrence Paulson <lp15@cam.ac.uk>
Obviously HOL has different code for translating into clause form.
Larry
Email Gateway (Aug 18 2022 at 11:41):From: Lawrence Paulson <lp15@cam.ac.uk>
It would be easy to make this limit a parameter that the user could
set. To the best of my knowledge, this is an issue only with
artificial problems.
Larry
Last updated: May 03 2024 at 08:18 UTC