Fluent Trees

Extension Name: achieve.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: None

Definitions

Definition 1 A fluent ?f is achieved by an occurrence ?occ iff it does not hold before the occurrence, but it does hold after the occurrence.

(forall (?f ?occ) (iff (achieved ?f ?occ)
(and    (holds ?f ?occ)
        (not (prior ?f ?occ)))))

Definition 2 A fluent ?f is falsified by an occurrence ?occ iff it holds in before the occurrence but it does not hold after the occurrence.

(forall (?f ?occ) (iff (falsified ?f ?occ)
(and    (not (holds ?f ?occ))
        (prior ?f ?occ))))

Definition 3 A fluent is irreversible iff it is never falsified.

(forall (?f) (iff (irreversible ?f)
(not (exists (?occ)
	(falsified ?f ?occ)))))

Definition 4 A fluent is unachievable iff it is never achieved.

(forall (?f) (iff (unachievable ?f)
(not (exists (?occ)
	(achieved ?f ?occ)))))

Definition 5

(forall (?f) (iff (bounded ?f)
(exists (?occ1 ?occ2)
	(and	(achieved ?f ?occ1)
		(falsified ?f ?occ2)))))