Discrete States

Extension Name: disc_state.th

Primitive Lexicon:

Relations:

(state ?f)
(holds ?f ?occcc)
(prior ?f ?occcc)

Defined Lexicon: none

Theories Required by this Extension: occtree.th, psl_core.th

Definitional Extensions Required by this Extension: None

Axioms

Axiom 1 States are objects.

(forall (?f)
	(if	(state ?f)
		(object ?f)))

Axiom 2 The holds relation is only between states and arboreal ctivity occurrences. Intuitively, it means that the fluent (property of the world) is true after the activity occurrence ?occ.

(forall (?f ?occ)
	(if	(holds ?f ?occ)
		(and	(state ?f)
			(arboreal ?occ))))

Axiom 3 The prior relation is only between states and arboreal activity occurrences. Intuitively, it means that the fluent (property of the world) is true before the activity occurrence ?occ.

(forall (?f ?occ)
	(if	(prior ?f ?occ)
		(and	(state ?f)
			(arboreal ?occ))))

Axiom 4 All initial occurrences agree on the states that hold prior to them.

(forall (?occ1 ?occ2 ?f)
	(if	(and	(initial ?occ1)
			(initial ?occ2))
		(iff	(prior ?f ?occ1)
			(prior ?f ?occ2))))

Axiom 5 A state holds after an arboreal activity occurrence if and only if it holds prior to the successor occurrence.

(forall (?f ?a ?occ)
        (iff    (prior ?f (successor ?a ?occ))
                (and    (holds ?f ?occ)
                        (generator ?a))))

Axiom 6 If a fluent holds after some activity occurrence, then there exists an earliest activity occurrence along the branch where the fluent holds.

(forall (?occ1 ?f)
	(if	(holds ?f ?occ1)
		(exists (?occ2)
			(and	(earlierEq ?occ2 ?occ1)
				(holds ?f ?occ2)
				(or	(initial ?occ2)
					(not (prior ?f ?occ2)))
				(forall (?occ3)
					(if	(and	(earlier ?occ2 ?occ3)
							(earlier ?occ3 ?occ1))
						(holds ?f ?occ3)))))))

Axiom 7 If a fluent does not hold after some activity occurrence, then there exists an earliest activity occurrence along the branch where the fluent does not hold.

(forall (?occ1 ?f)
	(if	(and	(state ?f)
			(arboreal ?occ1)
			(not (holds ?f ?occ1)))
		(exists (?occ2)
			(and	(earlierEq ?occ2 ?occ1)
				(not (holds ?f ?occ2))
				(or	(initial ?occ2)
					(prior ?f ?occ2))
				(not (exists (?occ3)
					(and	(earlier ?occ2 ?occ3)
						(earlier ?occ3 ?occ1)
						(holds ?f ?occ3))))))))

Axiom 8 If a fluent holds, there exists an earliest activity occurrence where it holds.

(forall (?f ?s1)
	(if	(holds ?f ?s1)
		(exists (?s2)
			(and	(holds ?f ?s2)
				(earlierEq ?s2 ?s1)
				(forall (?s3)
					(if	(holds ?f ?s3)
						(not (earlier ?s3 ?s2))))))))