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

Last Modified: 2016-01-01