[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.

https://people.compute.dtu.dk/andschl/resolution_jar_draft.pdf

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.

http://www.cse.unsw.edu.au/~kleing/JAR-milestone/index.html

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

Cheers,
Anders


-------------- 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