### Abstract

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.

### License

BSD License

### Topics

- Logic/General logic/Mechanization of proofs

### Session Ordered_Resolution_Prover

- Map2
- Lazy_List_Liminf
- Lazy_List_Chain
- Clausal_Logic
- Herbrand_Interpretation
- Abstract_Substitution
- Inference_System
- Ground_Resolution_Model
- Unordered_Ground_Resolution
- Ordered_Ground_Resolution
- Proving_Process
- Standard_Redundancy
- FO_Ordered_Resolution
- FO_Ordered_Resolution_Prover

### Depends on

- Coinductive
- Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

### Used by

- A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic
- Extensions to the Comprehensive Framework for Saturation Theorem Proving
- A Formal Proof of The Chandy–Lamport Distributed Snapshot Algorithm
- A Comprehensive Framework for Saturation Theorem Proving
- A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover

### Auto-related entries

- A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover

## Cite

×

Ordered_Resolution_Prover-AFP

    @article{Ordered_Resolution_Prover-AFP,
      author  = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel and Uwe Waldmann},
      title   = {Formalization of Bachmair and Ganzinger's Ordered Resolution Prover},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Ordered_Resolution_Prover.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Jan 22, 2018 : Isabelle2017