% INTRO TO LOGIC PROGRAMMING AND AI
% Spring 1998
% //Selmer Bringsjord
%
% Selmer and Conrad are brothers.  One is richer than the
% other.  Given this (and some other facts), who has the
% bigger tractor?  This file shows customary use of Otter's
% $ANSWER mechanism, as well as the max_proofs option (two
% proofs are obtained here).

set(ur_res).
assign(max_proofs,2).

list(usable).

% The following clause expresses the fact that if x is a
% brother to y and is richer than y, then x has a bigger
% tractor than y.  (You should be able to instinctively
% do the conversion from
%
%         all x all y ((Brother(x,y) & Richer(x,y)) ->
%                        BiggerTractor(x,y)).
%
% to this clause.  If you can't review the algorithm in
% the text-in-progress.)

-Brother(x,y) | -Richer(x,y) | BiggerTractor(x,y).

% A financial fact:
Richer(conrad,selmer).

% Being a brother is a symmetric property:
-Brother(x,y) | Brother(y,x).

% A SIMPLE EXPERIMENT:  Put in the following fact, comment
% out this fact in the list(sos), and run Otter.  What
% happens?  Why?
% BiggerTractor(brian,conrad).

% Clause used to trigger Info predicate to give unit
% conflict:
-BiggerTractor(x,y) | Info(x,y).

end_of_list.

list(sos).
Brother(selmer,conrad).

BiggerTractor(brian,conrad).
end_of_list.

list(passive).
-Info(x,y) | $ANSWER(biggertractor(x,y)).
end_of_list.