Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] auto-proofs for \forall qualified formulas


view this post on Zulip 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!

lyj238@ios.ac.cn

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 08:18 UTC