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.
Original language | English |
---|---|
Book series | Archive of Formal Proofs |
Pages (from-to) | 1-60 |
ISSN | 2150-914X |
Publication status | Published - 2018 |