The model evolution calculus.

DOI10.1007/B11829MaRDI QIDQ5900727zbMATH OpenOpenAlexFDO

Authors Peter Baumgartner, Cesare Tinelli

Publication date 20 April 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Recommendations

• The model evolution calculus as a first-order DPLL method
• scientific article; zbMATH DE number 1614697
• A model-constructing satisfiability calculus
• Lemma Learning in the Model Evolution Calculus
• scientific article; zbMATH DE number 1931669

Cited in

(26)

• Computing finite models by reduction to function-free clause logic
• First order Stålmarck. Universal lemmas through branch merges
• Eliminating models during model elimination
• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
• The model evolution calculus as a first-order DPLL method
• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• A model-constructing satisfiability calculus
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Model evolution with equality -- revised and implemented
• Model evolution and refinement
• A combined superposition and model evolution calculus
• MACE4 and SEM: a comparison of finite model generators
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• The Relative Power of Semantics and Unification
• First-order resolution methods for modal logics
• Superposition and Model Evolution Combined
• Decidability Results for Saturation-Based Model Building
• Model Evolution with Equality Modulo Built-in Theories
• System description: SPASS-FD
• Lemma Learning in the Model Evolution Calculus
• An algorithm for approximating the satisfiability problem of high-level conditions
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• Comparing instance generation methods for automated reasoning
• The disconnection tableau calculus
• Deciding effectively propositional logic using DPLL and substitution sets

This page was built for publication: The model evolution calculus.

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