(define-class time :axioms (forall (?s ?a) (= (end ?s ?a) (start (do ?a ?s)))) (forall (?a ?s) (< (start ?s) (end ?s ?a))) (start S_0 0) (define-function start (?s) ((Arity 1) (nth-domain 1 situation) (range time) :axioms (forall (?s ?a) (= (end ?s ?a) (start (do ?a ?s)))) (forall (?a ?s) (< (start ?s) (end ?s ?a))) (start S_0 0) (define-function end (?s ?a) ((Arity 2) (nth-domain 1 situation) (nth-domain 2 action) (range time) :axioms (forall (?s ?a) (= (end ?s ?a) (start (do ?a ?s)))) (forall (?a ?s) (< (start ?s) (end ?s ?a))) (start S_0 0) (define-relation branch (?s ?b) ((Arity 2) (nth-domain 1 situation) (nth-domain 2 branch)) :axioms (forall (?b) (branch S_0 ?b)) (forall (?a ?s ?b) (=> (branch (do ?a ?s) ?b) (and (branch ?s ?b) (poss ?a ?s)))) (forall (?a ?a' ?s ?b) (=> (and (branch (do ?a ?s) ?b) (branch (do ?a' ?s) ?b)) (= ?a ?a'))) (define-relation actual (?s) ((Arity 1) (nth-domain 1 situation)) :axioms (actual S_0) (forall (?a ?s) (=> (actual (do ?a ?s)) (and (actual ?s) (Poss ?a ?s)))) (forall (?a1 ?a2 ?s) (=> (and (actual (do ?a1 ?s)) (actual (do ?a2 ?s))) (= ?a1 ?a2))) (define-relation leq_f (?s ?sp) ((Arity 2) (nth-domain 1 situation) (nth-domain 2 situation)) :axioms (forall (?a ?s ?sp) (<=> (leq_f ?s (do ?a ?sp)) (and (allowed ?a ?sp) (leq_f ?s ?sp))) (forall (?s) (not (leq_f ?s S_0))) (forall (?s ?sp) (=> (leq_f ?s ?sp) (leq ?s ?sp))) (define-relation feasible (?s) ((Arity 1) (nth-domain 1 situation) :axioms (forall (?s) (<=> (feasible ?s) (leq_f S_0 ?s))) (forall (?s) (=> (actual ?s) (feasible ?s))) (define-relation feasible_branch (?b) ((Arity 1) (nth-domain 1 situation) :def (forall (?s) (=> (branch ?s ?b) (feasible ?s))) (define-relation holdsT (?f ?t) ((Arity 2) (nth-domain 1 fluent) (nth-domain 2 time)) :def (exists (?s) (and (actual ?s) (< (start ?s) ?t) (holds ?f ?s))) (define-relation PossT (?a ?t) ((Arity 2) (nth-domain 1 action) (nth-domain 2 time)) :def (exists (?s) (and (Poss ?a ?s) (= (start (do ?a ?s)) ?t))) (define-relation during_situation (?t ?s) ((Arity 2) (nth-domain 1 time) (nth-domain 2 situation)) :def (forall (?a) (=> (actual (do ?a ?s)) (leq ?t (end ?s ?a))))