Implementing Superposition in iProver (System Description)

DOI10.1007/978-3-030-51054-1_24MaRDI QIDQ5049017zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A superposition oriented theorem prover
• scientific article; zbMATH DE number 4029349
• Theoretical Aspects of Computing – ICTAC 2005
• Combining superposition and induction: a practical realization
• Superposition for full higher-order logic
• Superposition for higher-order logic
• Superposition: composition vs refinement of non-deterministic, action-based systems
• Superposition: Composition vs refinement of non-deterministic, action-based systems
• SAT-Inspired Eliminations for Superposition

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1552512 (Why is no real title available?)
• A comprehensive framework for saturation theorem proving
• An abstraction-refinement framework for reasoning with large theories
• Handbook of automated reasoning. In 2 vols
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• On using ground joinable equations in equational theorem proving
• Ordered rewriting and confluence
• Paramodulation-based theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Simultaneous paramodulation
• System Description: Spass Version 3.0
• System description: E 1.8
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Theory and Applications of Satisfiability Testing
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(17)

• A posthumous contribution by Larry Wos: excerpts from an unpublished column
• Larry Wos: visions of automated reasoning
• Set of support, demodulation, paramodulation: a historical perspective
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• AC simplifications and closure redundancies in the superposition calculus
• scientific article; zbMATH DE number 4029349 (Why is no real title available?)
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• A comprehensive framework for saturation theorem proving
• Verified Given Clause Procedures
• Graph sequence learning for premise selection
• Ground joinability and connectedness in the superposition calculus
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• ALASCA: reasoning in quantified linear arithmetic
• Formula normalizations in verification
• \texttt{gym-saturation}: gymnasium environments for saturation provers (system description)
• Resolution calculi for non-normal modal logics

Describes a project that uses

Uses Software

• DISCOUNT
• E Theorem Prover
• iProver
• TPTP
• SPASS
• VAMPIRE
• OTTER
• MiniSat

This page was built for publication: Implementing Superposition in iProver (System Description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5049017)