Email Gateway (Aug 22 2022 at 20:48): Email Gateway (Aug 22 2022 at 20:48):From: Geneau De Lamarliere Paul <paul.geneau-de-lamarliere@ens-lyon.fr>
Dear Isabelle users,
My teammates and I are working on a software which generates proofs of a
given first order logic formula (within axioms and language definition).
Dear Isabelle users,
We would like to know whether it is possible to check resolution proofs
in FOL in Isabelle and which formats are supported.
Any feedback will be welcomed.
Sincerely,
Paul Geneau de Lamarliere
ENS de Lyon
Email Gateway (Aug 22 2022 at 20:49):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Team,
You can program your own proof checker using Isabelle's ML infrastructure which
includes higher-order resolution, and there is even a proof term format [1].
However, Isabelle was never designed for that purpose and is unlikely to be a
good match for your requirements.
Best regards
Tobias Nipkow
[1] Stefan Berghofer, Tobias Nipkow. Proof terms for simply typed higher order
logic. In Theorem Proving in Higher Order Logics (TPHOLs 2000), LNCS 1869, 2000.
http://www21.in.tum.de/~nipkow/pubs/tphols00.html
smime.p7s
Last updated: Apr 19 2024 at 01:05 UTC