Email Gateway (Aug 22 2022 at 16:34): Email Gateway (Aug 22 2022 at 16:34):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a nice new AFP entry by Anders Schlichtkrull, Jasmin
Christian Blanchette, Dmitriy Traytel and Uwe Waldmann.
Enjoy,
René
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
This Isabelle/HOL formalization covers Sections 2 to 4 of Bachmair and
Ganzinger's "Resolution Theorem Proving" chapter in the Handbook of Automated
Reasoning. This includes soundness and completeness of unordered and ordered
variants of ground resolution with and without literal selection, the standard
redundancy criterion, a general framework for refutational theorem proving,
and soundness and completeness of an abstract first-order prover.
Email Gateway (Aug 22 2022 at 16:35):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi all,
Thanks, René, for this announcement. I'd like to use this opportunity to mention the existence of the corresponding paper draft, which we intend to submit to IJCAR next week:
http://matryoshka.gforge.inria.fr/pubs/rp_paper.pdf
Feedback is of course welcome. The PDF will be updated regularly. Be aware, though, that the target audience is one that is generally more familiar with resolution than with Isabelle.
Cheers,
Jasmin
Last updated: Apr 20 2024 at 01:05 UTC