Fight for a Snack: Solutions
Date: Fri, 28 Nov 2003
From: Vladimir Lifschitz
To: TAG
Appended at the end of this message are four solutions to the problem that
I sent you on October 3:
I have an apple, a banana and a carrot. My neighbor on the left
fights with me for the apple; maybe he will succeed in taking it
away from me, maybe he won't. After that, my neighbor on the right
fights with me for the banana. After these two events, who are
the possible owners of the apple, the banana and the carrot?
Represent this commonsense reasoning problem in an implemented
declarative language, and use the implementation to generate the
answer to the question above.
It is interesting to compare these representations.
The domain involves a nondeterministic action, and in the first two
solutions the effect of the action is expressed by disjunctive rules:
has(Fruit,Who,Time) v has(Fruit,me,Time) :- fight(Fruit,Who,Time) (1)
in the language of dlv, and
h(has(Person1, Fruit), T + 1) | h(has(Person2, Fruit), T + 1)
:- o(fightFor(Person1, Person2, Fruit), T) (2)
in the language of lparse/smodels. In (1), disjunction is understood as
in the answer set semantics for disjunctive programs. In (2), disjunction
can be understood in the same way, with the additional constraint that
makes it "exclusive." Generally,
p | q <- r
in the language of lparse corresponds to the combination
p v q <- r
<- p, q, r
in the language of dlv.
Solution 3 describes the effect of the action using the "may cause"
construct of CCalc:
fightFor(N,S) may cause owner(S)=N.
The logic programming countepart of this proposition is
owner(S,N,T+1) <- fightFor(N,S,T), not -owner(S,N,T+1). (3)
Since the fluent "owner" is declared as inertial, the logic program
corresponding to this solution contains also the rule
-owner(S,N,T+1) <- -owner(S,N,T), not owner(S,N,T+1). (3')
Interaction between rules (3) and (3') creates the mutiplicity of answer
sets similar to what is achieved in the first two solutions using
disjunctive rules.
Solution 4, in the langauge of CCalc also, is different from the others
in that it represents nondeterminism by replacing the fluent "owner"
with the fluent "possible_owner", and does not involve multiple models.
The CCalc proposition
caused possible_owner(P,S)
after fight(P,P1,S) && possible_owner(P1,S)
in that solution corresponds to
possible_owner(P,S,T+1) <- fight(P,P1,S,T), possible_owner(P1,S,T)
in logic programming. The logic program corresponding to Solution 4 has a
unique answer set.
Any comments?
Regards,
Vladimir
=========================================================================
*******************
* Solution 1: dlv
* by Gerald Pfeifer
*******************
has(apple ,me,1).
has(banana,me,1).
has(carrot,me,1).
fight(apple ,left ,2).
fight(banana,right,3).
#maxint=3.
%%%%%%%% Reasoning: (a) fighting, (b) inertia
has(Fruit,Who,Time) v has(Fruit,me,Time) :- fight(Fruit,Who,Time).
has(Fruit,Who,NextTime) :- has(Fruit,Who,Time),
not disputed(Fruit,NextTime), #succ(Time,NextTime).
disputed(Fruit,Time) :- fight(Fruit,_,Time).
%%%%%%%% Output
finally(Fruit,Who) :- has(Fruit,Who,#maxint).
*********************
* Solution 2: smodels
* by Gregory Gelfond
*********************
time(0..2).
person(me; left_neighbor; right_neighbor).
fruit(banana; apple; carrot).
inertialFluent(has(Person, Fruit)).
#domain person(Person; Person1; Person2).
#domain fruit(Fruit).
#domain time(T).
#domain inertialFluent(Fluent).
%% If two people fight for a piece of fruit, then one of them ends
%% up having possession of it.
h(has(Person1, Fruit), T + 1) | h(has(Person2, Fruit), T + 1)
:- o(fightFor(Person1, Person2, Fruit), T).
%% Executability Constraints
%% Two people cannot fight for a piece of fruit if neither of them has
%% it to begin with.
:- o(fightFor(Person1, Person2, Fruit), T), -h(has(Person1, Fruit), T),
-h(has(Person2, Fruit), T).
%% State Constraints
%% Two people cannot have the same fruit at the same time.
-h(has(Person1, Fruit), T) :- h(has(Person2, Fruit), T),
neq(Person1, Person2).
%% Inertia Axiom
h(Fluent, T + 1) :- h(Fluent, T), not -h(Fluent, T + 1).
-h(Fluent, T + 1) :- -h(Fluent, T), not h(Fluent, T + 1).
%% Initial Situation
h(has(me, banana), 0).
h(has(me, apple), 0).
h(has(me, carrot), 0).
%% From the problem description, we have the following series of events
o(fightFor(left_neighbor, me, apple), 0).
o(fightFor(right_neighbor, me, banana), 1).
%% SModels Directives
has(Person, Fruit, T) :- h(has(Person, Fruit), T).
hide.
show has(X, Y, Z).
*******************
* Solution 3: CCalc
* by Joohung Lee
*******************
:- sorts
snack;
person >> neighbor.
:- objects
apple, banana, carrot :: snack;
i :: person;
left, right :: neighbor.
:- variables
S :: snack;
N :: neighbor.
:- constants
owner(snack) :: inertialFluent(person);
fightFor(neighbor,snack) :: exogenousAction.
fightFor(N,S) may cause owner(S)=N.
nonexecutable fightFor(N,S) if owner(S)\=i.
:- nmquery
maxstep :: 2;
anyFluentValues;
cwaActions;
constraint 0: owner(S)=i;
0: fightFor(left,apple);
1: fightFor(right,banana).
*******************
* Solution 4: CCalc
* by Selim Erdogan
*******************
:- sorts
snack;
person.
:- variables
S :: snack;
P, P1 :: person.
:- constants
possible_owner(person,snack) :: inertialFluent;
fight(person,person,snack) :: exogenousAction.
caused possible_owner(P,S)
after fight(P,P1,S) && possible_owner(P1,S).
% one can't fight oneself
nonexecutable fight(P,P,S).
:- objects
left, me, right :: person;
apple, carrot, banana :: snack.
:- nmquery
label :: 1;
maxstep :: 2;
anyFluentValues;
cwaActions;
constraint 0:
[/\S | possible_owner(me,S)],
[/\S | -possible_owner(left,S)],
[/\S | -possible_owner(right,S)];
0: fight(left, me, apple);
1: fight(right, me, banana).