Abstract
Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. In this formalization, we restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects. We relied on the IsaFoR library for first-order terms and on the Isabelle saturation framework. A paper describing this formalization was published at the 15th International Conference on Interactive Theorem Proving (ITP 2024).
License
Topics
Related publications
- Desharnais, M., Toth, B., Waldmann, U., Blanchette, J., & Tourret, S. (2024). A Modular Formalization of Superposition in Isabelle/HOL. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.ITP.2024.12
Session Superposition_Calculus
- Transitive_Closure_Extra
- Abstract_Rewriting_Extra
- Term_Rewrite_System
- Ground_Critical_Pairs
- Multiset_Extra
- Uprod_Extra
- HOL_Extra
- Relation_Extra
- Clausal_Calculus_Extra
- Ground_Term_Extra
- Ground_Ctxt_Extra
- Ground_Clause
- Selection_Function
- Term_Ordering_Lifting
- Ground_Ordering
- Ground_Type_System
- Ground_Superposition
- Ground_Superposition_Completeness
- Variable_Substitution
- First_Order_Clause
- Fun_Extra
- First_Order_Type_System
- First_Order_Select
- First_Order_Ordering
- First_Order_Superposition
- Grounded_First_Order_Superposition
- First_Order_Superposition_Completeness
- IsaFoR_Term_Copy
- First_Order_Superposition_Example
- First_Order_Superposition_Soundness
- Ground_Superposition_Soundness
- Ground_Superposition_Welltypedness_Preservation
Depends on
- Abstract Substitution
- A Formalization of Knuth–Bendix Orders
- Minimal, Maximal, Least, and Greatest Elements w.r.t. Restricted Ordering
- Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover
- Regular Tree Relations
- A Comprehensive Framework for Saturation Theorem Proving
- Extensions to the Comprehensive Framework for Saturation Theorem Proving