[Matryoshka-devel] Paper draft - Formalization of first-order resolution

Anders Schlichtkrull andschl at dtu.dk
Wed Mar 22 13:46:00 CET 2017

Hi all

I am writing a paper about my formalization in Isabelle/HOL of resolution for first-order logic. It contains formalizations of soundness and completeness using the substitution lemma, semantic trees, Herbrand’s theorem, and the lifting lemma.


It extends my paper from ITP2016. I will submit it to the special issue of Journal of Automated Reasoning on milestones in interactive theorem proving.


Comments are welcome. My plan is to make the last adjustments before I submit on next Wednesday (29 March 2017).


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170322/a0103b18/attachment.html>

More information about the matryoshka-devel mailing list