             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).


