In order to make a proof using OTTER, one need to compose an input file. This file contains not only the assumptions and the conclusion one wants to check, but also general directives to instruct OTTER how to proceed with the proof.
A description of the components of an input file for OTTER is given below. The general file format contains the minimum set of directives needed to submit a proof to OTTER. The formulas in the assumptions and the conclusion can be given in a number of different formats. We will consider two of such formats: full first-order logic form and clausal form. The clausal format is more appealing to people with less knowledge of Logic and resembles Prolog's syntax. On the other hand, the full first-order logic format is more general and allows for the specification of more sophisticated kinds of information.
We also give two simple examples of input files using Full First-Order Logic and Clauses only.
General
Input File Format
Full First-Order
Logic Formula Format
Clause
Format
Sample Clausal File
Sample
First-Order Logic File
Sample
Clausal File
Understanding
the output result
Files submitted to Otter have to be written using a specific syntax. The parameters will actually be automatised in the implementation of e-Plato. For testing purposes only, the generator module is not yet implemented, so one needs to create the input file, whose format is specified below:
| set(auto). | This specifies that OTTER will run in automatic mode, i.e., without human intervention. |
| formula_list(usable). | This directive specifies the beginning of the list of formulas to be submitted to the prover. |
| list of well formed formulas one each line... | The list of formulas goes here. The negation of the conclusion to be proved must be incorporated and put at the end of the list. |
| end_of_list. | This directive marks the end of the list of formulas. |
Full First-Order Logic Formula Format (well formed formulas)
Formulas can be written using the following logical symbols:
|
connective
|
OTTER's
notation
|
|---|---|
| negation | - |
| disjunction | | |
| conjunction | & |
| implication | -> |
| equivalence | <-> |
| existential quantification | exists |
| universal quantification | all |
Note that if a formula has a string of identical quantifiers, all but the first can be dropped. For example, all x all y all z p(x,y,z) can be shortened to all x y z p(x,y,z). In expressions involving the associative operations & and |, extra parentheses can be dropped. Moreover, a default precedence on the logic symbols allows us to drop more parentheses: <-> has the same precedence as ->, and the rest in decreasing order are ->, |, &, -. Greater precedence means closer to the root of the term (i.e., larger scope).
For example, p | -q & r -> -s | t represents (p | (-(q) & r)) -> (-(s) | t).
When in doubt about how a particular string will be parsed, one can simply add additional parentheses.
Formulas are always terminated by a dot '.'.
The following are examples of formulas written using OTTER's syntax:
|
formula
|
OTTER's
syntax
|
|---|---|
| for all x P(x) | all x P(x). |
| for all x for all y there exists z(P(x, y, z) or Q(x, z)) | all x y exists z (P(x,y,z) | Q(x,z)). |
| for all x ((P(x) and Q(x) and R(x)) implies S(x)) | all x (P(x) & Q(x) & R(x) -> S(x)). |
Clause Format (well formed clauses)
Similar to the way clauses are written in Prolog. The directives list(usable) must be use instead of formula_list(usable). In addition, set(prolog_style_variables) must also be used to allow for Prolog's convention of uppercase letter representing variables.
See sample file below.
Clauses are also always terminated by a dot '.'.
|
Type
of Clause
|
OTTER's
syntax
|
|---|---|
| Facts | -> fact(term). |
| Rules | body_one(term), body_two(term) ... body_n(term) -> head(term). |
| Goal | goalone(term), goal_two(term), ..., goal_n(term) ->. |
set(auto).
formula_list(usable).
all x (x = x).
all x y z (f(f(x,y),z) = f(x,f(y,z))).
exists e ( (all x (f(e,x) = x) ) & (all x exists y (f(y,x) = e) ) &
(all x (f(x,x) = e)) ) .
-(all x y (f(x,y) = f(y,x))).
end_of_list.
set(auto).
set(input_sequent).
set(output_sequent).
set(prolog_style_variables).
list(usable).
-> human(socrates).
human(X) -> mortal(X).
mortal(socrates) ->.
end_of_list.
With the informal meaning:
"Socrates is human. All humans are mortals. Is Socrates mortal?".
Understanding the Output Result
This section was taken from OTTER's manual.
When a proof is submitted to OTTER, this web interface will collect its results and display them on the screen. A message reporting success or failure will be displayed. In addition, details of the proof are also shown. These come in two flavours, detailed and non-detailed. In the detailed version, details of the proof along with information about the execution of the proof are displayed. In the non-detailed version, only the summery of the proof itself is displayed. In either case, proofs are displayed listing all clauses used in the proof. Whenever a clause is printed, it is printed with its integer identifier (ID) and a justification list, which is enclosed in brackets.
We will use this mechanism of displaying proofs to translate the proof back to the original English meaning of each formula.
Examples of clauses printed
in the proof:
4 [] -j(x,y)|j(x,0).
13 [hyper,11,8,eval,demod] j(3,1).
41 [31,demod] p([a,b,b,c,c,c,d,e,f]).
14 [new_demod,13] f(y,f(y,f(y,x)))=x.
71 [back_demod,58,demod,70,14,55,11,34,11] e!=e.
12 [demod,9] f(a,f(b,f(g(a),g(b))))!=e.
77 [binary,57.3,30.2] sm|mm| -sl.
33,32 [para_from,26.1.1,15.1.1.2,demod,21] g(x)=f(x,x).
36 [hyper,31,2,26,30,unit_del,19,18,20,19] p(k,g(k)).
4 [factor_simp,factor_simp] p(x)|p($f1(x))| -q($f2(y))| -q(y)|p($c6).
199 [binary,198.1,191.1,factor_simp] q($c14).
If the justification list is empty, the clause was input. Otherwise, the first item in the justification list is one of the following.
An inference rule. The clause was generated by an inference rule. The IDs of the parents are listed after the inference rule with the given clause ID listed first (unless order_history is set).
A clause identifier. The clause was generated by the demod_inf rule.
new demod. The clause is a dynamically generated demodulator; it is a copy of the clause whose ID is listed after new_demod.
back demod.
The clause was generated by back demodulating the clause whose ID is listed
after back_demod.
demod. The clause was generated by back demodulating an input clause.
factor simp. The clause was generated by factor-simplifying an input clause. For example, p(x)|p(a) factor-simplifies to p(a).
The sublist [demod, id1, id2, . . .] indicates demodulation with id1, id2, . . .. The sublist [unit del, id1, id2, . . .] indicates unit deletion with id1, id2, . . .. The symbols eval indicates that a literal was “resolved” by evaluation during hyperresolution. The sublist [factor simp, factor simp, . . .] indicates a sequence of factor simplification steps.
In proofs, some clauses are printed with two (consecutive) IDs. In such a case, the clause is a dynamically generated demodulator, and the two IDs refer to difierent copies of the same clause: the first ID refers to its use for inference rules, and the second to its use as a demodulator.
If the fiag detailed_history
is set, then for the inference rules binary_res, para_from, and para_into, the
positions of the unified literals or terms are listed along with the parent
IDs. For example, [binary,57.3,30.2] means that the third literal of clause
57 was resolved with the second literal of clause 30. For paramodulation, the
“from” parent is listed as ID.i.j, where i is the literal number of
the equality literal, and j (either 1 or 2) is the number of the unified equality
argument; the “into” parent is listed as ID.i.j1. · ·
·.jn, where i is the literal number of the “into” term, and
j1. · · ·.jn is the position vector of the “into”
term; for example, 400.3.1.2 refers to the second argument of the first argument
of third literal of clause 400. If the flag para_all is set, then the paramodulation
positions are not
listed.
When the flag sos_queue is set, the search is breadth first (level saturation), and Otter sends a message to the output file when given clauses start on a new level. (Input clauses have level 0, and generated clauses have vel one greater than the maximum of the levels of the parents. Since clauses are given in the order in which they are retained, the level of given clauses never decreases.)