Lemma Learning in the Model Evolution Calculus

DOI10.1007/11916277_39zbMath1165.03308OpenAlexW2118601609MaRDI QIDQ5387921

Peter Baumgartner, Cesare Tinelli, Alexander Fuchs

Publication date: 27 May 2008

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11916277_39

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Semantically-guided goal-sensitive reasoning: model representation ⋮ Automated Reasoning Building Blocks ⋮ The model evolution calculus as a first-order DPLL method ⋮ On First-Order Model-Based Reasoning ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Unnamed Item ⋮ Deciding Effectively Propositional Logic Using DPLL and Substitution Sets ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Deciding effectively propositional logic using DPLL and substitution sets ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Computing finite models by reduction to function-free clause logic ⋮ SCL clause learning from simple models ⋮ SCL(EQ): SCL for first-order logic with equality

Uses Software

• Darwin
• E-Darvin
• Mace4