Predicate Elimination for Preprocessing in First-Order Theorem Proving
From MaRDI portal
Publication:2818027
DOI10.1007/978-3-319-40970-2_22zbMath1475.68441MaRDI QIDQ2818027
Konstantin Korovin, Zurab Khasidashvili
Publication date: 5 September 2016
Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-40970-2_22
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
SAT-Inspired Eliminations for Superposition, SAT-Inspired Higher-Order Eliminations, Set-blocked clause and extended set-blocked clause in first-order logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The Ackermann approach for modal logic, correspondence theory and second-order reduction
- Refutational theorem proving for hierarchic first-order theories
- Untersuchungen über das Eliminationsproblem der mathematischen Logik
- System Description: E 1.8
- Inprocessing Rules
- The TPTP World – Infrastructure for Automated Reasoning
- Counterexample-guided abstraction refinement for symbolic model checking
- Solving SAT and SAT Modulo Theories
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Efficient E-Matching for SMT Solvers
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- Interpolation and Symbol Elimination
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- A Computing Procedure for Quantification Theory
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Interpolation and Symbol Elimination in Vampire
- Combining Abstraction Refinement and SAT-Based Model Checking
