[isabelle] New in the AFP: A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover



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é




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.