Using Otter to prove a PARC sentence

We're going to prove this hypothesis using Otter:

(9) Q: The president visited Iraq in September.

A: Has the president gone to Iraq?

YES, STRICT, LINGUISTIC

Since this cannot be proven through first order logic alone, we need an assumption:

Assumption: if X visits Y, then X goes to Y.

We can represent these in Otter's FOL syntax as the following:

  exists 1 2 3 4 (President(1) & Iraq(2) & Visit(3, 1, 2) & September(4) & In(3, 4)).  % text
  exists 1 2 3 (President(1) & Iraq(2) & Go(3, 1, 2))).  % hypothesis
  all a b c (Visit(a, b, c) -> (exists d (Go(d, b, c)))).  % assumption

The syntax is more or less intuitive. For FOL, letters, words, and numbers all work as variables, constants, functions, and predicates, and it deduces from context which they are.

Input

Once we have these written as FOL sentences, we can feed them to Otter in an input file. Since Otter reads from the standard input and prints to the standard output, we call Otter as follows:

Otter < infile > outfile

Here's the input file:

% Text: The President visited Iraq in September.
% Hypothesis: The President has gone to Iraq.
% Assumption: if X visits Y, then X goes to Y.

set(hyper_res).
set(print_lists_at_end).
assign(stats_level, 0).

formula_list(sos).
  exists 1 2 3 4 (President(1) & Iraq(2) & Visit(3, 1, 2) & September(4) & In(3, 4)).
  -(exists 1 2 3 (President(1) & Iraq(2) & Go(3, 1, 2))).
end_of_list.

formula_list(usable).
  all a b c (Visit(a, b, c) -> (exists d (Go(d, b, c)))).
end_of_list.

Now we take each part separately. Comments are marked with a “%”:

% Text: The President visited Iraq in September.
% Hypothesis: The President has gone to Iraq.
% Assumption: if X visits Y, then X goes to Y.

Then, we set some flags. I'm not entirely clear on what these do, but they were used in the examples:

set(hyper_res).
set(print_lists_at_end).
assign(stats_level, 0).

Otter takes a set of sentneces as input and tries to reach a contradiction from them. This means if we want it to prove Q from P_1, ..., P_n, we give it P_1, ..., P_n, and -Q (not-Q). In our case, we have:

formula_list(sos).
  exists 1 2 3 4 (President(1) & Iraq(2) & Visit(3, 1, 2) & September(4) & In(3, 4)).  % text
  -(exists 1 2 3 (President(1) & Iraq(2) & Go(3, 1, 2))). % (negated) hypothesis
end_of_list.

This tells Otter to add these two sentences to its “sos” list. These are the sentences that it actively uses to derive new sentences. By contrast, we add our assumptions to the “usable” list. (I'll explain these lists below.)

formula_list(usable).
  all a b c (Visit(a, b, c) -> (exists d (Go(d, b, c)))).
end_of_list.

Output

Here's the output produced by the above. First, it echoes your input back to you (minus comments):

set(hyper_res).
assign(stats_level,0).

formula_list(sos).
exists 1 2 3 4 (President(1)&Iraq(2)&Visit(3,1,2)&September(4)&In(3,4)).
-(exists 1 2 3 (President(1)&Iraq(2)&Go(3,1,2))).
end_of_list.

Then, it translates your formulas into clauses, Skolemizing existentially quantified variables:

-------> sos clausifies to:

list(sos).
1 [] President($c4).
2 [] Iraq($c3).
3 [] Visit($c2,$c4,$c3).
4 [] September($c1).
5 [] In($c2,$c1).
6 [] -President(x1)| -Iraq(x2)| -Go(x3,x1,x2).
end_of_list.

formula_list(usable).
all a b c (Visit(a,b,c)-> (exists d Go(d,b,c))).
end_of_list.

-------> usable clausifies to:

list(usable).
7 [] -Visit(x4,x5,x6)|Go($f1(x4,x5,x6),x5,x6).
end_of_list.

======= end of input processing =======

For its actual theorem proving, it runs through its sos list. In each iteration, it picks one clause (usually the shortest) as the “given” clause. It moves this clause to the usable list, and then tries to resolve it with each of the clauses in its “usable” list. Any sentences inferred from this are then added to sos. The algorithm runs until a contradiction is found, or the sos list is empty. If a potentially infinite number of sentences can be derived from your lists, you can cap the number of given statements with assign(max_given, 1). The next thing it prints is its list of givens:

=========== start of search ===========

given clause #1: (wt=2) 1 [] President($c4).

given clause #2: (wt=2) 2 [] Iraq($c3).

given clause #3: (wt=2) 4 [] September($c1).

given clause #4: (wt=3) 5 [] In($c2,$c1).

given clause #5: (wt=4) 3 [] Visit($c2,$c4,$c3).
** KEPT (pick-wt=7): 8 [hyper,3,7] Go($f1($c2,$c4,$c3),$c4,$c3).

given clause #6: (wt=7) 8 [hyper,3,7] Go($f1($c2,$c4,$c3),$c4,$c3).

given clause #7: (wt=8) 6 [] -President(x1)| -Iraq(x2)| -Go(x3,x1,x2).
** KEPT (pick-wt=0): 9 [hyper,6,1,2,8] $F.

-----> EMPTY CLAUSE at   0.00 sec ----> 9 [hyper,6,1,2,8] $F.

Here, the last line says that falsity (represented as $F) was derived. Then, it proceeds to give the proof:

Length of proof is 1.  Level of proof is 1.

---------------- PROOF ----------------

1 [] President($c4).
2 [] Iraq($c3).
3 [] Visit($c2,$c4,$c3).
6 [] -President(x1)| -Iraq(x2)| -Go(x3,x1,x2).
7 [] -Visit(x4,x5,x6)|Go($f1(x4,x5,x6),x5,x6).
8 [hyper,3,7] Go($f1($c2,$c4,$c3),$c4,$c3).
9 [hyper,6,1,2,8] $F.

------------ end of proof -------------


Search stopped by max_proofs option.

============ end of search ============

That finishes the proof of the theorem.