Computing finite models by reduction to function-free clause logic

DOI10.1016/j.jal.2007.07.005zbMath1171.68040OpenAlexW2162131937MaRDI QIDQ1006733

Peter Baumgartner, Alexander Fuchs, Cesare Tinelli, Hans de Nivelle

Publication date: 25 March 2009

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2007.07.005

zbMATH Keywords

model buildingautomated theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Exploring Theories with a Model-Finding Assistant, Constraint solving for finite model finding in SMT solvers, Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA, Superposition for Bounded Domains, MACE4 and SEM: A Comparison of Finite Model Generators, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Exploiting Symmetry in SMT Problems, Blocking and other enhancements for bottom-up model generation methods, Model Finding for Recursive Functions in SMT

Uses Software

• Paradox
• TPTP
• Darwin
• FINDER
• E-Darvin
• Mace4
• Chaff
• E Theorem Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library. CNF release v1. 2. 1
• Computing answers with model elimination
• Proof and Model Generation with Disconnection Tableaux
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• A Powerful Technique to Eliminate Isomorphism in Finite Model Search
• Proving Theorems with the Modification Method
• Automated Reasoning
• Lemma Learning in the Model Evolution Calculus
• Automated Deduction – CADE-19