Implementing Superposition in iProver (System Description)
From MaRDI portal
Publication:5049017
DOI10.1007/978-3-030-51054-1_24OpenAlexW3038142530MaRDI QIDQ5049017
André Duarte, Konstantin Korovin
Publication date: 9 November 2022
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_24
Related Items (10)
Heterogeneous heuristic optimisation and scheduling for first-order theorem proving ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ A comprehensive framework for saturation theorem proving ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Ground joinability and connectedness in the superposition calculus
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On using ground joinable equations in equational theorem proving
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- An abstraction-refinement framework for reasoning with large theories
- System Description: E 1.8
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- System Description: Spass Version 3.0
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- Theory and Applications of Satisfiability Testing
- A comprehensive framework for saturation theorem proving
This page was built for publication: Implementing Superposition in iProver (System Description)
