Re: [isabelle] Proof checking in Isabelle



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

On 24/10/2019 09:45, Geneau De Lamarliere Paul wrote:
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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.