.. -*- mode: rst -*-
.. include:: ../../doc/definitions.rst

.. standard global imports

    >>>  import nltk, re, pprint

.. |multimap| unicode:: U+22B8
.. |vdash| unicode:: U+22A6
.. |nvdash| unicode:: U+22AC
.. |delta| unicode:: U+03B4
.. |Delta| unicode:: U+0394
.. |emptyset| unicode:: U+2205
.. |dagger| unicode:: U+2020
.. |tab| unicode:: U+00A0 U+00A0 U+00A0 U+00A0 U+00A0 U+00A0 U+00A0 U+00A0


===============================
Theorem Prover
===============================

:Author: Daniel H. Garrette

---------------------------------
NLTK Interface to Theorem Provers
---------------------------------

The module ``nltk_contrib/theorem_prover/prover.py`` can be used to access the 
theorem provers.  The module contains a method ``attempt_proof()`` that takes 
an ``Expression`` and, optionally, a name of a theorem prover.  The default is 
``'Prover9'``, but the tableau prover may be used by specifying ``'tableau'``.

>>> from nltk_contrib.theorem_prover import prover
>>> from nltk_contrib.drt import DRT
>>> f = DRT.Parser().parse('drs([x],[(man x)])').toFol()
>>> prover.attempt_proof(f)
False

-------
Prover9
-------

Prover9 Installation
~~~~~~~~~~~~~~~~~~~~

You can download Prover9 from http://www.cs.unm.edu/~mccune/prover9/.  Extract the 
source code into '/usr/share/nltk/tools/prover/'.  Follow the instructions from the 
site to compile the prover.

------------
DRS Equality
------------

The theorem prover funtionality can be used in NLTK to check whether two Discourse
Representation Structures (DRSs) are logically equivalent.  

>>> from nltk_contrib.drt import DRT
>>> a = DRT.Parser().parse(r'drs([x],[(man x), (walks x)])')
>>> b = DRT.Parser().parse(r'drs([x],[(walks x), (man x)])')
>>> print a == b
True

Use
~~~

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`:lx:\ :

>>> from nltk_contrib.gluesemantics import drt_glue
>>> readings = drt_glue.parse_to_meaning('John sees Mary')
>>> for drs in readings: print drs.simplify()
...
drs([z1,x],[(= z1 John),(= x Mary),(sees z1 x)])
drs([z2,x],[(= z2 Mary),(= x John),(sees x z2)])

However, it is easy to tell that these two readings are logially the same, and 
therefore, we have no need to keep both of them.  we can use the theorem prover
to determine that they are the same, and to delete one of the readings.

>>> readings[0] == readings[1]
True

----------
References
----------

Blackburn and Bos.  Representation and Inference in Natural Language.
