Combining Instance Generation and Resolution

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

Mathematics Subject Classification ID

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

• TPTP
• Yices
• z3
• iProver

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