Combining Instance Generation and Resolution
From MaRDI portal
Publication:3655208
DOI10.1007/978-3-642-04222-5_19zbMath1193.03028OpenAlexW1517563066WikidataQ118190433 ScholiaQ118190433MaRDI QIDQ3655208
Ralph Eric McGregor, Christopher Lynch
Publication date: 7 January 2010
Published in: Frontiers of Combining Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-04222-5_19
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
A combined superposition and model evolution calculus ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ SMELS: satisfiability modulo equality with lazy superposition
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Logic-based decision support. Mixed integer model formulation
- The TPTP problem library. CNF release v1. 2. 1
- Partial instantiation methods for inference in first-order logic
- The model evolution calculus as a first-order DPLL method
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Encoding First Order Proofs in SAT
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- Automatic Theorem Proving With Renamable and Semantic Resolution
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
This page was built for publication: Combining Instance Generation and Resolution
