Finite Model Generation
Given a set of formulas in the first-order logic, can we check its consistency or satisfiability automatically?
The answer is NO, because the first-order logic is undecidable. There have been quite some works on decidable
sub-classes of the logic, which consider only restricted forms of first-order formulas.
If a set of formulas is consistent, it is satisfiable in some model.
Instead of syntactic restrictions, we could restrict the size of models.
We may assume that the formulas are satisfied in a finite model of size N.
Then we can search for a model having N elements.
This is called Finite Model Generation.
(Sometimes we also use the phrase model building or model finding or model searching.)
A popular class of methods for doing that is based on backtracking search. Such methods can be viewed as a generalization of
DPLL-style algorithms for solving the SAT problem in the propositional logic.
In the early and mid-1990's, I spent much time studying how to find a finite model efficiently, for a given set of first-order formulas.
Working with Hantao Zhang, I implemented a finite model searching tool called
SEM.
Developed on Unix systems, it was first released in the summer of 1995.
(Recently, Zhiqiang Zhang ported it to Windows. You may download the executable for
64-bit systems or for 32-bit systems.)
Related Papers
- Hantao Zhang and Jian Zhang. MACE4 and SEM:
A Comparison of Finite Model Generators. In: Automated Reasoning and Mathematics - Essays in Memory of William W. McCune,
LNCS 7788. pp.101-130, 2013.
- Jian Zhang.
Automatic symmetry breaking method combined with SAT.
Proc. SAC 2001, pp.17-21.
- Jian Zhang.
System Description:
MCS: Model-based Conjecture Searching. Proc. CADE-16 (1999), pp.393-397.
- Jian Zhang. On the Relational Translation Method for Propositional Modal Logics.
Technical Report ISCAS-LCS-96-12, Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Dec. 1996.
- Jian Zhang and Hantao Zhang. System Description:
Generating Models by SEM. Proc. CADE-13, pp.308-312, 1996.
- Jian Zhang and Hantao Zhang. SEM: a
System for Enumerating Models. Proc. IJCAI-95, pp.298-303.
Last Modified: 2016-01-01