Appendix A: PSL in SWSL

This is Appendix A of the Semantic Web Services Ontology (SWSO) document.

Here we give the SWSL-FOL and SWSL-Rules formulations of selected theories of the Process Specification Language (PSL), including PSL core and five theories from the outer core. (These are the theories upon which SWSO builds.) Each of these theories is given in its entirety.

The original PSL declarations and axioms, expressed in KIF, are retained here, precisely as given on the PSL Web site. For each axiom of PSL, we give an equivalent axiom expressed in SWSL-FOL, and a (possibly weakened) set of rules expressed in SWSL-Rules. The SWSL-Rules axiomatizations were derived according to the translation approach described in Section 3 of the SWSL document.

  A.1 PSL Core
  A.2 Subactivity Theory
  A.3 Theory of Occurrence Trees
  A.4 Theory of Discrete States
  A.5 Theory of Atomic Activities
  A.6 Theory of Complex Activities


A.1 PSL Core

Extension Name: psl_core.th
Theories Required by this Extension: None
Definitional Extensions Required by this Extension: None

Primitive Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules Functions:

KIF SWSL-FOL and SWSL-Rules Constants:

KIF SWSL-FOL and SWSL-Rules

Defined Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules

Axioms

Axiom 1 The before relation only holds between timepoints.

KIF
(forall (?t1 ?t2)
	(implies  (before ?t1 ?t2)
    		  (and 	(timepoint ?t1) 
			(timepoint ?t2))))
SWSL-FOL
forall ?t1 ?t2
  ( before(?t1, ?t2) ==> timepoint(?t1) and timepoint(?t2) ).
SWSL-Rules
neg before(?t1, ?t2) :- neg timepoint(?t1).
timepoint(?t1) :- before(?t1, ?t2).
 
neg before(?t1, ?t2) :- neg timepoint(?t2).
timepoint(?t2) :- before(?t1, ?t2).
Axiom 2 The before relation is a total ordering.

KIF
(forall (?t1 ?t2)
	(implies  (and 	(timepoint ?t1) 
			(timepoint ?t2))
    		  (or 	(= ?t1 ?t2) 
			(before ?t1 ?t2) 
			(before ?t2 ?t1))))
SWSL-FOL
forall ?t1 ?t2
  ( timepoint(?t1) and timepoint(?t2) ==>
    ?t1 :=: ?t2 or before(?t1, ?t2) or before(?t2, ?t1) ).
SWSL-Rules
neg timepoint(?t1) :- timepoint(?t2) and neg?t1 :=: ?t2 and neg before(?t1,?t2) and neg before(?t2,?t1).
neg timepoint(?t2) :- timepoint(?t1) and neg ?t1 :=: ?t2 and neg before(?t1,?t2) and neg before(?t2,?t1).
?t1 :=: ?t2 :- timepoint(?t1) and timepoint(?t2) and neg before(?t1,?t2) and neg before(?t2,?t1).
before(?t1,?t2) :- timepoint(?t1) and timepoint(?t2) and neg ?t1 :=: ?t2 and neg before(?t2,?t1).
before(?t2,?t1) :- timepoint(?t1) and timepoint(?t2) and neg ?t1 :=: ?t2 and neg before(?t1,?t2).
Note: The following could cause problems, because time is assumed to be some built-in theory, such as the integers. For integers it doesn't make sense to assert additional equalities, since they could contradict the built-in theory.
  ?t1 :=: ?t2 :- timepoint(?t1), timepoint(?t2),
                 neg before(?t1,?t2), neg before(?t2, ?t1).
Axiom 3 The before relation is irreflexive.

KIF
(forall (?t1)
	(not (before ?t1 ?t1)))
SWSL-FOL
forall ?t1
  ( neg before(?t1, ?t1) ).
SWSL-Rules
neg before(?t1, ?t1) :- timepoint(?t1).
Notes:
  1. Another possibility is to use an empty head:
    :- before(?t1, ?t1). 
    
  2. neg before(?t1,?t1)
    
    would not be a "safe" rule, i.e., the bindings cannot be supplied by the body, which is inefficient for exhaustive forward reasoning and also not operational for backward reasoning when the goal contains a variable. Many engines do not support unsafe rules at all.

    We address this issue by adding "typing" conditions (i.e., the timepoint atom) to the body that provide bindings.

  3. This axiom could be expressed in Prolog in this fashion:
    before(X,Y) :- X==Y, !, fail.
    
Axiom 4 The before relation is transitive.

KIF
(forall (?t1 ?t2 ?t3)
	(implies  (and 	(before ?t1 ?t2) 
			(before ?t2 ?t3))
		  (before ?t1 ?t3)))
SWSL-FOL
forall ?t1 ?t2 ?t3
  ( before(?t1, ?t2) and before(?t2, ?t3) ==> before(?t1, ?t3) ).
SWSL-Rules
neg before(?t1, ?t2) :- before(?t2, ?t3) and neg before(?t1, ?t3).
neg before(?t2, ?t3) :- before(?t1, ?t2) and neg before(?t1, ?t3).
before(?t1, ?t3) :- before(?t1, ?t2) and before(?t2, ?t3).
Axiom 5 The timepoint inf- is before all other timepoints.

KIF
(forall (?t)
(implies  (and (timepoint ?t) (not (= ?t inf-)))
	  (before inf- ?t))
SWSL-FOL
forall ?t
  ( timepoint(?t) and neg (?t :=: minusInf) ==> before(minusInf, ?t) ).
SWSL-Rules
neg timepoint(?t) :- neg ?t :=: minusInf and neg before(minusInf, ?t).
?t :=: minusInf :- timepoint(?t) and neg before(minusInf, ?t).
before(minusInf, ?t) :- timepoint(?t) and neg ?t :=: minusInf.
Axiom 6 Every other timepoint is before inf+.

KIF
(forall (?t)
(implies  (and (timepoint ?t) (not (= ?t inf+)))
	  (before ?t inf+))
SWSL-FOL
forall ?t
  ( timepoint(?t) and neg (?t :=: plusInf) ==> before(?t, plusInf) ).
SWSL-Rules
neg timepoint(?t) :- neg ?t :=: plusInf and neg before(?t, plusInf).
?t :=: plusInf :- timepoint(?t) and neg before(?t, plusInf).
before(?t, plusInf) :- timepoint(?t) and neg ?t :=: plusInf.
Axiom 7 Given any timepoint t other than inf-, there is a timepoint between inf- and t.

KIF
(forall (?t)
	(implies  (and 	(timepoint ?t) 
			(not (= ?t inf-)))
		  (exists (?u) 
			(between inf- ?u ?t))))
SWSL-FOL
forall ?End
  ( timepoint(?End) and neg (?End :=: minusInf) ==>
    exists ?u ( between(minusInf, ?u, ?End) ) ).
SWSL-Rules
neg timepoint(?End) :- neg ?End :=: minusInf and neg between(minusInf, _#1(?End), ?End).
?End :=: minusInf :- timepoint(?End) and neg between(minusInf, _#1(?End), ?End).
between(minusInf, _#1(?End), ?End) :- timepoint(?End) and neg ?End :=: minusInf.
Axiom 8 Given any timepoint t other than inf+, there is a timepoint between t and inf+.

KIF
(forall (?t)
	(implies  (and 	(timepoint ?t) 
			(not (= ?t inf+)))
		  (exists (?u) 
			(between ?t ?u inf+))))
SWSL-FOL
forall ?Beg
  ( timepoint(?Beg) and neg (?Beg :=: plusInf) ==>
    exists ?u ( between(?Beg, ?u, plusInf) ) ).
SWSL-Rules
neg timepoint(?Beg)  :- neg ?Beg :=: plusInf and neg between(?Beg, _#1(?Beg), plusInf).
?Beg :=: plusInf :- timepoint(?Beg) and neg between(?Beg, _#1(?Beg), plusInf).
between(?Beg, _#1(?Beg), plusInf) :- timepoint(?Beg) and neg ?Beg :=: plusInf.
Axiom 9 Everything is either an activity, activity occurrence, timepoint, or object.

KIF
(forall (?x)
	(or 	(activity ?x) 
		(activity_occurrence ?x) 
		(timepoint ?x) 
		(object ?x)))
SWSL-FOL
forall ?x
  ( activity(?x) or activity_occurrence(?x) or timepoint(?x) or object(?x) ).
SWSL-Rules
activity(?x) :- neg activity_occurrence(?x) and neg timepoint(?x) and neg object(?x).
activity_occurrence(?x) :- neg activity(?x) and neg timepoint(?x) and neg object(?x).
timepoint(?x) :- neg activity(?x) and neg activity_occurrence(?x) and neg object(?x).
object(?x) :- neg activity(?x) and neg activity_occurrence(?x) and neg timepoint(?x).
Axiom 10 Objects, activities, activity occurrences, and timepoints are all distinct kinds of things.

KIF
(forall (?x)
(and (implies (activity ?x)
         (not (or (activity_occurrence ?x) (object ?x) (timepoint ?x))))
     (implies (activity_occurrence ?x)
         (not (or (object ?x) (timepoint ?x))))
     (implies (object ?x)
         (not (timepoint ?x))))
SWSL-FOL
forall ?x
  ( ( activity(?x) ==>
      neg ( activity_occurrence(?x) or object(?x) or timepoint(?x) ) )
    and
    ( activity_occurrence(?x) ==>
      neg ( object(?x) or timepoint(?x) ) )
    and
    ( object(?x) ==>
      neg timepoint(?x) ) ).
SWSL-Rules
neg activity(?x) :- activity_occurrence(?x).
neg activity_occurrence(?x) :- activity(?x).

neg activity(?x) :- object(?x).
neg object(?x) :- activity(?x).

neg activity(?x) :- timepoint(?x).
neg timepoint(?x) :- activity(?x).

neg activity_occurrence(?x) :- object(?x).
neg object(?x) :- activity_occurrence(?x).

neg activity_occurrence(?x) :- timepoint(?x).
neg timepoint(?x) :- activity_occurrence(?x).

neg object(?x) :- timepoint(?x).
neg timepoint(?x) :- object(?x).
Axiom 11 The occurrence relation only holds between activities and activity occurrences.

KIF
(forall (?a ?occ)
	(implies  (occurrence_of ?occ ?a)
		  (and	(activity ?a)
			(activity_occurrence ?occ))))
SWSL-FOL
forall ?a, ?occ
  ( occurrence_of(?occ, ?a) ==>
    ( activity(?a) and activity_occurrence(?occ) ) ).
SWSL-Rules
neg occurrence_of(?occ ?a) :- neg activity(?a).
activity(?a) :- occurrence_of(?occ ?a).

neg occurrence_of(?occ ?a) :- neg activity_occurrence(?occ).
activity_occurrence(?occ) :- occurrence_of(?occ ?a).
Axiom 12 Every activity occurrence is the occurrence of some activity.

KIF
(forall (?occ)
	(implies  (activity_occurrence ?occ)
		  (exists (?a)
			(and	(activity ?a)
				(occurrence_of ?occ ?a)))))
SWSL-FOL
forall ?occ
  ( activity_occurrence(?occ) ==>
    exists ?a	
     ( activity(?a) and occurrence_of(?occ, ?a) ) ).
SWSL-Rules
neg activity_occurrence(?occ) :- neg activity(_#1(?occ)).
activity(_#1(?occ)) :- activity_occurrence(?occ).

neg activity_occurrence(?occ) :- neg occurrence_of(?occ, _#1(?occ)).
occurrence_of(?occ, _#1(?occ)) :- activity_occurrence(?occ).
Axiom 13 An activity occurrence is associated with a unique activity.

KIF
(forall (?occ ?a1 ?a2)
        (implies (and   (occurrence_of ?occ ?a1)
                        (occurrence_of ?occ ?a2))
                 (= ?a1 ?a2))))
SWSL-FOL
forall ?occ, ?a1, ?a2
  ( occurrence_of(?occ ?a1) and occurrence_of(?occ, ?a2) ==>
    ?a1 :=: ?a2 ).
SWSL-Rules
neg occurrence_of(?occ, ?a1) :- occurrence_of(?occ, ?a2) and neg ?a1 :=: ?a2.
neg occurrence_of(?occ, ?a2) :- occurrence_of(?occ, ?a1) and neg ?a1 :=: ?a2.
?a1 :=: ?a2 :- occurrence_of(?occ, ?a1) and occurrence_of(?occ, ?a2).
Axiom 14 The begin and end of an activity occurrence or object are timepoints.

KIF
(forall (?a ?x)
	(implies  (or	(occurrence_of ?x ?a)
			(object ?x))
    		  (and 	(timepoint (beginof ?x))
         		(timepoint (endof ?x)))))
SWSL-FOL
forall ?a, ?x
  ( ( occurrence_of(?x, ?a) or object(?x) ) ==>
    ( timepoint(beginof(?x)) and timepoint(endof(?x)) ) ).
SWSL-Rules
neg occurrence_of(?x,?a) :- neg timepoint(beginof(?x)).
timepoint(beginof(?x)) :- occurrence_of(?x,?a).

neg occurrence_of(?x,?a) :- neg timepoint(endof(?x)).
timepoint(endof(?x))   :- occurrence_of(?x, ?a).

neg object(?x) :- neg timepoint(beginof(?x)).
timepoint(beginof(?x)) :- object(?x).

neg object(?x) :- neg timepoint(endof(?x)).
timepoint(endof(?x))   :- object(?x). 
Axiom 15 The begin point of every activity occurrence or object is before or equal to its end point.

KIF
(forall (?a ?x)
	(implies (or	(activity_occurrence ?x)
			(object ?x))
		 (beforeEq (beginof ?x) (endof ?x))))
SWSL-FOL
forall ?a, ?x
  ( activity_occurrence(?x) or object(?x) ==>
    beforeEq(beginof(?x), endof(?x)) ).
SWSL-Rules
neg activity_occurrence(?x) :- neg beforeEq(beginof(?x), endof(?x)).
beforeEq(beginof(?x), endof(?x)) :- activity_occurrence(?x).

neg object(?x) :- neg beforeEq(beginof(?x), endof(?x)).
beforeEq(beginof(?x), endof(?x)) :- object(?x).
Axiom 16 The participates_in relation only holds between objects, activities, and timepoints, respectively.

KIF
(forall (?x ?occ ?t)
	(implies  (participates_in ?x ?occ ?t)
    		  (and 	(object ?x) 
			(activity_occurrence ?occ) 
			(timepoint ?t))))
SWSL-FOL
forall ?x, ?occ, ?t
  ( participates_in(?x, ?occ, ?t) ==>
    object(?x) and activity_occurrence(?occ)and timepoint(?t) ).
SWSL-Rules
object(?x) :- participates_in(?x ?_Occ ?t).
neg participates_in(?x ?_Occ ?t) :- neg object(?x).

activity_occurrence(?occ) :- participates_in(?x ?occ ?t).
neg participates_in(?x ?occ ?t) :- neg activity_occurrence(?occ).

timepoint(?t) :- participates_in(?x ?_Occ ?t).
neg participates_in(?x ?_Occ ?t) :- neg timepoint(?t).
Axiom 17 An object can participate in an activity only at those timepoints at which both the object exists and the activity is occurring.

KIF
(forall (?x ?occ ?t)
	(implies  (participates_in ?x ?a ?t)
    		  (and 	(exists_at ?x ?t)
         		(is_occurring_at ?occ ?t))))
SWSL-FOL
forall ?x, ?occ, ?t
  ( participates_in(?x, ?a, ?t) ==>
    exists_at(?x, ?t) and is_occurring_at(?occ, ?t) ).
SWSL-Rules
exists_at(?x, ?t) :- participates_in(?x, ?a, ?t).
neg participates_in(?x, ?a, ?t) :- neg exists_at(?x, ?t).

is_occurring_at(?a, ?t) :- participates_in(?x, ?a, ?t).
neg participates_in(?x, ?a, ?t) :- neg is_occurring_at(?a, ?t).

Supporting Definitions

Definition 1 Timepoint ?t2 is between timepoints ?t1 and ?t3 if and only if ?t1 is before ?t2 and ?t2 is before ?t3.

KIF
(forall (?t1 ?t2 ?t) (iff (between ?t1 ?t2 ?t3)
  (and (before ?t1 ?t2) (before ?t2 ?t3))))
SWSL-FOL
forall ?t1, ?t2, ?t
  ( between(?t1, ?t2, ?t3) iff
    before( ?t1, ?t2) and before(?t2, ?t3) ).
SWSL-Rules
neg between(?Beg, ?Mid, ?End) :- neg before(?Beg, ?Mid).
before(?Beg, ?Mid) :- between(?Beg, ?Mid, ?End).

neg between(?Beg, ?Mid, ?End) :- neg before(?Mid, ?End).
before(?Mid, ?End) :- between(?Beg, ?Mid, ?End).

neg before(?Beg, ?Mid)  :- before(?Mid, ?End) and neg between(?Beg, ?Mid, ?End).
neg before(?Mid, ?End) :- before(?Beg, ?Mid) and neg between(?Beg, ?Mid, ?End).
between(?Beg, ?Mid, ?End) :- before(?Beg, ?Mid) and before(?Mid, ?End).
Definition 2 Timepoint ?t1 is beforeEq timepoint ?t2 if and only if ?t1 is before or equal to ?t2.

KIF
(forall (?t1 ?t2) (iff (beforeEq ?t1 ?t2)
  (and (timepoint ?t1) (timepoint ?t2)
       (or (before ?t1 ?t2) (= ?t1 ?t2)))))
SWSL-FOL
forall ?t1, ?t2
  ( beforeEq(?t1, ?t2) iff
    ( timepoint(?t1) and (timepoint ?t2) and
      ( before(?t1, ?t2) or ?t1 :=: ?t2 ) ) ).
SWSL-Rules
neg timepoint(?t1) :- timepoint(?t2) and before(?t1,?t2) and neg beforeEq(?t1,?t2).
neg timepoint(?t2) :- timepoint(?t1) and before(?t1,?t2) and neg beforeEq(?t1,?t2).
neg before(?t1,?t2) :- timepoint(?t1) and timepoint(?t2) and neg beforeEq(?t1,?t2).
beforeEq(?t1,?t2) :- timepoint(?t1) and timepoint(?t2) and before(?t1,?t2).

neg timepoint(?t1) :- timepoint(?t2) and ?t1 :=: ?t2 and neg beforeEq(?t1,?t2).
neg timepoint(?t2) :- timepoint(?t1)and ?t1 :=: ?t2 and neg beforeEq(?t1,?t2).
neg ?t1 :=: ?t2 :- timepoint(?t1) and timepoint(?t2) and neg beforeEq(?t1,?t2).
beforeEq(?t1,?t2) :- timepoint(?t1) and timepoint(?t2) and ?t1 :=: ?t2.

neg beforeEq(?t1,?t2) :- neg timepoint(?t1).
timepoint(?t1) :- beforeEq(?t1,?t2).

neg beforeEq(?t1,?t2) :- neg timepoint(?t2).
timepoint(?t2) :- beforeEq(?t1,?t2).

neg beforeEq(?t1,?t2) :- neg before(?t1,?t2) and neg ?t1 :=: ?t2.
before(?t1,?t2) :- beforeEq(?t1,?t2) and neg ?t1 :=: ?t2.
?t1 :=: ?t2 :- beforeEq(?t1,?t2) and neg before(?t1,?t2).
Definition 3 Timepoint ?t2 is betweenEq timepoints ?t1 and ?t3 if and only if ?t1 is before or equal to ?t2, and ?t2 is before or equal to ?t3.

KIF
(forall (?t1 ?t2 ?t3) (iff (betweenEq ?t1 ?t2 ?t3)
  (and (beforeEq ?t1 ?t2)
       (beforeEq ?t2 ?t3))))
SWSL-FOL
forall ?t1, ?t2, ?t3
  ( betweenEq(?t1, ?t2, ?t3) iff
    beforeEq(?t1, ?t2) and beforeEq(?t2, ?t3) ).
SWSL-Rules
betweenEq(?t1, ?t2, ?t3) :-  beforeEq(?t1, ?t2) and beforeEq(?t2, ?t3).
neg beforeEq(?t1, ?t2) :- neg betweenEq(?t1, ?t2, ?t3) and beforeEq(?t2, ?t3).
neg beforeEq(?t2, ?t3) :-neg betweenEq(?t1, ?t2, ?t3) and beforeEq(?t1, ?t2). 

beforeEq(?t1, ?t2) :- betweenEq(?t1, ?t2, ?t3).
neg betweenEq(?t1, ?t2, ?t3) :- neg beforeEq(?t1, ?t2).

beforeEq(?t2, ?t3) :- betweenEq(?t1, ?t2, ?t3).
neg betweenEq(?t1, ?t2, ?t3) :- neg beforeEq(?t2, ?t3).
Definition 4 An object exists at a timepoint ?t if and only if ?t is betweenEq its begin and end points.

KIF
(forall (?x ?t) (iff (exists_at ?x ?t)
  (and (object ?x)
       (betweenEq (beginof ?x) ?t (endof ?x)))))
SWSL-FOL
forall ?x, ?t)
  ( exists_at(?x, ?t) iff
    object(?x) and betweenEq(beginof(?x), ?t, endof(?x)) ).
SWSL-Rules
neg exists_at(?x,?t) :- neg object(?x).
object(?x) :- exists_at(?x,?t).

neg exists_at(?x,?t) :- neg betweenEq(beginof(?x),?t,endof(?x)).
betweenEq(beginof(?x),?t,endof(?x)) :- exists_at(?x,?t).

exists_at(?x,?t) :- object(?x) and betweenEq(beginof(?x),?t,endof(?x)).
neg object(?x) :- neg exists_at(?x,?t) and betweenEq(beginof(?x),?t,endof(?x)).
neg betweenEq(beginof(?x),?t,endof(?x)) :- neg exists_at(?x,?t) and object(?x).
Definition 5 An activity is occurring at a timepoint ?t if and only if ?t is betweenEq the activity's begin and end points.

KIF
(forall (?occ ?t) (iff (is_occurring_at ?occ ?t)
	(and 	(activity_occurrence ?occ)
		(betweenEq (beginof ?occ) ?t (endof ?occ))))))
SWSL-FOL
forall ?occ, ?t
 ( is_occurring_at(?occ, ?t) iff
   activity_occurrence(?occ) and betweenEq(beginof(?occ), ?t, endof(?occ)) ).
SWSL-Rules
is_occurring_at(?occ, ?t) :- activity_occurrence(?occ) and betweenEq(beginof(?occ), ?t, endof(?occ)).
neg activity_occurrence(?occ) :- neg is_occurring_at(?occ, ?t) and betweenEq(beginof(?occ), ?t, endof(?occ)).
neg betweenEq(beginof(?occ), ?t, endof(?occ)) :- neg is_occurring_at(?occ, ?t) and activity_occurrence(?occ).

activity_occurrence(?occ) :- is_occurring_at(?occ, ?t).
neg is_occurring_at(?occ, ?t) :- neg activity_occurrence(?occ).

betweenEq(beginof(?occ), ?t, endof(?occ)) :- is_occurring_at(?occ, ?t).
neg is_occurring_at(?occ, ?t) :- neg betweenEq(beginof(?occ), ?t, endof(?occ)).


A.2 Theory of Subactivities

Extension Name: subactivity.th
Theories Required by this Extension: psl_core.th
Definitional Extensions Required by this Extension: None

Primitive Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules

Defined Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules

Axioms

Axiom 1 subactivity is a relation over activities

KIF
(forall (?a1 ?a2)
	(implies  (subactivity ?a1 ?a2)
		  (and	(activity ?a1)
			(activity ?a2))))
SWSL-FOL
forall ?a1, ?a2
  ( subactivity(?a1 ,?a2) ==>
    ( activity(?a1) and activity(?a2) ) ).
SWSL-Rules
activity(?a1) :- subactivity(?a1, ?a2).
neg subactivity(?a1, ?a2) :- neg activity(?a1).

activity(?a2) :- subactivity(?a1, ?a2).
neg subactivity(?a1, ?a2) :- neg activity(?a2).
Axiom 2 The subactivity relation is reflexive.

KIF
(forall (?a)
        (implies  (activity ?a)
                  (subactivity ?a ?a)))
SWSL-FOL
forall ?a
  ( activity(?a) ==>
    subactivity(?a, ?a) ).
SWSL-Rules
subactivity(?a, ?a) :- activity(?a).
neg activity(?a) :- neg subactivity(?a, ?a).
Axiom 3 The subactivity relation is antisymmetric.

KIF
(forall (?a1 ?a2)
	(implies  (and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a1))
		  (= ?a1 ?a2)))
SWSL-FOL
forall ?a1 ?a2
  ( ( subactivity(?a1 ?a2) and
      subactivity(?a2 ?a1) ) ==>
    ?a1 :=: ?a2 ).
SWSL-Rules
?a1 :=: ?a2 :- subactivity(?a1, ?a2) and subactivity ?a2 ?a1).
neg subactivity(?a1, ?a2) :- subactivity ?a2 ?a1) and neg ?a1 :=: ?a2.
neg subactivity ?a2 ?a1) :- subactivity(?a1, ?a2) and neg ?a1 :=: ?a2.
Axiom 4 The subactivity relation is transitive.

KIF
(forall (?a1 ?a2 ?a3)
	(implies  (and	(subactivity ?a1 ?a2)
			(subactivity ?a2 ?a3))
		  (subactivity ?a1 ?a3)))
SWSL-FOL
forall ?a1, ?a2, ?a3
  ( ( subactivity(?a1, ?a2) and
      subactivity(?a2, ?a3) ) ==>
    subactivity(?a1, ?a3) ).
SWSL-Rules
neg subactivity(?a1, ?a2) :- subactivity(?a2, ?a3) and neg subactivity(?a1, ?a3).
neg subactivity(?a2, ?a3) :- subactivity(?a1, ?a2) and neg subactivity(?a1, ?a3).
subactivity(?a1, ?a3) :- subactivity(?a1, ?a2) and subactivity(?a2, ?a3).
Axiom 5 The subactivity relation is a discrete ordering, so every activity has an upwards successor in the ordering.

KIF
(forall (?a1 ?a2)
	(implies  (subactivity ?a1 ?a2)
		  (exists (?a3)
			(and	(subactivity ?a1 ?a3)
				(subactivity ?a3 ?a2)
				(forall (?a4)
					(implies  (and	(subactivity ?a1 ?a4)
							(subactivity ?a4 ?a3)
						  (or	(= ?a4 ?a1)
							(= ?a4 ?a3))))))))
SWSL-FOL
forall ?a1, ?a2
 ( subactivity(?a1, ?a2) ==>
   exists (?a3)
     ( subactivity(?a1, ?a3) and
       subactivity(?a3, ?a2) and
       forall ?a4
         ( ( subactivity(?a1, ?a4) and subactivity(?a4, ?a3) ) ==>
         ( ?a4 :=: ?a1 or ?a4 :=: ?a3 ) ) ) ).
SWSL-Rules
neg subactivity(?a1,?a2) :- neg subactivity(?a1,_#1(?a1,?a2)).
subactivity(?a1,_#1(?a1,?a2)) :- subactivity(?a1,?a2).

neg subactivity(?a1,?a2) :- neg subactivity(_#1(?a1,?a2),?a2).
subactivity(_#1(?a1,?a2),?a2) :- subactivity(?a1,?a2).

neg subactivity(?a1,?a2) :- subactivity(?a1,?a4) and subactivity(?a4,_#1(?a1,?a2)) and neg ?a4 :=: ?a1 and neg ?a4 :=: _#1(?a1,?a2).
neg subactivity(?a1,?a4) :- subactivity(?a1,?a2) and subactivity(?a4,_#1(?a1,?a2)) and neg ?a4 :=: ?a1 and neg ?a4 :=: _#1(?a1,?a2).
neg subactivity(?a4,_#1(?a1,?a2)) :- subactivity(?a1,?a2) and
subactivity(?a1,?a4) and neg ?a4 :=: ?a1 and neg ?a4 :=: _#1(?a1,?a2).
?a4 :=: ?a1 :- subactivity(?a1,?a2) and subactivity(?a1,?a4) and subactivity(?a4,_#1(?a1,?a2)) and neg ?a4 :=: _#1(?a1,?a2).
?a4 :=: _#1(?a1,?a2) :- subactivity(?a1,?a2) and subactivity(?a1,?a4) and subactivity(?a4,_#1(?a1,?a2)) and neg ?a4 :=: ?a1.
Axiom 6 The subactivity relation is a discrete ordering, so every activity has a downwards successor in the ordering.

KIF
(forall (?a1 ?a2)
	(implies  (subactivity ?a1 ?a2)
		  (exists (?a3)
			(and	(subactivity ?a1 ?a3)
				(subactivity ?a3 ?a2)
				(forall (?a4)
					(implies  (and	(subactivity ?a3 ?a4)
							(subactivity ?a4 ?a2)
						  (or	(= ?a4 ?a2)
							(= ?a4 ?a3))))))))
SWSL-FOL
forall ?a1, ?a2
  ( subactivity(?a1, ?a2) ==>
    exists ?a3
      ( subactivity(?a1, ?a3) and
	subactivity(?a3, ?a2) and
	forall ?a4
          ( ( subactivity(?a3, ?a4) and subactivity(?a4, ?a2) ) ==>
            ( ?a4 :=: ?a2 or ?a4 :=: ?a3 ) ) ) ). 

SWSL-Rules
neg subactivity(?a1,?a2) :- neg subactivity(?a1,_#1(?a1,?a2)).
subactivity(?a1,_#1(?a1,?a2)) :- subactivity(?a1,?a2).

neg subactivity(?a1,?a2) :- neg subactivity(_#1(?a1,?a2),?a2).
subactivity(_#1(?a1,?a2),?a2) :- subactivity(?a1,?a2).

neg subactivity(?a1,?a2) :- subactivity(_#1(?a1,?a2),?a4) and subactivity(?a4,?a2) and neg ?a4 :=: ?a2 and neg ?a4 :=: _#1(?a1,?a2).
neg subactivity(_#1(?a1,?a2),?a4) :- subactivity(?a1,?a2) and subactivity(?a4,?a2) and neg ?a4 :=: ?a2 and neg ?a4 :=: _#1(?a1,?a2).
neg subactivity(?a4,?a2) :- subactivity(?a1,?a2) and subactivity(_#1(?a1,?a2),?a4) and neg ?a4 :=: ?a2 and neg ?a4 :=: _#1(?a1,?a2).
?a4 :=: ?a2 :- subactivity(?a1,?a2) and subactivity(_#1(?a1,?a2),?a4) and subactivity(?a4,?a2) and neg ?a4 :=: _#1(?a1,?a2).
?a4 :=: _#1(?a1,?a2) :- subactivity(?a1,?a2) and subactivity(_#1(?a1,?a2),?a4) and subactivity(?a4,?a2) and neg ?a4 :=: ?a2.

Definitions

Definition 1 An activity is primitive iff it has no proper subactivities.

KIF
(forall (?a ?a1) (iff (primitive ?a)
(implies  (subactivity ?a1 ?a)
	  (= ?a1 ?a)))))
SWSL-FOL
forall ?a, ?a1
  ( primitive(?a) <==>
    ( subactivity ?a1 ?a) ==> ?a1 :=: ?a ).
SWSL-Rules
primitive(?a) :-
  subactivity(?a1, ?a) ==> (?a1 :=: ?a).
subactivity(?a1, ?a) ==> (?a1 :=: ?a) :-
  primitive(?a).


A.3 Theory of Occurrence Trees

Extension Name: occtree.th
Theories Required by this Extension: psl_core.th
Definitional Extensions Required by this Extension: None

Primitive Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules Functions:

KIF SWSL-FOL and SWSL-Rules

Defined Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules

Axioms

Axiom 1 The earlier relation is restricted to activity occurrences.

KIF
(forall (?s1 ?s2)
	(implies  (earlier ?s1 ?s2)
		  (and	(activity_occurrence ?s1)
			(activity_occurrence ?s2))))
SWSL-FOL
forall ?s1, ?s2
  ( earlier(?s1, ?s2) ==>
    activity_occurrence(?s1) and activity_occurrence(?s2) ).
SWSL-Rules
neg earlier(?s1, ?s2) :- neg activity_occurrence(?s1).
activity_occurrence(?s1) :- earlier(?s1, ?s2).

neg earlier(?s1, ?s2) :- neg activity_occurrence(?s2).
activity_occurrence(?s2) :- earlier(?s1, ?s2).
Axiom 2 The ordering relation over occurrences is irreflexive.

KIF
(forall (?s1 ?s2)
	(implies  (earlier ?s1 ?s2)
		  (not (earlier ?s2 ?s1))))
SWSL-FOL
forall ?s1, ?s2
  ( earlier(?s1, ?s2) ==>
    neg earlier(?s2, ?s1) ).
SWSL-Rules
neg earlier(?s2, ?s1) :- earlier(?s1, ?s2).
neg earlier(?s1, ?s2) :- earlier(?s2, ?s1).
Axiom 3 The ordering relation over occurrences is transitive.

KIF
(forall (?s1 ?s2 ?s3)
	(implies  (and	(earlier ?s1 ?s2)
			(earlier ?s2 ?s3))
		  (earlier ?s1 ?s3)))
SWSL-FOL
forall ?s1, ?s2, ?s3
  ( earlier(?s1, ?s2) and earlier(?s2, ?s3) ==>
    earlier(?s1, ?s3) ).
SWSL-Rules
neg earlier(?s1, ?s2) :- earlier(?s2, ?s3) and neg earlier(?s1, ?s3).
neg earlier(?s2, ?s3) :- earlier(?s1, ?s2) and neg earlier(?s1, ?s3).
earlier(?s1, ?s3) :- earlier(?s1, ?s2) and earlier(?s2, ?s3).
Axiom 4 A branch in the occurrence tree is totally ordered.

KIF
(forall (?s1 ?s2 ?s3)
	(implies  (and	(earlier ?s1 ?s2)
			(earlier ?s3 ?s2))
		  (or	(earlier ?s1 ?s3)
			(earlier ?s3 ?s1)
			(= ?s3 ?s1))))
SWSL-FOL
forall ?s1, ?s2, ?s3
  ( earlier(?s1, ?s2) and earlier(?s3, ?s2) ==>
    earlier(?s1, ?s3) or earlier(?s3, ?s1) or ?s3 :=: ?s ).
SWSL-Rules
neg earlier(?s1, ?s2) :- 
    earlier(?s3, ?s2) and neg earlier(?s1, ?s3) and neg earlier(?s3, ?s1) and neg ?s3 :=: ?s1.
neg earlier(?s3, ?s2) :- 
    earlier(?s1, ?s2) and neg earlier(?s1, ?s3) and neg earlier(?s3, ?s1) and neg ?s3 :=: ?s1.
earlier(?s1, ?s3) :- 
    earlier(?s1, ?s2) and earlier(?s3, ?s2) and neg earlier(?s3, ?s1) and neg ?s3 :=: ?s1.
earlier(?s3, ?s1) :- 
    earlier(?s1, ?s2) and earlier(?s3, ?s2) and neg earlier(?s1, ?s3) and neg ?s3 :=: ?s1.
?s3 :=: ?s1 :- 
    earlier(?s1, ?s2) and earlier(?s3, ?s2) and neg earlier(?s1, ?s3) and neg earlier(?s3, ?s1).
Axiom 5 No occurrence is earlier than an initial occurrence.

KIF
(forall (?s1)
	(iff	(initial ?s1)
		(not (exists (?s2)
			(earlier ?s2 ?s1)))))

SWSL-FOL
forall ?s1
  ( initial(?s1) <==> neg exists ?s2 ( earlier(?s2,?s1) ) ).
SWSL-Rules
initial(?s1) :- neg earlier(_#1(?s1),?s1).
earlier(_#1(?s1),?s1) :- neg initial(?s1).

neg initial(?s1) :- earlier(?s2,?s1).
neg earlier(?s2,?s1) :- initial(?s1).
Axiom 6 Every branch of the occurrence tree has an initial occurrence.

KIF
(forall (?s1 ?s2)
	(implies  (earlier ?s1 ?s2)
		  (exists (?sp)
			(and	(initial ?sp)
				(earlierEq ?sp ?s1)))))
SWSL-FOL
forall ?s1, ?s2
  ( earlier(?s1, ?s2) ==>
    exists ?sp
      ( initial(?sp) and earlierEq(?sp, ?s1) ) ).
SWSL-Rules
neg earlier(?s1, ?s2) :- neg initial(_#1(?s1, ?s2)).
initial(_#1(?s1, ?s2)) :- earlier(?s1, ?s2).

neg earlier(?s1, ?s2) :- neg earlierEq(_#1(?s1, ?s2), ?s1).
earlierEq(_#1(?s1, ?s2), ?s1) :- earlier(?s1, ?s2).
Axiom 7 There is an initial occurrence of each activity.

KIF
(forall (?a)
	(implies  (activity ?a)
		  (exists (?s)
			(and	(occurrence_of ?s ?a)
				(initial ?s)))))
SWSL-FOL
forall ?a
  ( activity(?a) ==>
    exists ?s
      ( occurrence_of(?s, ?a) and initial(?s) ) ).
SWSL-Rules
neg activity(?a) :- neg occurrence_of(_#1(?a), ?a).
occurrence_of(_#1(?a), ?a) :- activity(?a).
 
neg activity(?a) :- neg initial(_#1(?a)).
initial(_#1(?a)) :- activity(?a).
Axiom 8 No two initial activity occurrences in the occurrence tree are occurrences of the same activity.

KIF
(forall (?s1 ?s2 ?a)
	(implies  (and	(initial ?s1)
			(initial ?s2)
			(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a))
		  (= ?s1 ?s2)))
SWSL-FOL
forall ?s1, ?s2, ?a
  ( initial(?s1) and initial(?s2) and
    occurrence_of(?s1, ?a) and occurrence_of(?s2, ?a) ==>
    ?s1 :=: ?s2 ).

SWSL-Rules
neg initial(?s1) :- initial(?s2) and occurrence_of(?s1, ?a) and occurrence_of(?s2, ?a) and neg ?s1 :=: ?s2.
neg initial(?s2) :- initial(?s1) and occurrence_of(?s1, ?a) and occurrence_of(?s2, ?a) and neg ?s1 :=: ?s2.
neg occurrence_of(?s1, ?a) :- initial(?s1) and initial(?s2) and occurrence_of(?s2, ?a) and neg ?s1 :=: ?s2.
neg occurrence_of(?s2, ?a) :- initial(?s1) and initial(?s2) and occurrence_of(?s1, ?a) and neg ?s1 :=: ?s2.
?s1 :=: ?s2 :- initial(?s1) and initial(?s2) and occurrence_of(?s1, ?a) and occurrence_of(?s2, ?a).
Axiom 9 The successor of an activity occurrence is an occurrence of the activity.

KIF
(forall (?a ?s)
	(implies  (and	(activity ?a)
			(activity_occurrence ?s))
		  (occurrence_of (successor ?a ?s) ?a)))
SWSL-FOL
forall ?a, ?s
  ( activity(?a) and activity_occurrence(?s) ==>
    occurrence_of(successor(?a, ?s), ?a) ).
SWSL-Rules
neg activity(?a) :- activity_occurrence(?s) and neg occurrence_of(successor(?a, ?s), ?a).
neg activity_occurrence(?s) :- activity(?a) and neg occurrence_of(successor(?a, ?s), ?a).
occurrence_of(successor(?a, ?s), ?a) :- activity(?a) and activity_occurrence(?s).
Axiom 10 Every non-initial activity occurrence is the successor of another activity occurrence.

KIF
(forall (?s)
	(implies  (not (initial ?s))
		  (exists (?a ?sp)
			(= ?s (successor ?a ?sp)))))
SWSL-FOL
forall ?s
  ( neg initial(?s) ==>
    exists ?a ?sp
      ( ?s :=: successor(?a, ?sp) ) ).
SWSL-Rules
?s :=: successor(_#1(?s), _#2(?s)) :- neg initial(?s).
initial(?s) :- neg ?s :=: successor(_#1(?s), _#2(?s)).
Axiom 11 An occurrence ?s1 is earlier than the successor occurrence of ?s2 if and only if the occurrence ?s2 is later than ?s1.

KIF
(forall (?a ?s1 ?s2)
	(iff	(earlier ?s1 (successor ?a ?s2))
		(earlierEq ?s1 ?s2)))
SWSL-FOL
forall ?a, ?s1, ?s2
  ( earlier(?s1, successor(?a, ?s2)) iff earlierEq(?s1, ?s2) ).
SWSL-Rules
earlier(?s1, successor(?a, ?s2)) :- earlierEq(?s1, ?s2).
neg earlierEq(?s1, ?s2) :- neg earlier(?s1, successor(?a, ?s2)).

earlierEq(?s1, ?s2) :- earlier(?s1, successor(?a, ?s2)).
neg earlier(?s1, successor(?a, ?s2)) :- neg earlierEq(?s1, ?s2).
Axiom 12 The legal relation restricts activity occurrences.

KIF
(forall (?s)
	(implies  (legal ?s)
		  (activity_occurrence ?s)))
SWSL-FOL
forall ?s
  ( legal(?s) ==> activity_occurrence(?s) ).
SWSL-Rules
activity_occurrence(?s) :- legal(?s).
neg legal(?s) :- neg activity_occurrence(?s).
Axiom 13 If an activity occurrence is legal, all earlier activity occurrences in the occurrence tree are also legal.

KIF
(forall (?s1 ?s2)
	(implies  (and	(legal ?s1)
			(earlier ?s2 ?s1))
		  (legal ?s2)))
SWSL-FOL
forall ?s1, ?s2
  ( legal(?s1) and earlier(?s2, ?s1) ==> legal(?s2) ).
SWSL-Rules
neg legal(?s1) :- earlier(?s2, ?s1) and neg legal(?s2).
neg earlier(?s2, ?s1) :- legal(?s1) and neg legal(?s2).
legal(?s2) :- legal(?s1) and earlier(?s2, ?s1).
Axiom 14 The endof an activity occurrence is before the beginof the successor of the activity occurrence.

KIF
(forall (?s1 ?s2)
	(implies  (earlier ?s1 ?s2)
		  (before (endof ?s1) (beginof ?s2))))

TBD - why isn't successor mentioned above?
SWSL-FOL
forall ?s1, ?s2
  ( earlier(?s1, ?s2) ==>
    before(endof(?s1), beginof(?s2)) ).
SWSL-Rules
before(endof(?s1), beginof(?s2)) :- earlier(?s1, ?s2).
neg earlier(?s1, ?s2) :- neg before(endof(?s1), beginof(?s2)).

Definitions

Definition 1 An activity occurrence ?s1 precedes another activity occurrence ?s2 if and only if ?s1 is earlier than ?s2 in the occurrence tree and ?s2 is legal.

KIF
(forall (?s1 ?s2) (iff (precedes ?s1 ?s2)
(and	(earlier ?s1 ?s2)
	(legal ?s2))))
SWSL-FOL
forall ?s1, ?s2
  ( precedes(?s1, ?s2) iff
    earlier(?s1, ?s2) and legal(?s2) ).
SWSL-Rules
neg precedes(?s1, ?s2) :- neg earlier(?s1, ?s2) .
earlier(?s1, ?s2)  :- precedes(?s1, ?s2).

neg precedes(?s1, ?s2) :- neg legal(?s2).
legal(?s2) :- precedes(?s1, ?s2).

neg earlier(?s1, ?s2) :- legal(?s2) and neg precedes(?s1, ?s2).
neg legal(?s2) :- earlier(?s1, ?s2) and neg precedes(?s1, ?s2).
precedes(?s1, ?s2) :- earlier(?s1, ?s2) and legal(?s2).
Definition 2 An activity occurrence ?s1 is EarlierEq than an activity occurrence ?s2 if and only if it is either earlier than ?s2 or it is equal to ?s2.

KIF
(forall (?s1 ?s2) (iff (earlierEq ?s1 ?s2)
(or	(earlier ?s1 ?s2)
	(= ?s1 ?s2))))
SWSL-FOL
forall ?s2, ?s3
  ( earlierEq(?s1, ?s2) iff
    earlier(?s1, ?s2) or ?s1 :=: ?s2 ).
SWSL-Rules
earlierEq(?s1,?s2) :- earlier(?s1, ?s2).
neg earlier(?s1, ?s2) :- neg earlierEq(?s1,?s2).

earlierEq(?s1,?s2) :- ?s1 :=: ?s2.
neg ?s1 :=: ?s2 :- neg earlierEq(?s1,?s2).

neg earlierEq(?s1,?s2) :- neg earlier(?s1, ?s2) and neg ?s1 :=: ?s2.
earlier(?s1, ?s2) :- neg earlierEq(?s1,?s2) and neg ?s1 :=: ?s2.
?s1 :=: ?s2 :- earlierEq(?s1,?s2) and neg earlier(?s1, ?s2).
Definition 3 An activity is poss at some occurrence if and only if the successor occurrence of the activity is legal.

KIF
(forall (?a ?s) (iff (poss ?a ?s)
(legal (successor ?a ?s))))
SWSL-FOL
forall ?a, ?s
  ( poss(?a, ?s) iff legal(successor(?a, ?s)) ).
SWSL-Rules
poss(?a, ?s) :- legal(successor(?a, ?s)).
neg legal(successor(?a, ?s)) :- neg poss(?a, ?s).

legal(successor(?a, ?s)) :- poss(?a, ?s).
neg poss(?a, ?s) :- neg legal(successor(?a, ?s)).


A.4 Theory of Discrete States

Extension Name: disc_state.th
Theories Required by this Extension: occtree.th, psl_core.th
Definitional Extensions Required by this Extension: None

Primitive Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules

Defined Lexicon

(none)

Axioms

Axiom 1 States are objects.

KIF
(forall (?f)
	(implies  (state ?f)
		  (object ?f)))
SWSL-FOL
forall ?f
  ( state(?f) ==> object(?f) ).
SWSL-Rules
object(?f) :- state(?f).
neg state(?f) :- neg object(?f).
Axiom 2 The holds relation is only between states and activity occurrences. Intuitively, it means that the fluent (property of the world) is true after the activity occurrence ?occ.

KIF
(forall (?f ?occ)
	(implies  (holds ?f ?occ)
		  (and	(state ?f)
			(activity_occurrence ?occ))))
SWSL-FOL
forall ?f ?occ
  holds(?f ?occ) ==>
  ( state(?f) and activity_occurrence(?occ) ).
SWSL-Rules
state(?f) :- holds(?f, ?occ).
neg holds(?f, ?occ) :- neg state(?f).

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

KIF
(forall (?f ?occ)
	(implies  (prior ?f ?occ)
		  (and	(state ?f)
			(activity_occurrence ?occ))))
SWSL-FOL
forall ?f, ?occ
  ( prior(?f, ?occ) ==>
    ( state(?f) and activity_occurrence(?occ) ) ).
SWSL-Rules
state(?f) :- prior(?f, ?occ).
neg prior(?f, ?occ) :- neg state(?f).

activity_occurrence(?occ) :- prior(?f, ?occ).
neg prior(?f, ?occ) :- neg activity_occurrence(?occ).
Axiom 4 All initial occurrences agree on the states that hold prior to them.

KIF
(forall (?occ1 ?occ2 ?f)
	(implies  (and	(initial ?occ1)
			(initial ?occ2))
		  (iff	(prior ?f ?occ1)
			(prior ?f ?occ2))))
SWSL-FOL
forall ?occ1 ?occ2 ?f
  ( ( initial(?occ1) and initial(?occ2) ) ==>
    ( prior(?f, ?occ1) <==> prior(?f, ?occ2) ) ).
SWSL-Rules
neg initial(?occ1) :- initial(?occ2) and neg prior(?f, ?occ1) and prior(?f, ?occ2).
neg initial(?occ2) :- initial(?occ1) and neg prior(?f, ?occ1) and prior(?f, ?occ2).
prior(?f, ?occ1) :- initial(?occ1) and initial(?occ2) and prior(?f, ?occ2).
neg prior(?f, ?occ2) :- initial(?occ1) and initial(?occ2) and neg prior(?f, ?occ1).

neg initial(?occ1) :- initial(?occ2) and prior(?f, ?occ1) and neg prior(?f, ?occ2).
neg initial(?occ2) :- initial(?occ1) and prior(?f, ?occ1) and neg prior(?f, ?occ2).
neg prior(?f, ?occ1) :- initial(?occ1) and initial(?occ2) and neg prior(?f, ?occ2).
prior(?f, ?occ2) :- initial(?occ1) and initial(?occ2) and prior(?f, ?occ1).
Axiom 5 A state holds after an occurrence if and only if it holds prior to the successor occurrence.

KIF
(forall (?a ?occ)
	(iff	(holds ?f ?occ)
		(prior ?f (successor ?a ?occ))))
SWSL-FOL
forall ?a ,?occ
  ( holds(?f ,?occ) <==>
    prior(?f, successor(?a ,?occ)) ).
SWSL-Rules
holds(?f, ?occ) :- prior(?f, successor(?a, ?occ)).
neg prior(?f, successor(?a, ?occ)) :- neg holds(?f, ?occ).

prior(?f, successor(?a, ?occ)) :- holds(?f, ?occ).
neg holds(?f, ?occ) :- neg prior(?f, successor(?a, ?occ)).
Axiom 6 If a fluent holds after some activity occurrence, then there exists an earliest activity occurrence along the branch where the fluent holds.

KIF
(forall (?occ1 ?f)
	(implies  (holds ?f ?occ1)
		  (exists (?occ2)
			(and	(precedes ?occ2 ?occ1)
				(holds ?f ?occ2)
				(or	(initial ?occ2)
					(not (prior ?f ?occ2)))
				(forall (?occ3)
					(implies  (and	(precedes ?occ2 ?occ3)
							(precedes ?occ3 ?occ1))
						  (holds ?f ?occ3)))))))
SWSL-FOL
forall ?occ1, ?f
  ( holds(?f, ?occ1) ==>
    exists ?occ2
      ( precedes(?occ2, ?occ1) and
        holds(?f, ?occ2) and
        ( initial(?occ2) or neg prior(?f, ?occ2) ) and
        forall ?occ3
          ( ( precedes(?occ2, ?occ3) and precedes(?occ3, ?occ1) ) ==>
              holds(?f, ?occ3) ) ) ).
SWSL-Rules
neg holds(?f,?occ1) :- neg precedes(_#1(?occ1,?f),?occ1).
precedes(_#1(?occ1,?f),?occ1) :- holds(?f,?occ1).

neg holds(?f,?occ1) :- neg holds(?f,_#1(?occ1,?f)).
holds(?f,_#1(?occ1,?f)) :- holds(?f,?occ1).

neg holds(?f,?occ1) :- neg initial(_#1(?occ1,?f)) and prior(?f,_#1(?occ1,?f)).
initial(_#1(?occ1,?f)) :- holds(?f,?occ1) and prior(?f,_#1(?occ1,?f)).
neg prior(?f,_#1(?occ1,?f)) :- holds(?f,?occ1) and neg initial(_#1(?occ1,?f)).

neg holds(?f,?occ1) :- precedes(_#1(?occ1,?f),?occ3) and precedes(?occ3,?occ1) and neg holds(?f,?occ3).
neg precedes(_#1(?occ1,?f),?occ3) :- holds(?f,?occ1) and precedes(?occ3,?occ1) and neg holds(?f,?occ3).
neg precedes(?occ3,?occ1) :- holds(?f,?occ1) and precedes(_#1(?occ1,?f),?occ3) and neg holds(?f,?occ3).
holds(?f,?occ3) :- holds(?f,?occ1) and precedes(_#1(?occ1,?f),?occ3) and precedes(?occ3,?occ1).
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.

KIF
(forall (?occ1 ?f)
	(implies  (not (holds ?f ?occ1))
		  (exists (?occ2)
			(and	(precedes ?occ2 ?occ1)
				(not (holds ?f ?occ2))
				(or	(initial ?occ2)
					(prior ?f ?occ2))
				(not (exists (?occ3)
					(and	(precedes ?occ2 ?occ3)
						(precedes ?occ3 ?occ1))
						(holds ?f ?occ3))))))))
SWSL-FOL
forall ?occ1, ?f
  ( neg holds(?f, ?occ1) ==>
    exists ?occ2
      ( precedes(?occ2, ?occ1) and
        neg holds(?f, ?occ2) and
        ( initial(?occ2) or prior(?f, ?occ2) ) and
        neg exists ?occ3
          ( precedes(?occ2, ?occ3) and
            precedes(?occ3, ?occ1) and
            holds(?f, ?occ3) ) ) ).
SWSL-Rules
holds(?f,?occ1) :- neg precedes(_#1(?occ1,?f),?occ1).
precedes(_#1(?occ1,?f),?occ1) :- neg holds(?f,?occ1).

holds(?f,?occ1) :- holds(?f,_#1(?occ1,?f)).
neg holds(?f,_#1(?occ1,?f)) :- neg holds(?f,?occ1).

holds(?f,?occ1) :- neg initial(_#1(?occ1,?f)) and neg prior(?f,_#1(?occ1,?f)).
initial(_#1(?occ1,?f)) :- neg holds(?f,?occ1) and neg prior(?f,_#1(?occ1,?f)).
prior(?f,_#1(?occ1,?f)) :- neg holds(?f,?occ1) and neg initial(_#1(?occ1,?f)).

holds(?f,?occ1) :- precedes(_#1(?occ1,?f),?occ3) and precedes(?occ3,?occ1) and holds(?f,?occ3).
neg precedes(_#1(?occ1,?f),?occ3) :- neg holds(?f,?occ1) and precedes(?occ3,?occ1) and holds(?f,?occ3).
neg precedes(?occ3,?occ1) :- neg holds(?f,?occ1) and precedes(_#1(?occ1,?f),?occ3) and holds(?f,?occ3).
neg holds(?f,?occ3) :- neg holds(?f,?occ1) and precedes(_#1(?occ1,?f),?occ3) and precedes(?occ3,?occ1).


A.5 Theory of Atomic Activities

Extension Name: atomic.th
Theories Required by this Extension: occtree.th,subactivity.th, psl_core.th
Definitional Extensions Required by this Extension: None

Primitive Lexicon

Relations:

KIF SWSL-FOL and SWSL-Rules Functions:

KIF SWSL-FOL and SWSL-Rules

Defined Lexicon

(None)

Axioms

Axiom 1 Primitive activities are atomic.

KIF
(forall (?a)
	(implies  (primitive ?a)
		  (atomic ?a)))
SWSL-FOL
forall ?a
  ( primitive(?a) ==> atomic(?a) )
SWSL-Rules
atomic(?a) :- primitive(?a).
neg primitive(?a) :- neg atomic(?a).
Axiom 2 The function conc is idempotent.

KIF
(forall (?a)
	(= ?a (conc ?a ?a)))
SWSL-FOL
forall ?a
  ( ?a :=: conc(?a, ?a) ).
SWSL-Rules
?a :=: conc(?a, ?a) :- activity(?a).
Axiom 3 The function conc is commutative.

KIF
(forall (?a1 ?a2)
	(= (conc ?a1 ?a2) (conc ?a2 ?a1)))
SWSL-FOL
forall ?a1, ?a2
  ( conc(?a1, ?a2) :=: conc(?a2 ?a1) ).
SWSL-Rules
conc(?a1, ?a2) :=: conc(?a2, ?a1) :- activity(?a).
Axiom 4 The function conc is associative.

KIF
(forall (?a1 ?a2 ?a3)
	(= (conc ?a1 (conc ?a2 ?a3)) (conc (conc ?a1 ?a2) ?a3)))
SWSL-FOL
forall ?a1, ?a2, ?a3
  ( conc(?a1 conc(?a2, ?a3)) :=: conc(conc(?a1, ?a2), ?a3) ).
SWSL-Rules
conc(?a1, conc(?a2, ?a3)) :=: conc(conc(?a1, ?a2), ?a3) :- activity(?a).
Axiom 5 The concurrent aggregation of atomic action is an atomic action.

KIF
(forall (?a1 ?a2)
	(iff	(atomic (conc ?a1 ?a2))
		(and	(atomic ?a1)
			(atomic ?a2))))
SWSL-FOL
forall ?a1, ?a2
  ( atomic(conc(?a1, ?a2)) <==>
    ( atomic(?a1) and atomic(?a2) ) ).
SWSL-Rules
neg atomic(?a1) :- atomic(?a2) and neg atomic(conc(?a1, ?a2)).
neg atomic(?a2) :- atomic(?a1) and neg atomic(conc(?a1, ?a2)).
atomic(conc(?a1, ?a2)) :- atomic(?a1) and atomic(?a2).

neg atomic(conc(?a1, ?a2)) :- neg atomic(?a1).
atomic(?a1) :- atomic(conc(?a1, ?a2)).

neg atomic(conc(?a1, ?a2)) :- neg atomic(?a2).
atomic(?a2) :- atomic(conc(?a1, ?a2)).
Axiom 6 An atomic activity ?a1 is a subactivity of an atomic activity ?a2 if and only if ?a2 is an idempotent for ?a1.

KIF
(forall (?a1 ?a2)
	(implies  (and	(atomic ?a1)
			(atomic ?a2))
		  (iff	(subactivity ?a1 ?a2)
			(= ?a2 (conc ?a1 ?a2)))))
SWSL-FOL
forall ?a1, ?a2
  ( ( atomic(?a1) and atomic(?a2) ) ==>
    ( subactivity(?a1, ?a2) <==>
      ?a2 :=: conc(?a1, ?a2) ) ).
SWSL-Rules
neg atomic(?a1) :- atomic(?a2) and neg subactivity(?a1, ?a2) and ?a2 :=: conc(?a1, ?a2).
neg atomic(?a2) :- atomic(?a1) and neg subactivity(?a1, ?a2) and ?a2 :=: conc(?a1, ?a2).
subactivity(?a1, ?a2) :- atomic(?a1) and atomic(?a2) and ?a2 :=: conc(?a1, ?a2).
neg ?a2 :=: conc(?a1, ?a2) :- atomic(?a1) and atomic(?a2) and neg subactivity(?a1, ?a2).

neg atomic(?a1) :- atomic(?a2) and subactivity(?a1, ?a2) and neg ?a2 :=: conc(?a1, ?a2).
neg atomic(?a2) :- atomic(?a1) and subactivity(?a1, ?a2) and neg ?a2 :=: conc(?a1, ?a2).
neg subactivity(?a1, ?a2) :- atomic(?a1) and atomic(?a2) and neg ?a2 :=: conc(?a1, ?a2).
?a2 :=: conc(?a1, ?a2) :- atomic(?a1) and atomic(?a2) and subactivity(?a1, ?a2).
Axiom 7 An atomic action has a subactivity if and only if there exists another atomic activity which can be concurrently aggregated.

KIF
(forall (?a1 ?a2)
	(implies  (atomic ?a2)
		  (iff	(subactivity ?a1 ?a2)
			(exists (?a3)
				(= ?a2 (conc ?a1 ?a3))))))
SWSL-FOL
forall ?a1, ?a2
  ( atomic(?a2) ==>
    ( subactivity(?a1, ?a2) <==>
      exists ?a3
        ( ?a2 :=: conc(?a1, ?a3) ) ) ).
SWSL-Rules
neg atomic(?a2) :- subactivity(?a1,?a2) and neg ?a2 :=: conc(?a1,_#1(?a1,?a2)).
neg subactivity(?a1,?a2) :- atomic(?a2) and neg ?a2 :=: conc(?a1,_#1(?a1,?a2)).
?a2 :=: conc(?a1,_#1(?a1,?a2)) :- atomic(?a2) and subactivity(?a1,?a2).

neg atomic(?a2) :- neg subactivity(?a1,?a2) and ?a2 :=: conc(?a1,?a3).
subactivity(?a1,?a2) :- atomic(?a2) and ?a2 :=: conc(?a1,?a3).
neg ?a2 :=: conc(?a1,?a3) :- atomic(?a2) and neg subactivity(?a1,?a2).
Axiom 8 The semilattice of atomic activities is distributive.

KIF
(forall (?a ?b0 ?b1)
	(implies  (and	(subactivity ?a (conc ?b0 ?b1))
			(not (primitive ?a)))
		  (exists (?a0 ?a1)
			(and	(subactivity ?a0 ?a)
				(subactivity ?a1 ?a)
				(= ?a (conc ?a0 ?a1))))))
SWSL-FOL
forall ?a, ?b0, ?b1
  ( ( subactivity(?a, conc(?b0, ?b1)) and neg primitive(?a) ) ==>
    exists ?a0, ?a1
      ( subactivity(?a0, ?a) and
        subactivity(?a1, ?a) and
        ?a :=: conc(?a0, ?a1) ) ).
SWSL-Rules
neg subactivity(?a,conc(?b0,?b1)) :- neg primitive(?a) and neg subactivity(_#2(?a,?b0,?b1),?a).
primitive(?a) :- subactivity(?a,conc(?b0,?b1)) and neg subactivity(_#2(?a,?b0,?b1),?a).
subactivity(_#2(?a,?b0,?b1),?a) :- subactivity(?a,conc(?b0,?b1)) and neg primitive(?a).

neg subactivity(?a,conc(?b0,?b1)) :- neg primitive(?a) and neg subactivity(_#1(?a,?b0,?b1),?a).
primitive(?a) :- subactivity(?a,conc(?b0,?b1)) and neg subactivity(_#1(?a,?b0,?b1),?a).
subactivity(_#1(?a,?b0,?b1),?a) :- subactivity(?a,conc(?b0,?b1)) and neg primitive(?a).

neg subactivity(?a,conc(?b0,?b1)) :- neg primitive(?a) and neg ?a :=: conc(_#2(?a,?b0,?b1),_#1(?a,?b0,?b1)).
primitive(?a) :- subactivity(?a,conc(?b0,?b1)) and neg ?a :=: conc(_#2(?a,?b0,?b1),_#1(?a,?b0,?b1)).
?a :=: conc(_#2(?a,?b0,?b1),_#1(?a,?b0,?b1)) :- subactivity(?a,conc(?b0,?b1)) and neg primitive(?a).
Axiom 9 Only atomic activities can be elements of the legal occurrence tree.

KIF
(forall (?s ?a)
	(implies  (and	(occurrence ?s ?a)
			(legal ?s))
		  (atomic ?a)))
SWSL-FOL
forall ?s, ?a
  ( ( occurrence(?s, ?a) and legal(?s) ) ==>
    atomic(?a) ).
SWSL-Rules
neg occurrence(?s, ?a) :- legal(?s) and neg atomic(?a).
neg legal(?s) :- occurrence(?s, ?a) and neg atomic(?a).
atomic(?a) :- occurrence(?s, ?a) and legal(?s).


A.6 Theory of Complex Activities

Extension Name: complex.th
Theories Required by this Extension: occtree.th, atomic.th, subactivity.th, psl_core.th
Definitional Extensions Required by this Extension: None

Primitive Lexicon

KIF SWSL-FOL and SWSL-Rules

Defined Lexicon

KIF SWSL-FOL and SWSL-Rules

Axioms

Axiom 1 Occurrences in the activity tree for an activity correspond to atomic subactivity occurrences of the activity.

KIF
(forall (?a ?s1 ?s2)
	(implies  (min_precedes ?s1 ?s2 ?a)
		  (exists (?a1 ?ap)
			(and	(subactivity ?a1 ?a)
				(atomic ?ap)
				(subactivity ?a1 ?ap)
				(occurrence_of ?s2 ?ap)))))
SWSL-FOL
forall ?a, ?s1, ?s2
  min_precedes(?s1, ?s2, ?a) ==>
  exists ?a1, ?ap
    ( subactivity(?a1, ?a) and
      atomic(?ap) and
      subactivity(?a1, ?ap) and
      occurrence_of(?s2, ?ap) ).
SWSL-Rules
neg min_precedes(?s1, ?s2, ?a) :- neg subactivity(_#1(?a, ?s1, ?s2), ?a).
subactivity(_#1(?a, ?s1, ?s2), ?a) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg atomic(_#2(?a, ?s1, ?s2)).
atomic(_#2(?a, ?s1, ?s2)) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg subactivity(_#1(?a, ?s1, ?s2), _#2(?a, ?s1, ?s2)).
subactivity(_#1(?a, ?s1, ?s2), _#2(?a, ?s1, ?s2)) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg occurrence_of(?s2, _#2(?a, ?s1, ?s2)).
occurrence_of(?s2, _#2(?a, ?s1, ?s2)) :- min_precedes(?s1, ?s2, ?a).
Axiom 2 Occurrences in the activity tree for an activity correspond to atomic subactivity occurrences of the activity.

KIF
(forall (?a ?s1 ?s2)
	(implies  (min_precedes ?s1 ?s2 ?a)
		  (exists (?a2 ?ap)
			(and	(subactivity ?a2 ?a)
				(atomic ?ap)
				(subactivity ?a2 ?ap)
				(occurrence_of ?s1 ?ap)))))
SWSL-FOL
forall ?a, ?s1, ?s2
  ( min_precedes(?s1, ?s2, ?a) ==>
    exists ?a2, ?ap
      ( subactivity(?a2, ?a) and
        atomic(?ap) and
        subactivity(?a2, ?ap) and
        occurrence_of(?s1, ?ap) ) ).
SWSL-Rules
neg min_precedes(?s1, ?s2, ?a) :- neg subactivity(_#1(?a, ?s1, ?s2), ?a).
subactivity(_#1(?a, ?s1, ?s2), ?a) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg atomic(_#2(?a, ?s1, ?s2)).
atomic(_#2(?a, ?s1, ?s2)) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg subactivity(_#1(?a, ?s1, ?s2), _#2(?a, ?s1, ?s2)).
subactivity(_#1(?a, ?s1, ?s2), _#2(?a, ?s1, ?s2)) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg occurrence_of(?s1, _#2(?a, ?s1, ?s2)).
occurrence_of(?s1, _#2(?a, ?s1, ?s2)) :- min_precedes(?s1, ?s2, ?a).
Axiom 3 Root occurrences in the activity tree correspond to atomic subactivity occurrences of the activity.

KIF
(forall (?a ?s1)
	(implies  (root ?s1 ?a)
		  (exists (?a2 ?ap)
			(and	(subactivity ?a2 ?a)
				(atomic ?ap)
				(subactivity ?a2 ?ap)
				(occurrence_of ?s1 ?ap)))))
SWSL-FOL
forall ?a ?s1
  ( root(?s1 ?a) ==>
    exists ?a2 ?ap
      ( subactivity(?a2 ?a) and
        atomic(?ap) and
	subactivity(?a2 ?ap) and
        occurrence_of(?s1 ?ap) ) ).
SWSL-Rules
neg root(?s1, ?a) :- neg subactivity(_#1(?a, ?s1, ?s2), ?a).
subactivity(_#1(?a, ?s1, ?s2), ?a) :- root(?s1, ?a).

neg root(?s1, ?a) :- neg atomic(_#2(?a, ?s1, ?s2)).
atomic(_#2(?a, ?s1, ?s2)) :- root(?s1, ?a).

neg root(?s1, ?a) :- neg subactivity(_#1(?a, ?s1, ?s2), _#2(?a, ?s1, ?s2)).
subactivity(_#1(?a, ?s1, ?s2), _#2(?a, ?s1, ?s2)) :- root(?s1, ?a).

neg root(?s1, ?a) :- neg occurrence_of(?s1, _#2(?a, ?s1, ?s2)).
occurrence_of(?s1, _#2(?a, ?s1, ?s2)) :- root(?s1, ?a).
Axiom 4 All activity trees have a root subactivity occurrence.

KIF
(forall (?s1 ?s2 ?a)
	(implies  (min_precedes ?s1 ?s2 ?a)
		  (exists (?s3)
			(and	(root ?s3 ?a)
				(or	(min_precedes ?s3 ?s1 ?a)
					(= ?s3 ?s1))))))
SWSL-FOL
forall ?s1, ?s2, ?a
  ( min_precedes(?s1, ?s2, ?a) ==>
    exists ?s3
      ( root(?s3, ?a) and 
        ( min_precedes(?s3, ?s1, ?a) or ?s3 :=: ?s1 ) ) ).
SWSL-Rules
neg min_precedes(?s1,?s2,?a) :- neg root(_#1(?s1,?s2,?a),?a).
root(_#1(?s1,?s2,?a),?a) :- min_precedes(?s1,?s2,?a).

neg min_precedes(?s1,?s2,?a) :- neg min_precedes(_#1(?s1,?s2,?a),?s1,?a) and neg _#1(?s1,?s2,?a) :=: ?s1.
min_precedes(_#1(?s1,?s2,?a),?s1,?a) :- min_precedes(?s1,?s2,?a) and neg _#1(?s1,?s2,?a) :=: ?s1.
_#1(?s1,?s2,?a) :=: ?s1 :- min_precedes(?s1,?s2,?a) and neg min_precedes(_#1(?s1,?s2,?a),?s1,?a).
Axiom 5 No subactivity occurrences in an activity tree occur earlier than the root subactivity occurrence.

KIF
(forall (?s ?a)
	(implies  (root ?s ?a)
		  (not (exists (?s2)
			(min_precedes ?s2 ?s ?a)))))
SWSL-FOL
forall ?s, ?a
  ( root(?s, ?a) ==>
    neg exists ?s2
      ( min_precedes(?s2, ?s, ?a) ) ).
SWSL-Rules
neg root(?s, ?a) :- min_precedes(?s2, ?s, ?a).
neg min_precedes(?s2, ?s, ?a) :- root(?s, ?a).
Axiom 6 An activity tree is a subtree of the occurrence tree.

KIF
(forall (?s1 ?s2 ?a)
	(implies  (min_precedes ?s1 ?s2 ?a)
		  (exists (?s0)
			(and	(initial ?s0)
				(or	(precedes ?s0 ?s1)
					(= ?s0 ?s1))
				(precedes ?s1 ?s2)))))
SWSL-FOL
forall ?s1, ?s2, ?a
  ( min_precedes(?s1, ?s2, ?a) ==>
    exists ?s0
      ( initial(?s0) and
        ( precedes(?s0, ?s1) or ?s0 :=: ?s1 ) and
        precedes(?s1, ?s2) ) ).
SWSL-Rules
neg min_precedes(?s1, ?s2, ?a) :- neg initial(_#1(?s1,?s2,?a)).
initial(_#1(?s1,?s2,?a)) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg precedes(_#1(?s1,?s2,?a), ?s1) and neg _#1(?s1,?s2,?a) :=: ?s1.
precedes(_#1(?s1,?s2,?a), ?s1) :- min_precedes(?s1, ?s2, ?a) and neg _#1(?s1,?s2,?a) :=: ?s1.
_#1(?s1,?s2,?a) :=: ?s1 :- min_precedes(?s1, ?s2, ?a) and neg precedes(_#1(?s1,?s2,?a), ?s1).

neg min_precedes(?s1, ?s2, ?a) :- neg precedes(?s1, ?s2).
precedes(?s1, ?s2) :- min_precedes(?s1, ?s2, ?a).
Axiom 7 Root occurrences are elements of the occurrence tree.

KIF
(forall (?s ?a)
	(implies  (root ?s ?a)
		  (exists (?s0)
			(and	(initial ?s0)
				(or	(precedes ?s0 ?s)
					(= ?s0 ?s))))))
SWSL-FOL
forall ?s, ?a
  root(?s ?a) ==>
  exists ?s0
    ( initial(?s0) and
      ( precedes(?s0, ?s) or ?s0 :=: ?s ) ).
SWSL-Rules
neg root(?s ?a)  :- neg initial(_#1(?s,?a)).
initial(_#1(?s,?a)) :- root(?s ?a) .

neg root(?s ?a) :- neg precedes(_#1(?s,?a), ?s) and neg _#1(?s,?a) :=: ?s.
precedes(_#1(?s,?a), ?s) :- root(?s ?a) and neg _#1(?s,?a) :=: ?s.
_#1(?s,?a) :=: ?s :- root(?s ?a) and neg precedes(_#1(?s,?a), ?s).
Axiom 8 Every atomic activity occurrence is an activity tree containing only one occurrence.

KIF
(forall (?a1 ?a2 ?s)
        (implies  (and  (atomic ?a1)
                        (occurrence_of ?s ?a1)
			(subactivity ?a2 ?a1))
                  (root ?s ?a2)))
SWSL-FOL
forall ?a1, ?a2, ?s
  ( ( atomic(?a1) and occurrence_of(?s, ?a1) and subactivity(?a2, ?a1) ) ==>
    root(?s, ?a2) ).
SWSL-Rules
neg atomic(?a1) :- occurrence_of(?s, ?a1) and subactivity(?a2, ?a1) and neg root(?s, ?a2).
neg occurrence_of(?s, ?a1) :- atomic(?a1) and subactivity(?a2, ?a1) and neg root(?s, ?a2).
neg subactivity(?a2, ?a1) :- atomic(?a1) and occurrence_of(?s, ?a1) and neg root(?s, ?a2).
root(?s, ?a2) :- atomic(?a1) and occurrence_of(?s, ?a1) and subactivity(?a2, ?a1).
Axiom 9 Activity trees are discrete.

KIF
(forall (?s1 ?s2)
	(implies  (min_precedes ?s1 ?s2 ?a)
		  (exists (?s3)
			(and	(next_subocc ?s1 ?s3 ?a)
				(or	(min_precedes ?s3 ?s2 ?a)
					(= ?s3 ?s2))))))
SWSL-FOL
forall ?s1 ?s2
  ( min_precedes(?s1, ?s2, ?a) ==>
    exists ?s3
      ( next_subocc(?s1, ?s3, ?a) and
        ( min_precedes(?s3, ?s2, ?a) or ?s3 :=: ?s2 ) ) ).
SWSL-Rules
neg min_precedes(?s1, ?s2, ?a) :- neg next_subocc(?s1, _#1(?s1,?s2), ?a).
next_subocc(?s1, _#1(?s1,?s2), ?a) :- min_precedes(?s1, ?s2, ?a).

neg min_precedes(?s1, ?s2, ?a) :- neg min_precedes(_#1(?s1,?s2), ?s2, ?a) and neg _#1(?s1,?s2) :=: ?s2.
min_precedes(_#1(?s1,?s2), ?s2, ?a) :- min_precedes(?s1, ?s2, ?a) and neg _#1(?s1,?s2) :=: ?s2.
_#1(?s1,?s2) :=: ?s2 :- min_precedes(?s1, ?s2, ?a) and neg min_precedes(_#1(?s1,?s2), ?s2, ?a).
Axiom 10 Subactivity occurrences on the same branch of the occurrence tree are on the same branch of the activity tree.

KIF
(forall (?a ?s1 ?s2 ?s3)
	(implies  (and	(min_precedes ?s1 ?s2 ?a)
			(min_precedes ?s1 ?s3 ?a)
			(precedes ?s2 ?s3))
		  (min_precedes ?s2 ?s3 ?a)))
SWSL-FOL
forall ?a, ?s1, ?s2, ?s3
  ( ( min_precedes(?s1, ?s2, ?a) and
      min_precedes(?s1, ?s3, ?a) and
      precedes(?s2, ?s3) ) ==>
    min_precedes(?s2, ?s3, ?a) ).
SWSL-Rules
neg min_precedes(?s1, ?s2, ?a) :- min_precedes(?s1, ?s3, ?a) and precedes(?s2, ?s3) and neg min_precedes(?s2, ?s3, ?a).
neg min_precedes(?s1, ?s3, ?a) :- min_precedes(?s1, ?s2, ?a) and precedes(?s2, ?s3) and neg min_precedes(?s2, ?s3, ?a).
neg precedes(?s2, ?s3) :- min_precedes(?s1, ?s2, ?a) and min_precedes(?s1, ?s3, ?a) and neg min_precedes(?s2, ?s3, ?a).
min_precedes(?s2, ?s3, ?a) :- min_precedes(?s1, ?s2, ?a) and min_precedes(?s1, ?s3, ?a) and precedes(?s2, ?s3).
Axiom 11 The activity tree for a complex subactivity occurrence is a subtree of the activity tree for the activity occurrence.

KIF
(forall (?a1 ?a2)
	(implies  (subactivity ?a1 ?a2)
		  (not (exists (?s)
			(subtree ?s ?a2 ?a1)))))
SWSL-FOL
forall ?a1, ?a2
  ( subactivity(?a1, ?a2) ==>
    neg exists ?s
          ( subtree(?s, ?a2, ?a1) ) ).
SWSL-Rules
neg subactivity(?a1, ?a2) :- subtree(?s, ?a2, ?a1).
neg subtree(?s, ?a2, ?a1) :- subactivity(?a1, ?a2).

Definitions

Definition 1 An occurrence is the leaf of an activity tree if and only if there exists an earlier atomic subactivity occurrence but there does not exist a later atomic subactivity occurrence.

KIF
(forall (?s ?a) (iff (leaf ?s ?a)
(exists (?s1)
	(and	(or	(root ?s ?a)
			(min_precedes ?s1 ?s ?a))
		(not (exists (?s2)
			(min_precedes ?s ?s2 ?a)))))))
SWSL-FOL
forall ?s ?a  
  ( leaf(?s, ?a) <==>
    exists ?s1
      ( ( root(?s, ?a) or min_precedes(?s1, ?s, ?a) ) and
        neg exists ?s2
              ( min_precedes(?s, ?s2, ?a) ) ) ).
SWSL-Rules
neg leaf(?s,?a) :- neg root(?s,?a) and neg min_precedes(_#1(?s,?a),?s,?a).
root(?s,?a) :- leaf(?s,?a) and neg min_precedes(_#1(?s,?a),?s,?a).
min_precedes(_#1(?s,?a),?s,?a) :- leaf(?s,?a) and neg root(?s,?a).

neg leaf(?s,?a) :- min_precedes(?s,?s2,?a).
neg min_precedes(?s,?s2,?a) :- leaf(?s,?a).

leaf(?s,?a) :- root(?s,?a) and neg min_precedes(?s,_#2(?s,?a,?s1),?a).
neg root(?s,?a) :- neg leaf(?s,?a) and neg min_precedes(?s,_#2(?s,?a,?s1),?a).
min_precedes(?s,_#2(?s,?a,?s1),?a) :- neg leaf(?s,?a) and root(?s,?a).

leaf(?s,?a) :- min_precedes(?s1,?s,?a) and neg min_precedes(?s,_#2(?s,?a,?s1),?a).
neg min_precedes(?s1,?s,?a) :- neg leaf(?s,?a) and neg min_precedes(?s,_#2(?s,?a,?s1),?a).
min_precedes(?s,_#2(?s,?a,?s1),?a) :- neg leaf(?s,?a) and min_precedes(?s1,?s,?a).
Definition 2 The do relation specifies the initial and final atomic subactivity occurrences of an occurrence of an activity.

KIF
(forall (?a ?s1 ?s2) (iff (do ?a ?s1 ?s2)
(and	(root ?s1 ?a)
	(leaf ?s2 ?a)
	(or	(min_precedes ?s1 ?s2 ?a)
		(= ?s1 ?s2)))))
SWSL-FOL
forall ?a, ?s1, ?s2
  ( do(?a, ?s1, ?s2) <==>
    ( root(?s1, ?a) and
      leaf(?s2, ?a) and
      ( min_precedes(?s1, ?s2, ?a) or ?s1 :=: ?s2) ) ).
SWSL-Rules
neg do(?a,?s1,?s2) :- neg root(?s1,?a).
root(?s1,?a) :- do(?a,?s1,?s2).

neg do(?a,?s1,?s2) :- neg leaf(?s2,?a).
leaf(?s2,?a) :- do(?a,?s1,?s2).

neg do(?a,?s1,?s2) :- neg min_precedes(?s1,?s2,?a) and neg ?s1 :=: ?s2.
min_precedes(?s1,?s2,?a) :- do(?a,?s1,?s2) and neg ?s1 :=: ?s2.
?s1 :=: ?s2 :- do(?a,?s1,?s2) and neg min_precedes(?s1,?s2,?a).

do(?a,?s1,?s2) :- root(?s1,?a) and leaf(?s2,?a) and min_precedes(?s1,?s2,?a).
neg root(?s1,?a) :- neg do(?a,?s1,?s2) and leaf(?s2,?a) and min_precedes(?s1,?s2,?a).
neg leaf(?s2,?a) :- neg do(?a,?s1,?s2) and root(?s1,?a) and min_precedes(?s1,?s2,?a).
neg min_precedes(?s1,?s2,?a) :- neg do(?a,?s1,?s2) and root(?s1,?a) and leaf(?s2,?a).

do(?a,?s1,?s2) :- root(?s1,?a) and leaf(?s2,?a) and ?s1 :=: ?s2.
neg root(?s1,?a) :- neg do(?a,?s1,?s2) and leaf(?s2,?a) and ?s1 :=: ?s2.
neg leaf(?s2,?a) :- neg do(?a,?s1,?s2) and root(?s1,?a) and ?s1 :=: ?s2.
neg ?s1 :=: ?s2 :- neg do(?a,?s1,?s2) and root(?s1,?a) and leaf(?s2,?a).
Definition 3 An activity occurrence ?s2 is the next subactivity occurrence after ?s1 in an activity tree for ?a if and only of ?s1 precedes ?s2 in the tree and there does not exist a subactivity occurrence that is between them in the tree.

KIF
(forall (?s1 ?s2 ?a) (iff (next_subocc ?s1 ?s2 ?a)
(and    (min_precedes ?s1 ?s2 ?a)
        (not (exists (?s3)
                (and    (min_precedes ?s1 ?s3 ?a)
                        (min_precedes ?s3 ?s2 ?a)))))))
SWSL-FOL
forall ?s1, ?s2, ?a
  ( next_subocc(?s1, ?s2, ?a) <==>
    ( min_precedes(?s1, ?s2, ?a) and
      neg exists ?s3
            ( min_precedes(?s1, ?s3, ?a) and
              min_precedes(?s3, ?s2, ?a) ) ) ).
SWSL-Rules
neg next_subocc(?s1,?s2,?a) :- neg min_precedes(?s1,?s2,?a).
min_precedes(?s1,?s2,?a) :- next_subocc(?s1,?s2,?a).

neg next_subocc(?s1,?s2,?a) :- min_precedes(?s1,?s3,?a) and min_precedes(?s3,?s2,?a).
neg min_precedes(?s1,?s3,?a) :- next_subocc(?s1,?s2,?a) and min_precedes(?s3,?s2,?a).
neg min_precedes(?s3,?s2,?a) :- next_subocc(?s1,?s2,?a) and min_precedes(?s1,?s3,?a).

next_subocc(?s1,?s2,?a) :- min_precedes(?s1,?s2,?a) and neg min_precedes(?s1,_#1(?s1,?s2,?a),?a).
neg min_precedes(?s1,?s2,?a) :- neg next_subocc(?s1,?s2,?a) and neg min_precedes(?s1,_#1(?s1,?s2,?a),?a).
min_precedes(?s1,_#1(?s1,?s2,?a),?a) :- neg next_subocc(?s1,?s2,?a) and min_precedes(?s1,?s2,?a).

next_subocc(?s1,?s2,?a) :- min_precedes(?s1,?s2,?a) and neg min_precedes(_#1(?s1,?s2,?a),?s2,?a).
neg min_precedes(?s1,?s2,?a) :- neg next_subocc(?s1,?s2,?a) and neg min_precedes(_#1(?s1,?s2,?a),?s2,?a).
min_precedes(_#1(?s1,?s2,?a),?s2,?a) :- neg next_subocc(?s1,?s2,?a) and min_precedes(?s1,?s2,?a).
Definition 4 The activity tree for ?a1 with root occurrence ?s1 is a subtree of an activity tree for ?a2 if and only if every atomic asubactivity occurrence in the activity tree for ?a1 is an element of the activity tree for ?a2.

KIF
(forall (?s1 ?a1 ?a2) (iff (subtree ?s1 ?a1 ?a2)
(and	(root ?s1 ?a1)
	(exists (?s2 ?s3)
		(and	(root ?s2 ?a2)
			(min_precedes ?s1 ?s2 ?a1)
		    	(min_precedes ?s1 ?s3 ?a1)
			(not (min_precedes ?s2 ?s3 ?a2)))))))
SWSL-FOL
forall ?s1, ?a1, ?a2
  ( subtree(?s1, ?a1, ?a2) <==>
    ( root(?s1, ?a1) and
      exists ?s2, ?s2
        ( root(?s2, ?a2) and min_precedes(?s1, ?s2, ?a1) ) and
        ( min_precedes(?s1, ?s3, ?a1) and neg min_precedes(?s2, ?s3, ?a2) ) ) ).
SWSL-Rules
neg subtree(?s1,?a1,?a2) :- neg root(?s1,?a1).
root(?s1,?a1) :- subtree(?s1,?a1,?a2).

neg subtree(?s1,?a1,?a2) :- neg root(_#2(?s1,?a1,?a2),?a2).
root(_#2(?s1,?a1,?a2),?a2) :- subtree(?s1,?a1,?a2).

neg subtree(?s1,?a1,?a2) :- neg min_precedes(?s1,_#2(?s1,?a1,?a2),?a1).
min_precedes(?s1,_#2(?s1,?a1,?a2),?a1) :- subtree(?s1,?a1,?a2).

neg subtree(?s1,?a1,?a2) :- neg min_precedes(?s1,_#1(?s1,?a1,?a2),?a1).
min_precedes(?s1,_#1(?s1,?a1,?a2),?a1) :- subtree(?s1,?a1,?a2).

neg subtree(?s1,?a1,?a2) :- min_precedes(_#2(?s1,?a1,?a2),_#1(?s1,?a1,?a2),?a2).
neg min_precedes(_#2(?s1,?a1,?a2),_#1(?s1,?a1,?a2),?a2) :- subtree(?s1,?a1,?a2).

subtree(?s1,?a1,?a2) :- root(?s1,?a1) and root(?s2,?a2) and min_precedes(?s1,?s2,?a1) and min_precedes(?s1,?s3,?a1) and neg min_precedes(?s2,?s3,?a2).
neg root(?s1,?a1) :- neg subtree(?s1,?a1,?a2) and root(?s2,?a2) and min_precedes(?s1,?s2,?a1) and min_precedes(?s1,?s3,?a1) and neg min_precedes(?s2,?s3,?a2).
neg root(?s2,?a2) :- neg subtree(?s1,?a1,?a2) and root(?s1,?a1) and min_precedes(?s1,?s2,?a1) and min_precedes(?s1,?s3,?a1) and neg min_precedes(?s2,?s3,?a2).
neg min_precedes(?s1,?s2,?a1) :- neg subtree(?s1,?a1,?a2) and root(?s1,?a1) and root(?s2,?a2) and min_precedes(?s1,?s3,?a1) and neg min_precedes(?s2,?s3,?a2).
neg min_precedes(?s1,?s3,?a1) :- neg subtree(?s1,?a1,?a2) and root(?s1,?a1) and root(?s2,?a2) and min_precedes(?s1,?s2,?a1) and neg min_precedes(?s2,?s3,?a2).
min_precedes(?s2,?s3,?a2) :- neg subtree(?s1,?a1,?a2) and root(?s1,?a1) and root(?s2,?a2) and min_precedes(?s1,?s2,?a1) and min_precedes(?s1,?s3,?a1).
Definition 5 The atomic subactivity occurrences ?s1 and ?s2 are siblings in an activity tree for ?a iff they either have a common predecessor in the activity tree or they are both roots of activity trees that have a common predecessor in the occurrence tree.

KIF
(forall (?s1 ?s2 ?a) (iff (sibling ?s1 ?s2 ?a)
(or	(exists (?s3)
		(and	(next_subocc ?s3 ?s1 ?a)
			(next_subocc ?s3 ?s2 ?a)))
	(and	(root ?s1 ?a)
		(root ?s2 ?a)
		(or	(and	(initial ?s1)
				(initial ?s2))
			(exists (?s4 ?a1 ?a2)
				(and	(= ?s1 (successor ?a1 ?s4))
					(= ?s2 (successor ?a2 ?s4)))))))))
SWSL-FOL
forall ?s1, ?s2, ?a
  ( sibling(?s1, ?s2, ?a) <==>
    ( exists ?s3
        ( next_subocc(?s3, ?s1, ?a) and next_subocc(?s3, ?s2, ?a) ) or
      ( root(?s1, ?a) and
        root(?s2, ?a) and
        ( ( initial(?s1) and initial(?s2) ) or
          exists ?s4, ?a1, ?a2
            ( ?s1 :=: successor(?a1, ?s4) and 
              ?s2 :=: successor(?a2, ?s4) ) ) ) ) ).
SWSL-Rules
neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg root(?s1,?a).
next_subocc(_#1(?s1,?s2,?a),?s1,?a) :- sibling(?s1,?s2,?a) and neg root(?s1,?a).
root(?s1,?a) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg root(?s2,?a).
next_subocc(_#1(?s1,?s2,?a),?s1,?a) :- sibling(?s1,?s2,?a) and neg root(?s2,?a).
root(?s2,?a) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s1) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s1,?a) :- sibling(?s1,?s2,?a) and neg initial(?s1) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s1) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s1).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s1) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s1,?a) :- sibling(?s1,?s2,?a) and neg initial(?s1) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s1) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s1).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s2) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s1,?a) :- sibling(?s1,?s2,?a) and neg initial(?s2) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s2) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s2).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s2) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s1,?a) :- sibling(?s1,?s2,?a) and neg initial(?s2) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s2) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s1,?a) and neg initial(?s2).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg root(?s1,?a).
next_subocc(_#1(?s1,?s2,?a),?s2,?a) :- sibling(?s1,?s2,?a) and neg root(?s1,?a).
root(?s1,?a) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg root(?s2,?a).
next_subocc(_#1(?s1,?s2,?a),?s2,?a) :- sibling(?s1,?s2,?a) and neg root(?s2,?a).
root(?s2,?a) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s1) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s2,?a) :- sibling(?s1,?s2,?a) and neg initial(?s1) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s1) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s1).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s1) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s2,?a) :- sibling(?s1,?s2,?a) and neg initial(?s1) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s1) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s1).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s2) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s2,?a) :- sibling(?s1,?s2,?a) and neg initial(?s2) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s2) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg ?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s1 :=: successor(_#3(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s2).

neg sibling(?s1,?s2,?a) :- neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s2) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
next_subocc(_#1(?s1,?s2,?a),?s2,?a) :- sibling(?s1,?s2,?a) and neg initial(?s2) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
initial(?s2) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg ?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)).
?s2 :=: successor(_#2(?s1,?s2,?a),_#4(?s1,?s2,?a)) :- sibling(?s1,?s2,?a) and neg next_subocc(_#1(?s1,?s2,?a),?s2,?a) and neg initial(?s2).

sibling(?s1,?s2,?a) :- next_subocc(?s3,?s1,?a) and next_subocc(?s3,?s2,?a).
neg next_subocc(?s3,?s1,?a) :- neg sibling(?s1,?s2,?a) and next_subocc(?s3,?s2,?a).
neg next_subocc(?s3,?s2,?a) :- neg sibling(?s1,?s2,?a) and next_subocc(?s3,?s1,?a).

neg sibling(?s1,?s2,?a) :- root(?s1,?a) and root(?s2,?a) and initial(?s1) and initial(?s2).
root(?s1,?a) :- neg sibling(?s1,?s2,?a) and root(?s2,?a) and initial(?s1) and initial(?s2).
root(?s2,?a) :- neg sibling(?s1,?s2,?a) and root(?s1,?a) and initial(?s1) and initial(?s2).
initial(?s1) :- neg sibling(?s1,?s2,?a) and root(?s1,?a) and root(?s2,?a) and initial(?s2).
initial(?s2) :- neg sibling(?s1,?s2,?a) and root(?s1,?a) and root(?s2,?a) and initial(?s1).

neg sibling(?s1,?s2,?a) :- root(?s1,?a) and root(?s2,?a) and neg ?s1! :=: successor(?a1,?s4) and neg ?s2! :=: successor(?a2,?s4).
root(?s1,?a) :- neg sibling(?s1,?s2,?a) and root(?s2,?a) and neg ?s1! :=: successor(?a1,?s4) and neg ?s2! :=: successor(?a2,?s4).
root(?s2,?a) :- neg sibling(?s1,?s2,?a) and root(?s1,?a) and neg ?s1! :=: successor(?a1,?s4) and neg ?s2! :=: successor(?a2,?s4).
neg ?s1! :=: successor(?a1,?s4) :- neg sibling(?s1,?s2,?a) and root(?s1,?a) and root(?s2,?a) and neg ?s2! :=: successor(?a2,?s4).
neg ?s2! :=: successor(?a2,?s4) :- neg sibling(?s1,?s2,?a) and root(?s1,?a) and root(?s2,?a) and neg ?s1! :=: successor(?a1,?s4).