[Matryoshka-devel] Paper draft - Formalization of first-order resolution
andschl at dtu.dk
Wed Mar 22 13:46:00 CET 2017
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...
More information about the matryoshka-devel