\begin{verbatim}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
const length=6.
time(1..length).
%%%%%%%%%%%%%%%%%%%A simple domain%%%%%%%%%%%%%%%%%%%%%%%%%%%
action(a).
action(b).
action(c).
action(null).
fluent(f).
fluent(g).
causes(a, f, set1).
set(set1).
in(neg(g), set1).
causes(b, neg(g), set2).
set(set2).
causes(c, neg(f), set2).
exec(a, set2).
exec(b, set2).
exec(c, set2).
exec(null, set2).
%%%%%%%%%%%%%%%%%%%%A very simple domain%%%%%%%%%%%%%%%%%%%%
action(d).
action(e).
fluent(h).
exec(d, set1).
exec(e, set2).
causes(d, h, set2).
causes(e, neg(g), set2).
procedure(test2).
first(test2, ch1).
last(test2, null).
choice_st(ch1).
in(d, ch1).
in(e, ch1).
%%%%%%%%%%%%%%%%%%%%Intitially %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
initially(neg(f)).
initially(g).
%%%%%%%%%%%%%%%%%%%% A simple Golog program %%%%%%%%%%%%%%%%
procedure(test).
first(test, b).
last(test, rest1).
procedure(rest1).
first(rest1, choice).
last(rest1, rest2).
choice_st(choice).
in(a, choice).
in(c, choice).
procedure(rest2).
first(rest2, rest3).
last(rest2, null).
formula(rest3).
set(rest3).
in(set3, rest3).
set(set3).
in(f, set3).
%%%%%%%%%%%%%%A dumb Golog program %%%%%%%%%%%%%%%%%%
procedure(test5).
first(test5, a).
last(test5, null).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
goal(T) :- time(T),
% holds(f, T).
unfold(test, 1, T).
goal(T+1) :-
time(T),
T < length,
goal(T).
exists_plan :-
goal(length).
:- not exists_plan.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
literal(G) :-
fluent(G).
literal(neg(G)) :-
fluent(G).
contrary(F, neg(F)) :-
fluent(F).
contrary(neg(F), F) :-
fluent(F).
def_literal(G) :-
def_fluent(G).
def_literal(neg(G)) :-
def_fluent(G).
contrary(F, neg(F)) :-
def_fluent(F).
contrary(neg(F), F) :-
def_fluent(F).
leq(T,T):- time(T).
leq(Tb,Te):- time(Tb), time(Te), Tb < Te.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
not_holds_set(S, T) :-
set(S),
time(T),
in(L,S),
not holds(L,T).
holds_set(S, T) :-
set(S),
time(T),
not not_holds_set(S,T).
holds(F, 1) :-
literal(F),
initially(F).
holds(F, T+1) :-
literal(F),
time(T),
set(S),
T < length,
action(A),
executable(A,T),
occurs(A,T),
causes(A,F,S),
holds_set(S,T).
holds(F, T) :-
literal(F),
literal(G),
time(T),
T < length,
holds(G, T),
static_causes(G,F).
holds(F, T+1) :-
literal(F),
literal(G),
contrary(F,G),
time(T),
T < length,
holds(F,T),
not holds(G, T+1).
executable(A,T) :-
action(A),
time(T),
set(S),
T < length,
exec(A,S),
holds_set(S,T).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
possible(A,T) :-
action(A),
time(T),
executable(A,T),
not goal(T).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
occurs(A,T) :-
action(A),
time(T),
possible(A,T),
not not_occurs(A,T).
not_occurs(A,T) :-
action(A),
action(AA),
time(T),
occurs(AA,T),
neq(A,AA).
%%%%%%%%%%%%%%% Global truths and constraints %%%%%%%%%%%%
holds(true, T):- time(T).
:- time(T), occurs(null,T).
%%%%%%%%%%%%%%%%%%%% Unfolding %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
unfold(P,Tb,Te):-
time(Tb),
time(Te),
leq(Tb,Te),
time(Te1),
leq(Tb, Te1),
leq(Te1,Te),
procedure(P),
first(P,P1),
unfold(P1,Tb,Te1),
last(P,P2),
unfold(P2,Te1,Te).
unfold(A,Tb,Tb+1):-
time(Tb),
action(A),
neq(A, null),
occurs(A,Tb).
unfold(A,Tb,Tb):-
time(Tb),
action(A),
A = null.
unfold(N,Tb,Te):-
time(Tb),
time(Te),
leq(Tb,Te),
choice_st(N),
in(P1,N),
unfold(P1,Tb,Te).
unfold(F,Tb,Tb):-
time(Tb),
formula(F),
holds_formula(F,Tb).
unfold(F,Tb,Tb):-
time(Tb),
literal(F),
holds(F,Tb).
unfold(I,Tb,Te):-
time(Tb),
time(Te),
leq(Tb,Te),
if(I,F,P1,P2),
holds_formula(F,Tb),
unfold(P1,Tb,Te).
unfold(I,Tb,Te):-
time(Tb),
time(Te),
leq(Tb,Te),
if(I,F,P1,P2),
not_holds_formula(F,Tb),
unfold(P2,Tb,Te).
unfold(W,Tb,Te):-
time(Tb),
time(Te),
leq(Tb,Te),
while(W,F,P),
holds_formula(F,Tb),
time(Te1),
leq(Tb, Te1),
leq(Te1,Te),
unfold(P,Tb,Te1),
unfold(W,Te1,Te).
unfold(W,Tb,Tb):-
time(Tb),
while(W,F,P),
not_holds_formula(F,Tb).
unfold(S,Tb, Te) :-
time(Tb),
time(Te),
leq(Tb,Te),
choice_arg(S,F,P),
holds(F,Tb),
unfold(P, Tb, Te).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% computing the truth value of fluent formula
% a formula F in DNF
% can be represented by a set S1,...,Sn of sets of literals.
holds_formula(F, T):-
time(T),
formula(F),
in(S, F),
holds_set(S,T).
not_holds_formula(F, T):-
time(T),
formula(F),
not holds_formula(F, T).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
hide time(T).
hide action(A).
hide causes(A,F,L).
hide initially(F).
hide contrary(F,G).
hide fluent(F).
hide literal(L).
hide not_occurs(A,T).
hide possible(A,T).
hide exists_plan.
hide finally(X).
hide goal(T).
hide not_goal(T).
hide static_causes(X,Y).
hide def_fluent(X).
hide def_literal(X).
hide unfold(P,T1,T2).
hide first(P,P1).
hide last(P,P2).
hide procedure(P).
hide choice_st(P).
hide if(I,P,P1,P2).
hide while(W,F,P).
hide holds_formula(C,T).
hide not_holds_formula(C, T).
hide formula(C).
hide set(S).
hide in(F,S).
hide holds_set(S, T).
hide not_holds_set(S,T).
hide leq(T1,T2).
hide executable(A, T).
hide holds(F, T).
hide exec(A,L).
hide choice_arg(X,Y,Z).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{verbatim}