Email Gateway (Aug 22 2022 at 11:09): Email Gateway (Aug 22 2022 at 11:09):From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:
I have tried to use Isablle to prove some lemmas involving some \forall qualified formulas.
I use the seldgehammer to find the corresponding proof, but fails.
In my opinion, proofs for lemmas involving \exist (or \not \forll) needs the human hints to finish the proof, but for \forall
formulas should be automated by Isabelle.
Here I want to get a general suggestion from an expert who meet a similar question.
regards!
Email Gateway (Aug 22 2022 at 11:09):From: Lawrence Paulson <lp15@cam.ac.uk>
We are always trying to improve the level of automation in Isabelle. However, universally quantified formulas include many undecidable statements.
Larry Paulson
Email Gateway (Aug 22 2022 at 11:09):From: Buday Gergely <gbuday@karolyrobert.hu>
Dear lyj238,
Isabelle might not be the best automated theorem prover out there. Its strength is in interactive theorem proving.
For universally quantified formulas, use the fix-assume-show pattern, on page 27 of the Isabelle/Isar reference manual you will find an example:
https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/isar-ref.pdf#page=38
Cheers
Email Gateway (Aug 22 2022 at 11:10):From: Makarius <makarius@sketis.net>
Isabelle is actually a comined ITP + ATP environment, with lots of
automated tools included.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC