Lemma Learning in the Model Evolution Calculus

DOI10.1007/11916277_39MaRDI QIDQ5387921zbMATH OpenOpenAlexFDO

Authors Peter Baumgartner, Alexander Fuchs, Cesare Tinelli

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)

Recommendations

• The model evolution calculus as a first-order DPLL method
• The model evolution calculus.
• Model evolution with equality -- revised and implemented
• Automated Deduction – CADE-20
• A combined superposition and model evolution calculus

Cited in

(23)

• SCL(EQ): SCL for first-order logic with equality
• SCL(EQ): SCL for first-order logic with equality
• Using membrane calculus to describe DPLL algorithm with clause learning
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Automated Deduction – CADE-20
• Semantically-guided goal-sensitive reasoning: model representation
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Deciding effectively propositional logic using DPLL and substitution sets
• Computing finite models by reduction to function-free clause logic
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Exploring partial models with SCL
• SCL clause learning from simple models
• Lemma Learning in SMT on Linear Constraints
• On First-Order Model-Based Reasoning
• The model evolution calculus.
• Automated reasoning building blocks
• Model evolution with equality -- revised and implemented
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• Analysis of graph transformation systems: native vs translation-based techniques
• The model evolution calculus as a first-order DPLL method
• Model Evolution with Equality Modulo Built-in Theories
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets

Describes a project that uses

Uses Software

• Mace4
• E-Darvin
• Darwin

This page was built for publication: Lemma Learning in the Model Evolution Calculus

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