Logical Inference and Model Building

1 Introduction

Within the area of automated reasoning, first order theorem proving and model building (or model generation) have both received much attention, and have given rise to highly sophisticated techniques. We focus therefore on providing an NLTK interface to third party tools for these tasks. In particular, the module nltk.inference can be used to access both theorem provers and model builders.

2 NLTK Interface to Theorem Provers

The nltk.inference module contains a method get_prover() that takes a proof goal and optionally, the name of a theorem prover. The default is 'Prover9', but the tableau prover may be used by specifying 'tableau'. The proof goal needs to be an instance of the Expression class specified by nltk.sem.logic. In the following example, the proof goal is a biconditional.

>>> from nltk.inference import *
>>> from nltk.sem import LogicParser, ApplicationExpression
>>> lp = LogicParser()
>>> bicond = lp.parse('(exists x.(man(x) and walks(x)) <-> exists x.(walks(x) and man(x)))')
>>> get_prover(bicond, prover_name='tableau').prove()
True
>>> get_prover(bicond, prover_name='Prover9').prove()
True

3 Prover9

3.1 Prover9 Installation

You can download Prover9 from http://www.cs.unm.edu/~mccune/prover9/.

Extract the source code into a suitable directory and follow the instructions in the Prover9 README.make file to compile the executables. Install these into an appropriate location; the prover9_search variable is currently configured to look in the following locations:

>>> prover9_path 
['/usr/local/bin/prover9', '/usr/local/bin/prover9/bin',
'/usr/local/bin', '/usr/bin', '/usr/local/prover9',
'/usr/local/share/prover9']

If the executables cannot be found, Prover9 will issue a warning message:

>>> p = Prover9() 
Traceback (most recent call last):
  ...
LookupError:
===========================================================================
  NLTK was unable to find the prover9 executable!  Use config_prover9() or
  set the PROVER9HOME environment variable.
<BLANKLINE>
    >> config_prover9('/path/to/prover9')
<BLANKLINE>
  For more information, on prover9, see:
    <http://www.cs.unm.edu/~mccune/prover9/>
===========================================================================

The path to the correct directory can be set manually in the following manner:

>>> config_prover9(path='/usr/local/bin') 
[Found prover9: /usr/local/bin/prover9]

3.2 Using Prover9

The general case in theorem proving is to determine whether S |- g holds, where S is a possibly empty set of assumptions, and g is a proof goal.

As mentioned earlier, NLTK input to Prover9 must be Expressions of nltk.sem.logic. A Prover9 instance is initialized with a proof goal and, possibly, some assumptions. The prove() method attempts to find a proof of the goal, given the list of assumptions (in this case, none).

>>> goal = LogicParser().parse('(man(x) <-> --man(x))')
>>> prover = Prover9Command(goal)
>>> prover.prove()
True

Given a Prover9Command instance prover, the method prover.show_proof() will print out the extensive proof information provided by Prover9, shown in abbreviated form here:

============================== Prover9 ===============================
Prover9 (32) version ...
Process ... was started by ... on ...
...
The command was ".../prover9 -f ...".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file /var/...


formulas(goals).
(all x (man(x) -> man(x))).
end_of_list.

...
============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 6317 exit (max_proofs) Mon Jan 21 15:23:28 2008

As mentioned earlier, we may want to list some assumptions for the proof, as shown here.

>>> g = LogicParser().parse('mortal(socrates)')
>>> a1 = LogicParser().parse('all x.(man(x) -> mortal(x))')
>>> prover = Prover9Command(g, assumptions=[a1])
>>> prover.print_assumptions()
all x.(man(x) -> mortal(x))

However, the assumptions are not sufficient to derive the goal:

>>> print prover.prove()
False

So let's add another assumption:

>>> a2 = LogicParser().parse('man(socrates)')
>>> prover.add_assumptions([a2])
>>> prover.print_assumptions()
all x.(man(x) -> mortal(x))
man(socrates)
>>> print prover.prove()
True

We can also show the assumptions in Prover9 format.

>>> prover.print_assumptions(output_format='Prover9')
all x (man(x) -> mortal(x))
man(socrates)

>>> prover.print_assumptions(output_format='Spass')
Traceback (most recent call last):
  . . .
NameError: Unrecognized value for 'output_format': Spass

Assumptions can be retracted from the list of assumptions.

>>> prover.retract_assumptions([a1])
>>> prover.print_assumptions()
man(socrates)
>>> prover.retract_assumptions([a1])

Statements can be loaded from a file and parsed. We can then add these statements as new assumptions.

>>> g = LogicParser().parse('all x.(boxer(x) -> -boxerdog(x))')
>>> prover = Prover9Command(g)
>>> prover.prove()
False
>>> import nltk.data
>>> new = nltk.data.load('grammars/background0.fol')
>>> for a in new:
...     print a
all x.(boxerdog(x) -> dog(x))
all x.(boxer(x) -> person(x))
all x.-(dog(x) & person(x))
exists x.boxer(x)
exists x.boxerdog(x)
>>> prover.add_assumptions(new)
>>> print prover.prove()
True
>>> prover.show_proof() 
============================== prooftrans ============================
Prover9 (...) version ...
Process ... was started by ... on ...
...
The command was ".../prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at ... seconds.
% Length of proof is 13.
% Level of proof is 4.
% Maximum clause weight is 0.
% Given clauses 0.

1 (all x (boxerdog(x) -> dog(x))).  [assumption].
2 (all x (boxer(x) -> person(x))).  [assumption].
3 (all x -(dog(x) & person(x))).  [assumption].
6 (all x (boxer(x) -> -boxerdog(x))).  [goal].
8 -boxerdog(x) | dog(x).  [clausify(1)].
9 boxerdog(c3).  [deny(6)].
11 -boxer(x) | person(x).  [clausify(2)].
12 boxer(c3).  [deny(6)].
14 -dog(x) | -person(x).  [clausify(3)].
15 dog(c3).  [resolve(9,a,8,a)].
18 person(c3).  [resolve(12,a,11,a)].
19 -person(c3).  [resolve(15,a,14,a)].
20 $F.  [resolve(19,a,18,a)].

============================== end of proof ==========================

4 The tp_equals() method

One application of the theorem prover functionality is to check if two Expressions have the same meaning. The tp_equals() method calls a theorem prover to determine whether two Expressions are logically equivalent.

>>> a = LogicParser().parse(r'exists x.(man(x) & walks(x))')
>>> b = LogicParser().parse(r'exists x.(walks(x) & man(x))')
>>> print a.tp_equals(b)
True

The same method can be used on Discourse Representation Structures (DRSs). In this case, each DRS is converted to a first order logic form, and then passed to the theorem prover.

>>> from nltk.sem.drt import DrtParser
>>> a = DrtParser().parse(r'drs([x],[man(x), walks(x)])')
>>> b = DrtParser().parse(r'drs([x],[walks(x), man(x)])')
>>> print a.tp_equals(b)
True

Checking for equality of two DRSs is very useful when generating readings of a sentence. For example, the drt_glue module generates two readings for the sentence John sees Mary:

>>> from nltk.sem import logic
>>> from nltk.internals import Counter
>>> logic._counter = Counter()
>>> from nltk_contrib.gluesemantics.drt_glue import DrtGlue
>>> readings = DrtGlue().parse_to_meaning('John sees Mary')
>>>
>>> for drs in readings: print drs.simplify()
...
DRS([x,z1],[(x = Mary), (z1 = John), sees(z1,x)])
DRS([x,z2],[(x = John), (z2 = Mary), sees(x,z2)])

However, it is easy to tell that these two readings are logically the same, and therefore one of them is superfluous. We can use the theorem prover to determine this equivalence, and then delete one of them. A particular theorem prover may be specified, or the argument may be left off to use the default.

>>> readings[0].tp_equals(readings[1])
True

5 NLTK Interface to Model Builders

The top-level to model builders is parallel to that for theorem-provers. The method get_model_builder() takes an Expression and, optionally, the name of a model builder prover. The default is 'Mace', (or more precisely, 'Mace4') which is currently the only model builder supported.

Typically we use a model builder to show that some set of formulas has a model, and is therefore consistent. One way of doing this is by treating our candidate set of sentences as assumptions, and leaving the goal unspecified. Thus, the following interaction shows how both {a, c1} and {a, c2} are consistent sets, since Mace succeeds in a building a model for each of them, while {c1, c2} is inconsistent.

>>> a3 = lp.parse('exists x.(man(x) and walks(x))')
>>> c1 = lp.parse('mortal(socrates)')
>>> c2 = lp.parse('-mortal(socrates)')
>>> print get_model_builder(None, [a3, c1]).build_model()
True
>>> print get_model_builder(None, [a3, c2]).build_model()
True

We can also use the model builder as an adjunct to theorem prover. Let's suppose we are trying to prove S |- g, i.e. that g is logically entailed by assumptions S = {s1, s2, ..., sn}. We can this same input to Mace4, and the model builder will try to find a counterexample, that is, to show that g does not follow from S. So, given this input, Mace4 will try to find a model for the set S' = {s1, s2, ..., sn, (not g)}. If g fails to follow from S, then Mace4 may well return with a counterexample faster than Prover9 concludes that it cannot find the required proof. Conversely, if g is provable from S, Mace4 may take a long time unsuccessfully trying to find a counter model, and will eventually give up.

In the following example, we see that the model builder does succeed in building a model of the assumptions together with the negation of the goal. That is, it succeeds in finding a model where there is a woman that every man loves; Adam is a man; Eve is a woman; but Adam does not love Eve.

>>> a4 = lp.parse('exists y. (woman(y) & all x. (man(x) -> love(x,y)))')
>>> a5 = lp.parse('man(adam)')
>>> a6 = lp.parse('woman(eve)')
>>> g = lp.parse('love(adam,eve)')
>>> print get_model_builder(g, [a4, a5, a6]).build_model()
True

6 Mace4

6.1 Mace4 Installation

Mace4 is packaged with Prover9, and can be downloaded from the same source, namely http://www.cs.unm.edu/~mccune/prover9/. It is installed in the same manner as Prover9.

6.2 Using Mace4

Check whether Mace4 can find a model.

>>> a = LogicParser().parse('(see(mary,john) & -(mary = john))')
>>> mb = MaceCommand(assumptions=[a])
>>> mb.build_model()
True

Show the model in 'tabular' format.

>>> mb.show_model(format='tabular')
% number = 1
% seconds = 0

% Interpretation of size 2

 john : 0

 mary : 1

 see :
       | 0 1
    ---+----
     0 | 0 0
     1 | 1 0