The model evolution calculus as a first-order DPLL method

DOI10.1016/j.artint.2007.09.005zbMath1182.03034OpenAlexW2141010048MaRDI QIDQ2389629

Cesare Tinelli, Peter Baumgartner

Publication date: 17 July 2009

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.artint.2007.09.005

zbMATH Keywords

first-order logicsequent calculimodel generationDPLL procedure

Mathematics Subject Classification ID

Related Items (19)

Semantically-guided goal-sensitive reasoning: model representation ⋮ History and Prospects for First-Order Automated Deduction ⋮ On First-Order Model-Based Reasoning ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Model evolution with equality -- revised and implemented ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ SMELS: Satisfiability Modulo Equality with Lazy Superposition ⋮ Deciding Effectively Propositional Logic Using DPLL and Substitution Sets ⋮ The Relative Power of Semantics and Unification ⋮ Deciding effectively propositional logic using DPLL and substitution sets ⋮ A sound and complete model-generation procedure for consistent and confidentiality-preserving databases ⋮ A Slice-Based Decision Procedure for Type-Based Partial Orders ⋮ Labelled splitting ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ Combining Instance Generation and Resolution ⋮ First order Stålmarck. Universal lemmas through branch merges ⋮ SGGS decision procedures ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ SMELS: satisfiability modulo equality with lazy superposition

Uses Software

• VAMPIRE
• SPASS
• TPTP
• Darwin
• SATCHMO
• Chaff
• BerkMin
• E Theorem Prover
• Denali

Cites Work

• Eliminating dublication with the hyper-linking strategy
• Properties of substitutions and unifications
• The TPTP problem library. CNF release v1. 2. 1
• Controlled integration of the cut rule into connection tableau calculi
• Depth-first proof search without backtracking for free-variable clausal tableaux
• Ordered semantic hyper-linking
• Partial instantiation methods for inference in first-order logic
• Ordered semantic hyper tableaux
• Automated deduction -- CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22--27, 2005. Proceedings.
• BerkMin: A fast and robust SAT-solver
• Proof and Model Generation with Disconnection Tableaux
• Pruning the search space and extracting more models in tableaux
• The disconnection method
• Hyperresolution and automated model building
• Soft typing for ordered resolution
• Hyper tableaux
• Automated Reasoning
• Lemma Learning in the Model Evolution Calculus
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The model evolution calculus as a first-order DPLL method