Implementing Superposition in iProver (System Description)
From MaRDI portal
Publication:5049017
DOI10.1007/978-3-030-51054-1_24OpenAlexW3038142530MaRDI QIDQ5049017FDOQ5049017
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
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
- Theory and Applications of Satisfiability Testing
- System description: E 1.8
- Title not available (Why is that?)
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Paramodulation-based theorem proving
- Title not available (Why is that?)
- Handbook of automated reasoning. In 2 vols
- System Description: Spass Version 3.0
- Ordered rewriting and confluence
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- On using ground joinable equations in equational theorem proving
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- An abstraction-refinement framework for reasoning with large theories
- A comprehensive framework for saturation theorem proving
- Simultaneous paramodulation
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
- Title not available (Why is that?)
- 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
Uses Software
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)
