In the course of the lecture “Ontology-based Interpretation of Natural Language” my team did a project, dealing with the conversion of natural language into first-order logic. The focus was set on parsing soccer-commentary and creating a time-ontology, which is capable of handling time-relations and -intervals. For this purpose we choose a tool called Prover9.

Prover9, developed by William McCune, is the successor of the Otter prover. It provides automatic theorem proving for first-order and equational logic. Prover9 is open source and released under GPL version >= 2. The first release was in July 2005. After that, new versions followed nearly every month, until 2009 when the development stopped. The current version is therefore LADR-2009-11A.


Curious how far we would get with this tool, we gave it a shot.
At first we did some basic examples to get familiar with Prover9. Below I'm briefly going to explain, how to use this tool and what you should keep in mind, while creating you're own complex scenarios.

Example 1:

"All robots enjoy life. ToBI is a robot."
          ? "ToBI enjoys life."
          ? "There is someone who does not enjoy life."

formulas(usable). % Relations
      % All robots enjoy life.
     all x (Robot(x) -> enjoysLife(x)).
end_of_list.

formulas(assumptions). % Knowledge
      % ToBI is a robot.
     Robot(ToBI).
end_of_list.

formulas(goals). % Goals
      % ToBI enjoys life.
     enjoysLife(ToBI).
      % There is someone who does not enjoy life.
     exists x (-enjoysLife(x)).
end_of_list.

Assertion	Consistent	Informativ
"ToBI enjoys life."
"There is someone who does not enjoy life."

After solving the basic sentences without much effort, we quickly ran into some trouble coding the much more complex tasks. The first problem was how to create an awareness of numbers, without actually coding in all relations (like: less(1,2) less(1,3) …) ? Intervals were the answer! We then created some rules that allowed us to create intervals, either overlapping or isolated.

The next scenario was quite a pain in the ***, because we had to count goals. So there was no way around numbers anymore. After several annoying ideas dealing with the definition of numbers as successor of the successor of … the successor of zero, we finally spotted a flicker of hope on the horizon. We discovered the so called “production mode”, which is only available in the command-line version of Prover9, since this is also the only version, which was developed until 2009 (LADR-2009-11A). Unfortunately there's not much documentation for this mode, if your are interested in doing some fancy stuff with it. So let me tell you the main features I found out, while grappling with this mighty tool:

• Numbers
• Relations (<,>,=)
• Recursion
• Lists
• Variables (u,v,w,x,y,z)

The activation of the production mode provides you great new feature, but limits other abilities of Prover9 at the same time. (“because the production mode is quite different and more limited in nature from the ordinary mode of Prover9.” ¹ )

At last we came up with two different versions. The first one makes use of lists (in some kind of haskell-style) to keep track of the goals shot. Unfortunately it is not possible to see which player made a particular goal, because all goals are made by the specific team. In contrast to that, the second approach is mainly based on “nogoals”, which are recursively generated to cover those minutes in which no goal was shot. It also has a very intuitive way to describe and process the given sentence.

If you want to have a look at our solutions mentioned in this post, feel free to do so:

• Robot.in
• NeuerTime.in
• SoccerWithLists.in
• SoccerWithoutLists.in

In the course of the development, I also made a highlighting file for KDE's “Kate”. It is still rudimentary, so there is always room for improvement.

• Prover9_Kate_Highlighting

Below are the slides of the final presentation:

• OloNLII_Prover9.pdf

References:

¹http://www.cs.unm.edu/~mccune/mace4/manual/2009-11A/production.html