\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}