“Schubert’s Steamroller” was an unsurmountable problem for the 1978 Markgraf Karl Resolution Theorem Prover (The Markgraf Karl Refutation Procedure, 1981), but today is only of interest as an exercise in modeling a problem expressed in human language in some formalism.
So I have tried to do that. Paper from 1985:
- A Mechanical Solution to Schubert’s Steamroller by Many-Sorted Resolution (Typewriter-written paper, 1984)
- A Mechanical Solution to Schubert’s Steamroller by Many-Sorted Resolution (Typeset paper, 1985)
The original problem modeled as an AND-OR set of literals has some interesting aspects:
- Integrity constraints (“conjunction => false”). It took me some time to figure out how to get them into a Prolog program. In the end I added
\+ integrity_constraint_fails(...)at the end of the clauses. - Non-Horn clauses (head with disjunction).
- An apparent XOR in the description which is modelled by an OR.
- Misses the transitive relationship of “much_smaller_than/2” … it really isn’t in there. What happened?
- Does some peculiar modeling with function symbols concerning grain-eating animals which I don’t get and which is pointless anyway because the whole universe only has one grain:
g. - Has a wrongly transcribed clause in the typeset version.
Here we go:
:- discontiguous likes_to_eat/2.
:- discontiguous must_not_occur/0.
:- discontiguous dislikes_to_eat/2.
% ----------------------------------------------------------------------
% From: AAAI-84 Proceedings. Copyright 1984 AAAI. p 330 ff.
% "A MECHANICAL SOLUTION OF SCHUBERT'S STEAMROLLER BY MANY-SORTED RESOLUTION"
% Christoph Walther, Institut für Informatik I, Universität Karlsruhe
%
% "In the fall of 1978 L. Schubert spend his sabbatical at the University of Karlsruhe
% and a first-order axiomatization of his Problem was given to the Markgraf Karl
% Refutation Procedure (MKRP), a resolution-based automated theorem prover
% under development at the University of Karlsruhe. The system generated
% the clause set of figure 1.1, but failed to find a refutation."
%
% "Wolves, foxes, birds, caterpillars and snails are animals, and there are
% some of each of them. Also, there are some grains and grains are plants.
% Every animal either likes to eat all plants or (likes to eat) all animals
% much smaller than itself that like to eat some plants. Caterpillars and
% snails are much smaller than foxes which in turn are much smaller than wolves.
% Wolves do not like to eat foxes or grains while birds like to eat
% caterpillars but not snails. Caterpillar and snails like to eat some plants.
% Therefore there is an animal that likes to eat a grain-eating animal."
%
% Figure 1.1
%
% Using the following predicates as an abbreviation:
%
% A(x) - x is an animal W(x) - x is a wolf
% F(x) - x is a fox B(x) - x is a bird
% C(x) - x is a caterpillar S(x) - x is a snail
% G(x) - x is a grain P(x) - x is a plant
% M(xy) - x is much smaller than y
% E(xy) - x likes to eat y
%
% we obtain the following set of clauses as a predicate logic formulation
% of the problem [the commas are ORs, ed.]
%
% (1) {W(w)} (2) {F(f)}
% (3) {B(b)} (4) {C(c)}
% (5) {S(s)} (6) {G(g)}
% (7) {~W(x1),A(x1)} (8) {~F(x1),A(x1)}
% (9) {~B(x1),A(x1)} (10) {~C(x1),A(x1)}
% (11) {~S(x1),A(x1)} (12) {~G(x1),P(x1)}
% (13) {~A(x1),~P(x2),~A(x3),~P(x4),E(x1 x2),~M(x3 x1),~E(x3 x4),E(x1 x3)}
% (14) {~C(x1),~B(x2),M(x1 x2)} (15) {~S(X1),~B(x2),M(x1 x2}
% (16) {~B(x1),~F(x2),M(x1 x2)} (17) {~F(x1),~W(x2),M(x1 x2)}
% (18) {~F(x1),~W(x2),~E(x2 x1)} (19) {~G(x1),~W(x2),~E(x2 x1)}
% (20) {~B(x1),~C(x2),E(x1 x2)} (21) {~B(x1),~S(x2),~E(x1 x2)}
% (22) {~C(x1),P(h(x1))} (23) {~C(x1),Ex1 h(x1))} (22 is wrong in reprint)
% (24) {~S(x1),P(i(x1))} (25) {~S(x1),E(x1 i(x1))}
% (26) {~A(x1),~A(x2),G(j(x1 x2))}
% (27) {~A(x1),~A(x2),~E(x1 x2),~E(x2 j(x1 x2))}
% ----------------------------------------------------------------------
% Part 1
% ------
% "Wolves, foxes, birds, caterpillars and snails are animals, and there are some of
% each of them."
% "Also, there are some grains and grains are plants."
% Skolemize the existence facts:
% ∃X:wolf(X) ~~~> wolf(w), where "w" is an atom standing for some wolf.
wolf(wolf).
fox(fox).
bird(bird).
caterpillar(caterpillar).
snail(snail).
grain(grain).
% Define the hierarchy of sorts
animal(X) :- wolf(X).
animal(X) :- fox(X).
animal(X) :- bird(X).
animal(X) :- caterpillar(X).
animal(X) :- snail(X).
plant(X) :- grain(X).
% Part 2
% ------
% "Every animal either likes to eat all plants ...."
%
% animal(A) -> (plant(Plant) -> likes_to_eat(A,Plant))
%
% transformed into
%
% animal(A) & plant(A) -> likes_to_eat(A,Plant)
%
% We add "unless there are exceptions" using NAF because that
% seems to be a good way to cover the integrity constraints further below.
likes_to_eat(A,Plant) :-
animal(A),plant(Plant),
\+dislikes_to_eat(A,Plant).
% "...or (likes to eat) all animals much smaller than itself that like to eat some plants"
% We add "unless there are exceptions" using NAF.
likes_to_eat(A,Prey) :-
animal(A),animal(Prey),plant(Plant),
much_smaller(Prey,A),likes_to_eat(Prey,Plant),
\+dislikes_to_eat(A,Prey).
% In the paper, everything is in a single rule, with a disjunction in the consequent.
%
% A(x1) & P(x2) & A(x3) & P(x4) & M(x3,x1) & E(x3,x4) => E(x1,x2) | E(x1,X3).
%
% That is not a Horn clause! Also, the "either ... or" indicates an exclusive OR,
% but in the paper (and here) we have an inclusive OR. Is this really right?
% Part 3
% ------
% "Caterpillars and snails are much smaller than foxes which in turn are much
% smaller than wolves"
much_smaller_direct(X,Y) :- caterpillar(X),bird(Y),!.
much_smaller_direct(X,Y) :- snail(X),bird(Y),!.
much_smaller_direct(X,Y) :- bird(X),fox(Y),!.
much_smaller_direct(X,Y) :- fox(X),wolf(Y),!.
% The paper's formalization seems to miss the transitive relationship completely.
% What happened there? Without that, wolves eat nothing. We add it:
much_smaller(X,Y) :- much_smaller_direct(X,Y).
much_smaller(X,Y) :- much_smaller_direct(X,Z),much_smaller(Z,Y).
% Part 4
% ------
% "Wolves do not like to eat foxes or grains"
%
% These are not clauses, but integrity constraints. In the paper, they are actually
% given as:
%
% F(x1),W(x2),E(x2x1) => false.
% G(x1),W(x2),E(x2x1) => false.
%
% They actually say something about the exceptions to "likes_to_eat" but
% one has to think a bit out of the box for that:
dislikes_to_eat(X,Y) :- wolf(X),fox(Y).
dislikes_to_eat(X,Y) :- wolf(X),grain(Y).
% Part 5
% ------
% "...while birds like to eat caterpillars but not snails". Similar to the above.
likes_to_eat(X,Y) :-
bird(X),caterpillar(Y),
\+dislikes_to_eat(X,Y).
dislikes_to_eat(X,Y) :- bird(X),snail(Y).
% Part 6
% ------
% "caterpillar and snails like to eat some plants"
%
% Really "there are plants such that caterpillar and snails like to eat those"
% or "Not for all plants, caterpillars or snails do not like them"
%
% In the paper, this employs a function symbol:
%
% C(x1) => P(h(x1)) % "h(x1) is a plant that is a function of caterpillar x1"
% C(x1) => E(x1 h(x1)) % "caterpillar x1 likes to eat h(x1)"
% S(x1) => P(i(x1) % "i(x1) is a plant that is a function of snail x1"
% S(x1) => E(x1 i(x1)) % "snail x1 likes to eat i(x1)"
%
% There is really not enough info to know what to do here. In fact, our
% whole universe has just one plant: P = grain. So what's the point?
likes_to_eat(X,P) :- caterpillar(X),plant(P),\+dislikes_to_eat(X,P).
likes_to_eat(X,P) :- snail(X),plant(P),\+dislikes_to_eat(X,P).
% Part 7
% ------
% "therefore there is an animal that likes to eat a grain-eating animal"
% (actually "...that likes to eat an animal that likes to eat grain")
%
% That's the query!
%
% The paper says:
%
% A(x1),A(x2) => G(j(x1x2)) % j(x1x2) is grain that depends on the animal pair. WEIRD! WEIRD! WEIRD!
% A(x1),A(x2),E(x1x2),E(x2j(x1x2)) => false % An integrity constraint that will make the program inconsistent
% Here is ours, we constructively search for the animal...
go(A) :- animal(A),animal(Prey),grain(G),likes_to_eat(A,Prey),likes_to_eat(Prey,G).
/* RUN IT ----------------------------
?- set_prolog_flag(answer_write_options,[max_depth(0)]).
true.
% Ready!
?- time(setof(A,go(A),L)).
% 2,443 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 6955913 Lips)
L = [bird, fox, wolf].
% Let's take a look at these...
?- setof([A,B],likes_to_eat(A,B),C).
C = [[bird,caterpillar],
[bird,grain],
[caterpillar,grain],
[fox,bird],
[fox,caterpillar],
[fox,grain],
[fox,snail],
[snail,grain],
[wolf,bird],
[wolf,caterpillar],
[wolf,snail]].
?- setof(X,likes_to_eat(wolf,X),L).
L = [bird, caterpillar, snail].
*/