Combining instance generation and resolution

DOI10.1007/978-3-642-04222-5_19MaRDI QIDQ3655208zbMATH OpenOpenAlexWikidataFDO

Authors Christopher Lynch, Ralph Eric McGregor

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

Mechanization of proofs and logical operations (03B35)

Recommendations

• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Partial instantiation methods for inference in first-order logic
• New methods for computing inferences in first order logic
• scientific article; zbMATH DE number 3871320

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Encoding First Order Proofs in SAT
• scientific article; zbMATH DE number 5305114 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• scientific article; zbMATH DE number 1903355 (Why is no real title available?)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Logic-based decision support. Mixed integer model formulation
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• Partial instantiation methods for inference in first-order logic
• Resolution theorem proving
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• The model evolution calculus as a first-order DPLL method
• The TPTP problem library. CNF release v1. 2. 1

Cited in

(5)

• New methods for computing inferences in first order logic
• SMELS: satisfiability modulo equality with lazy superposition
• A combined superposition and model evolution calculus
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Comparing instance generation methods for automated reasoning

Describes a project that uses

Uses Software

• TPTP
• Yices
• z3
• iProver

This page was built for publication: Combining instance generation and resolution

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