Computing finite models by reduction to function-free clause logic
From MaRDI portal
Publication:1006733
DOI10.1016/J.JAL.2007.07.005zbMATH Open1171.68040OpenAlexW2162131937MaRDI QIDQ1006733FDOQ1006733
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
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
- The TPTP problem library. CNF release v1. 2. 1
- Automated Reasoning
- Proof and model generation with disconnection tableaux
- Lemma Learning in the Model Evolution Calculus
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Title not available (Why is that?)
- Handbook of automated reasoning. In 2 vols
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- The state of CASC
- The model evolution calculus.
- Title not available (Why is that?)
- Proving Theorems with the Modification Method
- Title not available (Why is that?)
- Computing answers with model elimination
- A Powerful Technique to Eliminate Isomorphism in Finite Model Search
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
- Title not available (Why is that?)
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA
- Title not available (Why is that?)
- 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
Uses Software
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)
