Using Mathematica as a Graphical Front-End for Otter

Zac Ernst and Branden Fitelson

Philosophy Department, University of Wisconsin-Madison
and
Mathematics and Computer Science Division, Argonne National Laboratory

August, 2001

NOTE: A Mathematica notebook version of this webpage (from which this HTML page was generated automatically using Mathematica 4.2) can be downloaded from the following url:

http://fitelson.org/otter.nb

1.  Installation & Loading in the Otter Package

To install the Otter package: (1) download the package file otter.m from the following url:

http://fitelson.org/otter.m

Then (2) place the otter.m file in a place where Mathematica can see it.

Finally, (3) use the following command to load the Otter package (again, you must make sure that the file otter.m is in a path that Mathematica can see, or you can use the InputFilePath command in Mathematica to directly specify the path of the file otter.m supplied with this package):

<< otter.m

2.  Examining the Functions Defined in the Otter Package

We can see all the Mathematica functions that the Otter package provides, as follows:

? Otter`*

Otter`

MathematicaToOtterPrefix

ShowOtterInputFile

WriteOtterInputFile

OtterProof

ToOtter

 

2.1  The Basic Translation Functions of the Otter Package

ToOtter function:

? ToOtter

ToOtter[statement_].  Converts an arbitrary statement in first-order logic with equality from Mathematica's (NormalForm) syntax to Otter's formula syntax.   The output of this function can be copied and pasted directly into  any Otter input file (i.e., into an Otter formula_list).

Here's a non-trivial example, illustrating the use of the translation function ToOtter:

ToOtter[&emdash; _ x &emdash; _ y (S[x, y] <=> (&#8707; _ z (P[z, x] &#8743; P[z, y]) &#8743; ¬ Q[x, y]))]

(all x (all y (S(x, y) <-> ((exists z (P(z, x) & P(z, y))) & -Q(x, y))))).

The output of ToOtter can be copied and pasted directly into any Otter input file (in a formula_list).

We can also convert from Mathematica syntax to Otter's "pure prefix" syntax, using the alternative translation function MathematicaToOtterPrefix, as the following example illustrates:

MathematicaToOtterPrefix[&emdash; _ x &emdash; _ y (S[x, y] <=> (&#8707; _ z (P[z, x] &#8743; P[z, y]) &#8743; ¬ Q[x, y]))]

$Quantified(all,x,all,y,<->,S(x, y),&,exists,z,&,P(z, x),P(z, y),-,Q(x, y)).

Full first-order syntax (including n-ary functions and predicates) with equality is supported.  Standard Mathematica syntax is assumed.  Since Mathematica does not have a built-in "if and only if" function, we have stipulated the symbol "<=>" to play this role.

2.2  The Input-File Generation Functions of the Otter Package

? ShowOtterInputFile

ShowOtterInputFile[set_].   Creates an (autonomous mode) Otter input file, containing an arbitrary set of first-order formulas (converted into Otter's formula syntax, using the ToOtter function) in its formula_usable list.  This file is then written to the screen.  It can then be copied, pasted, and saved to a file, on which Otter can then be run, in the usual way.

Let's say you are trying to prove some first-order formula ’ from a set of first-order formulae ±.  This is equivalent to trying to demonstrate that the set of formulas β = ± ∪ {¬’} is unsatisfiable.  We can generate an (autonomous mode) Otter input file which will attempt to prove that a set β of first order formulas is unsatisfiable.  If Otter is run on an input file containing the members of β in the formula_usable list, and it returns a proof, then the set β is unsatisfiable (and, consequently,  ± entails ’).  Of course, if Otter does not return a proof, we cannot necessarily infer that no proof exists (this is because first-order logic is undecidable).  Let's start with a simple example.  In first-order logic, we know that ± = {&#8707; _ x &emdash; _ y P[x, y]}  entails ’ =  &emdash; _ y &#8707; _ x P[x, y].  So, the set

&#946; = {&#8707; _ x &emdash; _ y P[x, y], ¬ &emdash; _ y &#8707; _ x P[x, y]} ;

is unsatisfiable.  Therefore, if we run the following input file in Otter, we should get a proof.

ShowOtterInputFile[&#946;]

set(auto).
formula_list(usable).
(exists x (all y P(x, y))).
(exists y (all x -P(x, y))).
end_of_list.

Sure enough, when this file in input to Otter, a trivial (zero step) hyperresolution proof is returned.  The input files displayed by ShowOtterInputFile will run on any platform, using version 3.x (or later) of Otter.

Here is a more complicated example.  Consider the following set of first-order formulae:

&#947; = { &emdash; _ x &#8707; _ y P[y, x], &emdash; _ x &emdash; _ y (P[x, y] => ¬ P[y, x]), &emdash; _ x &emdash; _ y (S[x, y] <=> (&#8707; _ z (P[z, x] &#8743; P[z, y]) &#8743; ¬ Q[x, y])), &emdash; _ x Q[x, x], &emdash; _ x &emdash; _ y (Q[x, y] => Q[y, x]), &emdash; _ x &emdash; _ y &emdash; _ z ((Q[x, y] &#8743; Q[y, z]) => Q[x, z]), &emdash; _ x &emdash; _ y &emdash; _ z ((P[x, y] &#8743; P[y, z]) => ¬ P[x, z]), &emdash; _ x &emdash; _ y &emdash; _ z ((P[x, y] &#8743; Q[z, x]) => P[z, y]), &emdash; _ x &emdash; _ y &emdash; _ z ((P[x, y] &#8743; Q[z, y]) => P[x, z]), &#8707; _ x &#8707; _ y (S[x, y] &#8743; ¬ S[y, x]) } ;

It is not obvious to the naked eye, but γ is unsatisfiable.  Here is the Otter input file for γ:

ShowOtterInputFile[&#947;]

set(auto).
formula_list(usable).
(all x (exists y P(y, x))).
(all x (all y (P(x, y) -> -P(y, x)))).
(all x (all y (S(x, y) <-> ((exists z (P(z, x) & P(z, y))) & -Q(x, y))))).(all x Q(x, x)).
(all x (all y (Q(x, y) -> Q(y, x)))).
(all x (all y (all z ((Q(x, y) & Q(y, z)) -> Q(x, z))))).
(all x (all y (all z ((P(x, y) & P(y, z)) -> -P(x, z))))).
(all x (all y (all z ((P(x, y) & Q(z, x)) -> P(z, y))))).
(all x (all y (all z ((P(x, y) & Q(z, y)) -> P(x, z))))).
(exists x (exists y (S(x, y) & -S(y, x)))).
end_of_list.

This time, when Otter (3.0.4) is run on γ, a 4-step hyperresolution proof is returned.  We are not limited to predicate logic.  We have recourse to the full first-order functional calculus, with equality.  Here's an example involving functions and equality.  The following set is unsatisfiable:

´ = { &#8707; _ x &#8707; _ y (x != y &#8743; &emdash; _ z (z == x &#8744; z == y)), &emdash; _ x &emdash; _ y (f[x] == f[y] => x == y), ¬ &emdash; _ x &#8707; _ y x == f[y] } ;

Running Otter (3.0.4) on the following input file

ShowOtterInputFile[´]

set(auto).
formula_list(usable).
(exists x (exists y ((x!=y) & (all z ((z=x) | (z=y)))))).
(all x (all y ((f(x)=f(y)) -> (x=y)))).
(exists x (all y (x!=f(y)))).
end_of_list.

generates a non-trivial 13-step proof which uses paramodulation, demodulation, hyperresolution, and factoring.  

? WriteOtterInputFile

WriteOtterInputFile[set_, filepath_].  Creates an (autonomous mode) Otter input file, containing an  arbitrary set of first-order formulas (converted into Otter's formula  syntax, using the ToOtter function) in its formula_usable list.   This file is then written to whatever path is specified in the  filepath_ argument (on the local disk).  Otter can then be run,  in the usual way, on the resulting input file.

The function WriteOtterInputFile writes Otter input files to a specified filepath on a local disk.  For instance, we can write the above input file to a local file called "delta.in", as follows (please consult the Mathematica help facility to see how to properly specify filepaths on your operating system).

WriteOtterInputFile[´, "delta.in"]

Otter can then be run directly (on any platform) on the resulting file (consult the Otter user manual for instructions on how to use Otter -- see section 3 below for references).

2.3  Running Otter Directly from Mathematica: the function OtterProof

NOTE: The function OtterProof only works on Linux/UNIX operating systems with Otter properly configured, etc.

If one is working on a Linux/UNIX operating system (with Otter properly installed on the system -- that is, so that the command "otter < input > output" will execute properly from the path containing this Mathematica file), one can run Otter directly from the Mathematica front-end, and view the proof it finds (if it finds one) -- without ever leaving Mathematica.

? OtterProof

OtterProof[set_].  Writes an (autonomous mode) Otter input file for a set of formulas (using the function WriteOtterInputFile), then runs Otter on the input file, and returns the proof (if one is found) directly to the Mathematica front-end.  NOTE: this function only works on Linux/UNIX systems with Otter properly installed --- that is, so that the command 'otter' will execute properly from the path containing this Mathematica file.  The Otter input and output files written to disk are 'ottertemp.in' and 'ottertemp.out', respectively.

Here's an example.  The following set is unsatisfiable:

õ = { &emdash; _ x &#8707; _ y Parent[y, x], &emdash; _ x &emdash; _ y (Parent[x, y] => ¬ Parent[y, x]), &emdash; _ x &emdash; _ y &emdash; _ z ((Parent[x, z] &#8743; Parent[y, z]) => (x == y)), &emdash; _ x &emdash; _ y (Sibling[x, y] <=> (&#8707; _ z (Parent[z, x] &#8743; Parent[z, y]) &#8743; x != y)), &emdash; _ x &emdash; _ y (Grandparent[x, y] <=> &#8707; _ z (Parent[x, z] &#8743; Parent[z, y])), &emdash; _ x &emdash; _ y (Uncle[x, y] <=> &#8707; _ z (Sibling[z, x] &#8743; Parent[z, y])), ¬ &emdash; _ x &emdash; _ y &emdash; _ z (Uncle[x, y] &#8743; Uncle[y, z] => ¬ Grandparent[x, z]) } ;

If we run OtterProof on õ (Otter 3.0.6, and Linux OS), we quickly get the following 17-step hyperresolution and demodulation proof echoed directly back to our Mathematica session:

OtterProof[õ]

---------------- PROOF ----------------
1 [] -Parent(x,y)| -Parent(y,x).
2 [] -Parent(x,y)| -Parent(z,y)|x=z.
3 [] -Sibling(x,y)|Parent($f2(x,y),x).
4 [] -Sibling(x,y)|Parent($f2(x,y),y).
5 [] -Sibling(x,y)|x!=y.
7 [] -Grandparent(x,y)|Parent(x,$f3(x,y)).
8 [] -Grandparent(x,y)|Parent($f3(x,y),y).
10 [] -Uncle(x,y)|Sibling($f4(x,y),x).
11 [] -Uncle(x,y)|Parent($f4(x,y),y).
14 [factor,2,1,2] -Parent(x,y)|x=x.
17 [] Uncle($c3,$c2).
18 [] Uncle($c2,$c1).
19 [] Grandparent($c3,$c1).
25 [hyper,17,11] Parent($f4($c3,$c2),$c2).
26 [hyper,17,10] Sibling($f4($c3,$c2),$c3).
31 [hyper,18,11] Parent($f4($c2,$c1),$c1).
32 [hyper,18,10] Sibling($f4($c2,$c1),$c2).
37 [hyper,19,8] Parent($f3($c3,$c1),$c1).
38 [hyper,19,7] Parent($c3,$f3($c3,$c1)).
91 [hyper,32,4] Parent($f2($f4($c2,$c1),$c2),$c2).
92 [hyper,32,3] Parent($f2($f4($c2,$c1),$c2),$f4($c2,$c1)).
104,103 [hyper,37,2,31] $f4($c2,$c1)=$f3($c3,$c1).
109 [back_demod,92,demod,104,104] Parent($f2($f3($c3,$c1),$c2),$f3($c3,$c1)).
110 [back_demod,91,demod,104] Parent($f2($f3($c3,$c1),$c2),$c2).
122 [hyper,38,14] $c3=$c3.
255,254 [hyper,110,2,25] $f4($c3,$c2)=$f2($f3($c3,$c1),$c2).
302 [back_demod,26,demod,255] Sibling($f2($f3($c3,$c1),$c2),$c3).
411,410 [hyper,109,2,38,flip.1] $f2($f3($c3,$c1),$c2)=$c3.
414 [back_demod,302,demod,411] Sibling($c3,$c3).
457 [hyper,414,5,122] $F.

3.  Information About Otter and Automated Reasoning

There is no limit to the number of first-order problems that can be attacked with Otter.  Indeed, Otter is an extremely powerful and flexible theorem-prover (perhaps the most powerful and flexible in the world).  We urge anyone interested in using Otter to explore automated reasoning in first-order theories to consult the following two sources:

McCune, William, 1994, "Otter 3.0 Reference Manual and Guide", Argonne National Laboratory, Technical Report ANL-94/6, Argonne, IL.

Wos, Larry, and Pieper, Gail, 1999, "A Fascinating Country in  the World of Computing: Your Guide to Automated Reasoning", World Scientific, Singapore.

The former is the official user manual for Otter, which shows you the basics of using Otter (e.g., how to run Otter on the input files generated above, and on more complicated input files, with additional user-controlled strategies and options).  The latter is an encyclopedic treatment of automated reasoning with Otter, which illustrates how Otter can be used to solve challenging and open questions in mathematics and logic.

Otter is free!  The latest version of Otter can be obtained for various platforms, from the following URL:  

http://www-unix.mcs.anl.gov/AR/otter/

Converted by Mathematica  (August 22, 2002)