Tammet – 21. mai 2009, kell 22:46

2009-05-21T22:46:05Z

Uus lehekülg

First, a simple version.

<pre>

%set(auto).
set(factor).
set(binary_res).

%clear(print_kept).

set(prolog_style_variables).

list(sos).
%formulas(sos).

% ----- initial situation ------

holds(on(a,table),s0).

holds(on(b,table),s0).

holds(on(c,d),s0).

holds(on(d,table),s0).

holds(clear(a),s0).

holds(clear(b),s0).

holds(clear(c),s0).

holds(empty,s0).

holds(clear(table),State).

% ---- difference of objects -----

differ(X,Y)
| -differ(Y,X).

differ(a,b).

differ(a,c).

differ(a,d).

differ(a,table).

differ(b,c).

differ(b,d).

differ(b,table).

differ(c,d).

differ(c,table).

differ(d,table).

% ---- rules -----

%holds(and(X,Y),State)
% | -holds(X,State)
% | -holds(Y,State).

% pickup rules

holds(holding(X),do(pickup(X),State))
| -holds(empty,State)
| -holds(clear(X),State)
| -differ(X,table).

holds(clear(Y),do(pickup(X),State))
| -holds(on(X,Y),State)
| -holds(clear(X),State)
| -holds(empty,State).

% frame axioms for pickup

holds(on(X,Y),do(pickup(Z),State))
| -holds(on(X,Y),State)
| -differ(X,Z).

holds(clear(X),do(pickup(Z),State))
| -holds(clear(X),State)
| -differ(X,Z).

% putdown rules

holds(empty,do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).

holds(on(X,Y),do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).

holds(clear(X),do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).

% frame axioms for putdown

holds(on(X,Y),do(putdown(Z,W),State))
| -holds(on(X,Y),State).

holds(clear(Z),do(putdown(X,Y),State))
| -holds(clear(Z),State)
| -differ(Z,Y).

% ----- query -------

end_of_list.

list(usable).

-holds(on(b,a),State) | -holds(on(c,b),State).

%-holds(and(on(c,b),on(b,a)),State).

end_of_list.

</pre>

Second, a lot more complex version (not necessarily better!)

<pre>
% this is the way comments start
%set(hyper_res). % another alternative is set(binary_res)
%set(factor). % probably comes automatically
%set(para_from).
%set(para_into).
set(auto).
clear(print_kept). % this will print out ALL derived and kept stuff

%formula_list(sos). % use list(sos) if not formula syntax
formulas(sos).

on(b,table,s0).
on(a,table,s0).
on(c,table,s0).
empty(s0).
all x hasspace(table,x).

-on(b,a,s0).
-on(a,b,s0).
-on(c,b,s0).
-on(c,a,s0).
-on(a,c,s0).
-on(b,c,s0).
all x all y -on(table,x,y).

block(a).
block(b).
block(c).
-block(table).

% being clear: closed world

all z ((-on(b,a,z) & -on(c,a,z)) -> clear(a,z)).
all z ((-on(a,b,z) & -on(c,b,z)) -> clear(b,z)).
all z ((-on(a,c,z) & -on(b,c,z)) -> clear(c,z)).

% general world rules

all x all y (clear(x,y) -> hasspace(x,y)).

all x all y all z
((on(x,y,z) & block(y))
->
-on(x,table,z)).

all x all z
( -(exists y on(y,x,z))
->
clear(x,z)).

% closed world

%all x (x=a | x=b | x=c | x=table).
%a!=b.
%a!=c.
%a!=table.
%b!=c.
%b!=table.
%c!=table.

all x (sameas(x,a) | sameas(x,b) | sameas(x,c) | sameas(x,table)).
-sameas(a,b).
-sameas(a,c).
-sameas(a,table).
-sameas(b,c).
-sameas(b,table).
-sameas(c,table).

all x sameas(x,x).
all x all y (sameas(x,y) -> sameas(y,x)).
%all x all y all z (sameas(x,y) & sameas(y,z) -> sameas(x,z)).

% actions

all x all y all z
((holds(x,z) &
hasspace(y,z) &
-sameas(x,y) )
->
(on(x,y,puton(x,y,z)) &
-clear(y,puton(x,y,z)) &
clear(x,puton(x,y,z)) &
hasspace(x,puton(x,y,z)) &
empty(puton(x,y,z))) ).

all x all y all z
((on(x,y,z) &
empty(z) &
clear(x,z))
->
(-on(x,y,lift(x,z)) &
clear(y,lift(x,z)) &
hasspace(y,lift(x,z)) &
holds(x,lift(x,z))) ).

% frame axioms

all x all y all z
(-on(x,y,z)
->
-on(x,y,lift(x,z)) ).

all x all y all z all u
((on(x,y,z) & -sameas(u,x))
->
on(x,y,lift(u,z)) ).

all x all y all z
((clear(x,z) & -sameas(x,y))
->
clear(x,lift(y,z)) ).

all x all y all z
((-clear(x,z) & -on(y,x))
->
-clear(x,lift(y,z)) ).

%

all x all y all z all u
(-on(x,y,z)
->
-on(x,y,puton(x,z)) ).

all x all y all z all u
((on(x,y,z) & -sameas(u,x))
->
on(x,y,lift(u,z)) ).

all x all y all z all u
((clear(x,z) & -sameas(x,y))
->
clear(x,puton(u,y,z)) ).

all x all y all z all u
((-clear(x,z) & -sameas(u,x))
->
-clear(x,puton(u,y,z)) ).

% queries

all z ((on(c,a,z) & on(b,c,z)) -> $answer(z)).
%all z (on(b,c,z) -> $answer(z)).
%all z (on(c,a,z) -> $answer(z)).
%all z (clear(a,z) -> $answer(z)).

end_of_list.

</pre>

Blocks world axiom/query examples from lecture - Redigeerimiste ajalugu

Tammet – 21. mai 2009, kell 22:46