#option --totalize-negations --dlp --true-negation %% Palikkamaailman toteutus lauselogiikalla: instantiate-ohjelmaa varten %% laadittu esitys vastaavasta satplan-järjestelmän esityksestä %% %% Laatinut: Tomi Janhunen, 2005 %% %% Operaattorin MOVE(X,Y,Z,T) toteuttavat predikaatit: %% %% obj(X,T) -- palikka X on siirron kohteena ajanhetkellä T %% src(Y,T) -- siirto suoritaan palikan Y päältä ajanhetkellä T %% dst(Z,T) -- siirto suoritaan palikan Z päälle ajanhetkellä T %% %% Tilaa kuvaavat predikaatit: %% %% on(X,Y,T) -- palikka X on palikan Y päällä ajanhetkellä T %% clear(X,T) -- palikan X päällä ei ole mitään ajanhetkellä T %% %% ============================================================================ %% %% Käyttöesimerkkejä: %% %% instantiate -ct=3 bw.sat sussman.dat | gnt2 %% %% tai vaihtoehtoisesti: %% %% instantiate -ct=3 bw.sat sussman.dat | %% dimacs > dimacs_output_file %% zchaff dimacs_output_file > model_file %% intp dimacs_output < model_file %% %% ============================================================================ %% Määritellään muuttujille tyypit #type block(X). #type block(Y). #type block(Z). #type time(T). %% Operaattorien ja tilojen kuvaamiseen liittyvät predikaatit #action obj(_, _). #action src(_, _). #action dst(_, _). #state on(_, _, _). #state clear(_, _). time(0..t). %% Kätketään tietyt symbolit (suunnitelman lukeminen mallista helpottuu) #hide block(_). #hide movable(_). #hide time(_). #hide src(_, _). #hide on(_, _, _). #hide clear(_, _). %% Toiminnon aiheuttamat vaikutukset ovat voimassa suorittamisen jälkeen obj(X, T), movable(X), dst(Y, T), X != Y, time(T+1) -> on(X, Y, T+1). obj(X, T), movable(X), src(Y, T), X != Y, time(T+1) -> -on(X, Y, T+1). src(X, T), movable(X), time(T+1) -> clear(X, T+1). dst(X, T), movable(X), time(T+1) -> -clear(X, T+1). %% Toiminnon suorittaminen edellyttää esiehtojen voimassaoloja obj(X, T), movable(X), src(Y, T), X != Y, T < t -> on(X, Y, T). obj(X, T), movable(X), T < t -> clear(X, T). dst(X, T), movable(X), T < t -> clear(X, T). %% Kehysaksiomat (totena säilyvät predikaatti-instanssit) clear(X, T), movable(X), time(T+1) -> clear(X, T+1) | dst(X, T). on(X, Y, T), movable(X), X != Y, time(T+1) -> on(X, Y, T+1) | obj(X, T). %% Kehysaksiomat (epätotena säilyvät predikaatti-instanssit) -clear(X, T), movable(X), time(T+1) -> -clear(X, T+1) | src(X, T). -on(X, Y, T), movable(X), X != Y, time(T+1) -> -on(X, Y, T+1) | obj(X, T). -on(X, Y, T), movable(X), X != Y, time(T+1) -> -on(X, Y, T+1) | dst(Y, T). %% Jokaisella ajanhetkellä suoritetaan ainakin yksi toiminto %% %% HUOM! Käytämme muuttujaa V, jotta disjunktiosta tulee monijäseninen %% (muuttujan X käyttö V:n asemesta johtaisi väärään lopputulokseen) T < t -> { obj(V, T): movable(V) }. T < t -> { src(V, T): block(V) }. T < t -> { dst(V, T): block(V) }. %% Toiminnot sulkevat toinen toisensa pois obj(X, T), movable(X), X != Y, movable(Y), T < t -> -obj(Y, T). src(X, T), X != Y, T < t -> -src(Y, T). dst(X, T), X != Y, T < t -> -dst(Y, T). %% Toimintoon osalliset objektit ovat eriävät obj(X, T), movable(X), T < t -> -src(X, T). obj(X, T), movable(X), T < t -> -dst(X, T). src(X, T), movable(X), T < t -> -dst(X, T). %% on-predikaatin ominaisuudet: irrefleksiivisyys ja antisymmetria -on(X, X, T). on(X, Y, T), X != Y -> -on(Y, X, T). %% Päällekkäisyyteen liittyvä yksikäsitteisyys on(X, Y, T), movable(X), X != Y, movable(Y), X != Z, Y != Z, movable(Z) -> -on(Z, Y, T). on(X, Y, T), movable(X), X != Y, X != Z, Y != Z -> -on(X, Z, T). movable(X), movable(Y) -> -on(X,Y,T) | -clear(Y,T). -movable(X) -> -on(X,Y,T).