http://www.cs.bham.ac.uk/~mmk

Computer Science, The University of Birmingham

Birmingham B15 2TT, England

Humans use semantic information in their proof search, and typically
they know important models of mathematical concepts. Models can be
used to direct proof search in systems such as
Scott [Slaney94a] or the semantically guided clause graph
procedure [AI2002-clausegraph]. Model generation itself can be
computationally very hard and typically complete methods are used,
which are built on variants of the Davis-Putnam-Loveland-Logemann
method. Such model generators are `Mace` (*M*odels
*A*nd *C*ounter-*E*xamples) [McCune03] and
`Finder` [Slaney94]. In this abstract we propose a method using a local
search approach. Such approaches have proved successful in constraint
satisfaction and propositional logic model generation. We adopt the
method for the generation of finite models of first-order clauses.

The approach we are proposing takes as input a first-order clause set, FCLAUSE, and the intended cardinality of the model, n. In a first step the first-order clause set is translated to a propositional logic one, C. Then a random initial interpretation I is generated and the number of clauses satisfied in C is calculated. This interpretation is modified until the process is either stuck and restarted, or a model is found (see Figure 1).

Compared to the actual PHP-implementation, which can be run for some few examples from http://www.cs.bham.ac.uk/~mmk/demos/LocModGen, there are some simplifications in the abstract description. Typically the procedure tries to make small positive steps (S+), by modifying one single element in the interpretation. The change is taken over only if it increases the number of satisfied propositional logic clauses. If the procedure does not make any progress for a while - measured by a counter j - it tries to make a big positive step (B+), in which the change is taken over only if it increases the number of satisfied propositional logic clauses. If neither is successful for a number of steps (e.g., 100 steps) it makes a big arbitrary step (B*). If all this is not successful after a number of steps (e.g., 150 steps), the procedure restarts (RESTART). There are two resource constraints, the maximal number of steps allowed and the maximum time spent on the search. If the process runs out of resources, it will return the best interpretation found so far.

For transforming first-order clauses to propositional logical ones, it
is necessary to fix the cardinality n of the universe. It is assumed
that the universe is given in the form of the first n natural
numbers, {1,... ,n}. We add constant symbols
,... , to the syntax, which stand for 1,... ,n,
respectively, (in order to simplify notation we will write simply
1,... ,n). All clauses are replaced by their variable-free
counterparts, that is, each variable is systematically replaced by each
of its possible values in {1,... ,n}. For instance the clause
P(x,a),Q(y,f(x)) with n=3 will be replaced by
the following nine clauses

- P(1,a),Q(1,f(1))
- P(1,a),Q(2,f(1))
- P(1,a),Q(3,f(1))

- P(2,a),Q(1,f(2))
- P(2,a),Q(2,f(2))
- P(2,a),Q(3,f(2))

- P(3,a),Q(1,f(3))
- P(3,a),Q(2,f(3))
- P(3,a),Q(3,f(3))

While the method presented here has the disadvantage that we cannot use it to prove that there is no model, we can use it to define a notion of "near-model", which tells that an interpretation satisfies k out of m propositional logical clauses. Such near models may be used as a heuristic in adaptations of the methods described in [Slaney94a] and [AI2002-clausegraph]. The method presented here can also be directly adapted to deal with higher-order formulae.

- [AI2002-clausegraph] Seungyeob Choi and Manfred Kerber. Semantic selection for resolution in clause graphs. In B. McKay, J. Slaney, eds., AI-2002: 15th Australian Joint Conference on Artificial Intelligence, pages 83-94. Springer, 2002.
- [McCune03] William McCune. Mace4: Models and counter-examples. Argonne National Laboratory, Illinois, USA, 2003. http://www.mcs.anl.gov/AR/mace4/.
- [Slaney94] John Slaney. Finder: Finite domain enumerator-system description. In A. Bundy, ed., 12th CADE, pages 798-801. Springer, 1994.
- [Slaney94a] John Slaney, Ewing Lusk, William McCune. SCOTT: Semantically Constraint Otter - System Description. In A. Bundy, ed., 12th CADE, pages 764-768, Springer, 1994.

© 2005, Manfred Kerber

The URL of this page is http://www.cs.bham.ac.uk/~mmk/papers/05-ARW.html.

Also available as pdf ps.gz bib .