[isabelle] Proof checking in Isabelle



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


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