Otter
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:
Otter
PackageTo install the Otter
package: (1) download the package file otter.m
from the following url:
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
PackageWe can see all the Mathematica functions that
the Otter
package
provides, as follows:
|
Otter
PackageToOtter
function:
Here's a non-trivial example, illustrating the use of
the translation function ToOtter
:
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:
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.
Otter
Package
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 ± =
{} entails
= . So,
the set
is unsatisfiable. Therefore,
if we run the following input file in Otter
,
we should get a proof.
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:
It is not obvious to the naked eye, but γ is unsatisfiable. Here is the Otter input file for γ:
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:
Running Otter
(3.0.4) on the following input file
generates a non-trivial 13-step proof which uses paramodulation, demodulation, hyperresolution, and factoring.
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).
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).
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.
Here's an example. The following set is unsatisfiable:
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:
Otter
and Automated ReasoningThere 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:
Converted by Mathematica (August 22, 2002)