(define-class situation :axioms (forall (?a ?s) (not (= S_0 (do ?a ?s)))) (forall (?a1 ?a2 ?s1 ?s2) (=> (= (do ?a1 ?s1) (do ?a2 ?s2)) (= ?a1 ?a2))) (forall (?s) (not (< ?s S_0)) (forall (?a ?s1 ?s2) (<=> (< ?s1 (do ?a ?s2)) (and (Poss ?a ?s2) (leq ?s1 ?s2)))) (forall (?P) (=> (and (?P S_0) (forall (?s ?a) (=> (?P s) (?P (do ?a ?s))))) (forall (?s) (?P ?s)))) (define-class action :axioms (forall (?a ?s) (not (= S_0 (do ?a ?s)))) (forall (?a1 ?a2 ?s1 ?s2) (=> (= (do ?a1 ?s1) (do ?a2 ?s2)) (= ?a1 ?a2))) (forall (?s) (not (< ?s S_0)) (forall (?a ?s1 ?s2) (<=> (< ?s1 (do ?a ?s2)) (and (Poss ?a ?s2) (leq ?s1 ?s2)))) (forall (?P) (=> (and (?P S_0) (forall (?s ?a) (=> (?P s) (?P (do ?a ?s))))) (forall (?s) (?P ?s)))) (forall (?a) (exists (?f) (precondition ?f ?a)) (forall (?a) (exists (?f) (effects+ ?f ?a)) (forall (?a) (exists (?f) (effects- ?f ?a)) (define-class fluent (?f)) :axioms (forall (?f) (exists (?Phi) (successor-state ?Phi ?f)) (define-class domain-object (?x)) (define-relation < (?s1 ?s2)) ((Arity 2) (nth-domain 1 situation) (nth-domain 2 situation)) :axioms (forall (?a ?s) (not (= S_0 (do ?a ?s)))) (forall (?a1 ?a2 ?s1 ?s2) (=> (= (do ?a1 ?s1) (do ?a2 ?s2)) (= ?a1 ?a2))) (forall (?s) (not (< ?s S_0)) (forall (?a ?s1 ?s2) (<=> (< ?s1 (do ?a ?s2)) (and (Poss ?a ?s2) (leq ?s1 ?s2)))) (forall (?P) (=> (and (?P S_0) (forall (?s ?a) (=> (?P s) (?P (do ?a ?s))))) (forall (?s) (?P ?s)))) (define-relation leq (?s1 ?s2) ((Arity 2) (nth-domain 1 situation) (nth-domain 2 situation)) :def (or (< ?s1 ?s2) (= ?s1 ?s2))) (define-function do (?a ?s) ((Arity 2) (nth-domain 1 action) (nth-domain 2 situation) (range situation)) :axioms (forall (?a ?s) (not (= S_0 (do ?a ?s)))) (forall (?a1 ?a2 ?s1 ?s2) (=> (= (do ?a1 ?s1) (do ?a2 ?s2)) (= ?a1 ?a2))) (forall (?s) (not (< ?s S_0)) (forall (?a ?s1 ?s2) (<=> (< ?s1 (do ?a ?s2)) (and (Poss ?a ?s2) (leq ?s1 ?s2)))) (forall (?P) (=> (and (?P S_0) (forall (?s ?a) (=> (?P s) (?P (do ?a ?s))))) (forall (?s) (?P ?s)))) (define-relation holds (?f ?s) ((Arity 2) (nth-domain 1 fluent) (nth-domain 2 situation)) (define-relation Poss (?a ?s) ((Arity 2) (nth-domain 1 action) (nth-domain 2 situation)) :axioms (forall (?a ?s1 ?s2) (<=> (< ?s1 (do ?a ?s2)) (and (Poss ?a ?s2) (leq ?s1 ?s2))))