Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A Verified Functional Implemen...

view this post on Zulip Email Gateway (Aug 22 2022 at 18:48):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

there is now a verified first-order automated theorem prover in the AFP, cf.

https://www.isa-afp.org/entries/Functional_Ordered_Resolution_Prover.html

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

Abstract:
This Isabelle/HOL formalization refines the abstract ordered resolution prover presented
in Section 4.3 of Bachmair and Ganzinger's "Resolution Theorem Proving" chapter in the
Handbook of Automated Reasoning. The result is a functional implementation of a first-order
prover.

Thanks to Anders, Jasmin and Dmitriy,
René

Last updated: Apr 25 2024 at 20:15 UTC