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 . However, Isabelle was never designed for that purpose and is unlikely to be a good match for your requirements.
Best regards Tobias Nipkow 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
Description: S/MIME Cryptographic Signature