Computing finite models by reduction to function-free clause logic

DOI10.1016/J.JAL.2007.07.005MaRDI QIDQ1006733zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• A calculus combining resolution and enumeration for building finite models
• Model building with ordered resolution: Extracting models from saturated clause sets
• Finite model finding using the logic of equality with uninterpreted functions
• Finding Finite Models in Multi-sorted First-Order Logic
• The model evolution calculus.

Cites work

• scientific article; zbMATH DE number 4053069 (Why is no real title available?)
• scientific article; zbMATH DE number 1301750 (Why is no real title available?)
• scientific article; zbMATH DE number 1303344 (Why is no real title available?)
• A Powerful Technique to Eliminate Isomorphism in Finite Model Search
• Automated Reasoning
• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• Computing answers with model elimination
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Handbook of automated reasoning. In 2 vols
• Lemma Learning in the Model Evolution Calculus
• Proof and model generation with disconnection tableaux
• Proving Theorems with the Modification Method
• The TPTP problem library. CNF release v1. 2. 1
• The model evolution calculus.
• The state of CASC

Cited in

(13)

• Blocking and other enhancements for bottom-up model generation methods
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Superposition for bounded domains
• Exploring theories with a model-finding assistant
• A calculus combining resolution and enumeration for building finite models
• scientific article; zbMATH DE number 67452 (Why is no real title available?)
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA
• scientific article; zbMATH DE number 4043224 (Why is no real title available?)
• MACE4 and SEM: a comparison of finite model generators
• Exploiting symmetry in SMT problems
• Model finding for recursive functions in SMT
• Constraint solving for finite model finding in SMT solvers

Describes a project that uses

Uses Software

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

This page was built for publication: Computing finite models by reduction to function-free clause logic

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