Subactivities

Theory of Subactivities

Extension Name: subactivity.th

Primitive Lexicon:

Relations:

Defined Lexicon:

Relations:

Theories Required by this Extension: psl_core.th

Definitional Extensions Required by this Extension: None

Axioms

Axiom 1 subactivity is a relation over activities 
(forall (?a1 ?a2)
	(if	(subactivity ?a1 ?a2)
		(and	(activity ?a1)
			(activity ?a2))))
Axiom 2 The subactivity relation is reflexive. 
(forall (?a)
	(if	(activity ?a)
		(subactivity ?a ?a)))
Axiom 3 The subactivity relation is antisymmetric. 
(forall (?a1 ?a2)
	(if	(and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a1))
		(= ?a1 ?a2)))
Axiom 4 The subactivity relation is transitive. 
(forall (?a1 ?a2 ?a3)
	(if	(and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a3))
		(subactivity ?a1 ?a3)))
Axiom 5 The subactivity relation is a discrete ordering, so every activity has an upwards successor in the ordering. 
(forall (?a1 ?a2)
	(if	(and	(subactivity ?a1 ?a2)
			(not (= ?a1 ?a2)))
		(exists (?a3)
			(and	(subactivity ?a1 ?a3)
				(subactivity ?a3 ?a2)
				(not (= ?a3 ?a1))
				(forall (?a4)
					(if	(and	(subactivity ?a1 ?a4)
							(subactivity ?a4 ?a3))
						(or	(= ?a4 ?a1)
							(= ?a4 ?a3))))))))
Axiom 6 The subactivity relation is a discrete ordering, so every activity has a downwards successor in the ordering. 
(forall (?a1 ?a2)
	(if	(and	(subactivity ?a1 ?a2)
			(not (= ?a1 ?a2)))
		(exists (?a3)
			(and	(subactivity ?a1 ?a3)
				(subactivity ?a3 ?a2)
				(not (= ?a3 ?a2))
				(forall (?a4)
					(if	(and	(subactivity ?a3 ?a4)
							(subactivity ?a4 ?a2))
						(or	(= ?a4 ?a2)
							(= ?a4 ?a3))))))))

Definitions

Definition 1 An activity is primitive iff it has no proper subactivities. 
(forall (?a) (iff (primitive ?a)
(and    (activity ?a)
	(forall (?a1)
		(if	(subactivity ?a1 ?a)
			(= ?a1 ?a))))))