(define-theory planning (Unrestricted-Time diagrams meronymy))
(in-theory 'planning)


(DEFINE-RELATION CLOSES-AT (?A ?B) :DEF (PLANNING-RELATION ?A ?B)
 :AXIOM-CONSTRAINTS
 (AND (RANGE CLOSES-AT GENERIC-PLAN)
      (DOMAIN CLOSES-AT GENERIC-PLAN)))
(DEFINE-RELATION EXIT-CONDITION (?A ?B) :DEF (POSTCONDITION ?A ?B))
(DEFINE-RELATION EXIT-CONDITION-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE EXIT-CONDITION) EXIT-CONDITION-OF)
      (SITUATION ?A)
      (ABSTRACTION ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE EXIT-CONDITION-OF ABSTRACTION)
      (DOMAIN EXIT-CONDITION-OF SITUATION)))
(DEFINE-RELATION FIRST-PLAN (?A ?B) :IFF-DEF
 (AND (= (INVERSE FIRST-PLAN-OF) FIRST-PLAN)
      (GENERIC-PLAN ?A)
      (GENERIC-PLAN ?B))
 :CONSTRAINTS (AND (GENERIC-PLAN ?A) (GENERIC-PLAN ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE FIRST-PLAN GENERIC-PLAN)
      (DOMAIN FIRST-PLAN GENERIC-PLAN)))
(DEFINE-RELATION FIRST-PLAN-OF (?A ?B) :IFF-DEF
 (AND (NOT (EXISTS ?W (AND (GENERIC-PLAN ?W) (PLAN-PREDECESSOR ?A ?W))))
      (PLANNING-RELATION ?A ?B)
      (GENERIC-PLAN ?A)
      (GENERIC-PLAN ?B)))
(DEFINE-RELATION INVERSE-OF-PLANNING-RELATION (?A ?B) :IFF-DEF
 (= (INVERSE PLANNING-RELATION) INVERSE-OF-PLANNING-RELATION))
(DEFINE-RELATION IS-CLOSING-OF (?A ?B) :IFF-DEF
 (= (INVERSE CLOSES-AT) IS-CLOSING-OF))
(DEFINE-RELATION IS-OPENING-OF (?A ?B) :IFF-DEF
 (= (INVERSE OPENS-AT) IS-OPENING-OF))
(DEFINE-RELATION IS-PLAN-SUBDIVISION (?A ?B))
(DEFINE-FUNCTION ITERATED-FOR (?A) :-> ?B :DEF (NUMERIC-VALUE ?A ?B)
 :AXIOM-DEF (FUNCTION ITERATED-FOR) :AXIOM-CONSTRAINTS
 (RANGE ITERATED-FOR INTEGER))
(DEFINE-RELATION ITERATION-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE ITERATED-FOR) ITERATION-VALUE-OF))
(DEFINE-RELATION LAST-PLAN (?A ?B) :IFF-DEF
 (AND (= (INVERSE LAST-PLAN-OF) LAST-PLAN)
      (GENERIC-PLAN ?A)
      (GENERIC-PLAN ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE LAST-PLAN GENERIC-PLAN)
      (DOMAIN LAST-PLAN GENERIC-PLAN)))
(DEFINE-RELATION LAST-PLAN-OF (?A ?B) :DEF
 (AND (PLANNING-RELATION ?A ?B) (GENERIC-PLAN ?A) (GENERIC-PLAN ?B))
 :CONSTRAINTS
 (NOT (EXISTS ?W (AND (GENERIC-PLAN ?W) (PLAN-SUCCESSOR ?A ?W)))))
(DEFINE-RELATION OPENS-AT (?A ?B) :DEF (PLANNING-RELATION ?A ?B)
 :AXIOM-CONSTRAINTS
 (AND (RANGE OPENS-AT GENERIC-PLAN)
      (DOMAIN OPENS-AT GENERIC-PLAN)))
(DEFINE-RELATION PLAN-DIRECT-PREDECESSOR (?A ?B) :IFF-DEF
 (AND (= (INVERSE PLAN-DIRECT-SUCCESSOR) PLAN-DIRECT-PREDECESSOR)
      (GENERIC-PLAN ?A)
      (GENERIC-PLAN ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE PLAN-DIRECT-PREDECESSOR GENERIC-PLAN)
      (DOMAIN PLAN-DIRECT-PREDECESSOR GENERIC-PLAN)))
(DEFINE-RELATION PLAN-DIRECT-SUCCESSOR (?A ?B) :DEF
 (PLAN-SUCCESSOR ?A ?B))
(DEFINE-RELATION PLAN-PREDECESSOR (?A ?B)
 "To be understood as 'plan part x 
has predecessor y'. This is transitive."
 :IFF-DEF
 (AND (= (INVERSE PLAN-SUCCESSOR) PLAN-PREDECESSOR)
      (GENERIC-PLAN ?A)
      (GENERIC-PLAN ?B))
 :CONSTRAINTS (AND (GENERIC-PLAN ?A) (GENERIC-PLAN ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE PLAN-PREDECESSOR GENERIC-PLAN)
      (DOMAIN PLAN-PREDECESSOR GENERIC-PLAN)))
(DEFINE-RELATION PLAN-SUBDIVISION (?A ?B) :DEF (BINARY-TUPLE ?A ?B))
(DEFINE-RELATION PLAN-SUCCESSOR (?A ?B)
 "To be understood as 'plan part x 
has successor y'. This is transitive."
 :DEF (AND (PLANNING-RELATION ?A ?B) (GENERIC-PLAN ?A) (GENERIC-PLAN ?B))
 :CONSTRAINTS (AND (GENERIC-PLAN ?A) (GENERIC-PLAN ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE PLAN-SUCCESSOR GENERIC-PLAN)
      (DOMAIN PLAN-SUCCESSOR GENERIC-PLAN)))
(DEFINE-RELATION PLANNING-PROPERTY (?A ?B) :DEF
 (AND (TYPICALITY-PROPERTY ?A ?B) (GENERIC-PLAN ?A)))
(DEFINE-RELATION PLANNING-RELATION (?A ?B) :DEF
 (STRUCTURING-RELATION ?A ?B))
(DEFINE-RELATION POSTCONDITION (?A ?B) :DEF
 (AND (PLANNING-RELATION ?A ?B)
      (EXISTS (?C) (AND (METHOD-OF ?A ?C) (OUTCOME ?C ?B)))
      (SITUATION ?B)))
(DEFINE-RELATION POSTCONDITION-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE POSTCONDITION) POSTCONDITION-OF)
      (SITUATION ?A)
      (ABSTRACTION ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE POSTCONDITION-OF ABSTRACTION)
      (DOMAIN POSTCONDITION-OF SITUATION)))
(DEFINE-RELATION PRECONDITION (?A ?B) :DEF
 (AND (PLANNING-RELATION ?A ?B)
      (EXISTS (?C) (AND (METHOD-OF ?A ?C) (FOLLOWS ?C ?B)))
      (GENERIC-PLAN ?A)
      (SITUATION ?B)))
(DEFINE-RELATION PRECONDITION-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE PRECONDITION) PRECONDITION-OF)
      (SITUATION ?A)
      (GENERIC-PLAN ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE PRECONDITION-OF GENERIC-PLAN)
      (DOMAIN PRECONDITION-OF SITUATION)))
(DEFINE-FUNCTION REPETITION-INTERVAL (?A) :-> ?B :DEF
 (DURATION-VALUE ?A ?B))
(DEFINE-RELATION REPETITION-INTERVAL-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE REPETITION-INTERVAL) REPETITION-INTERVAL-OF)
      (NUMBER ?A))
 :AXIOM-CONSTRAINTS
 (DOMAIN REPETITION-INTERVAL-OF NUMBER))
(DEFINE-RELATION SIBLING-PLAN (?A ?B)
 "Two plans contained in the same plan." :DEF
 (AND (EXISTS (?C) (AND (PART-OF ?A ?C) (PART ?C ?B)))
      (ENTITY ?A)
      (ENTITY ?B)
      (PLANNING-RELATION ?A ?B)
      (GENERIC-PLAN ?A)
      (GENERIC-PLAN ?B))
 :CONSTRAINTS (AND (GENERIC-PLAN ?A) (GENERIC-PLAN ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE SIBLING-PLAN GENERIC-PLAN)
      (DOMAIN SIBLING-PLAN GENERIC-PLAN)))
(DEFINE-RELATION _ACCEPTED (?A ?B) :DEF (PLANNING-PROPERTY ?A ?B))
(DEFINE-RELATION _CONSIDERED (?A ?B) :DEF (PLANNING-PROPERTY ?A ?B))
(DEFINE-RELATION _POSSIBLE (?A ?B) :DEF (PLANNING-PROPERTY ?A ?B))
(DEFINE-RELATION _REJECTED (?A ?B) :DEF (PLANNING-PROPERTY ?A ?B))
(DEFINE-CLASS ALTERNATE-PLAN (?SELF)
 "A case plan branched to exactly 2 plans not executable in 
parallel."
 :DEF
 (AND (CASE-PLAN ?SELF)
      (VALUE-CARDINALITY ?SELF PLAN-DIRECT-SUCCESSOR 2)))
(DEFINE-CLASS ANY-ORDER-PLAN (?SELF)
:DEF
 (AND (CONCURRENT-PLAN ?SELF)
      (EXISTS (?A)
              (AND (PLAN-DIRECT-SUCCESSOR ?SELF ?A) (SEQUENTIAL-PLAN ?A)))))
(DEFINE-CLASS BRANCHING-PLAN (?SELF)
 "A plan that subdivides in a set of plans." :DEF
 (AND (ELEMENTARY-PLAN ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF PLAN-DIRECT-SUCCESSOR 2))
 :CONSTRAINTS
 (AND (EXISTS (?A) (AND (REPRESENTED-BY ?SELF ?A) (FORK-NODE ?A)))
      (EXISTS (?B) (AND (METHOD-OF ?SELF ?B) (PLANNING-STAGE ?B)))))
(DEFINE-CLASS CASE-PLAN (?SELF)
 "A plan branched to a set of plans not executable in 
parallel."
 :DEF
 (AND (BRANCHING-PLAN ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF PLAN-DIRECT-SUCCESSOR 2))
 :CONSTRAINTS
 (AND (EXISTS (?A) (AND (METHOD-OF ?SELF ?A) (CASE-STAGE ?A)))
      (EXISTS (?B) (AND (REPRESENTED-BY ?SELF ?B) (FORK-NODE ?B)))))
(DEFINE-CLASS COMPLEX-PLAN (?SELF)
:IFF-DEF
 (AND (GENERIC-PLAN ?SELF) (MINIMUM-SLOT-CARDINALITY ?SELF PART 2))
:AXIOM-DEF
 (SUBCLASS-PARTITION COMPLEX-PLAN
  (SETOF SEQUENTIAL-PLAN CYCLICAL-PLAN)))
(DEFINE-CLASS CONCURRENT-PLAN (?SELF)
 "A branching plan to a set of plans executable concurrently." :DEF
 (AND (BRANCHING-PLAN ?SELF)
      (EXISTS (?A) (AND (METHOD-OF ?SELF ?A) (CONCURRENT-STAGE ?A)))))
(DEFINE-CLASS CYCLE-FOR (?SELF)
:DEF
 (AND (CYCLICAL-PLAN ?SELF)
      (VALUE-CARDINALITY ?SELF ITERATED-FOR 1)
      (VALUE-TYPE ?SELF ITERATED-FOR INTEGER))
 :CONSTRAINTS (VALUE-TYPE ?SELF REPETITION-INTERVAL NUMBER))
(DEFINE-CLASS CYCLE-UNTIL (?SELF)
 "A cyclical plan which iterates until a certain condition
becomes true. It can be repeated after a certain repetition interval."
 :DEF
 (AND (CYCLICAL-PLAN ?SELF)
      (EXISTS (?A) (AND (EXIT-CONDITION ?SELF ?A) (SITUATION ?A))))
 :CONSTRAINTS (VALUE-TYPE ?SELF REPETITION-INTERVAL NUMBER))
(DEFINE-CLASS CYCLICAL-PLAN (?SELF)
 "A plan containing at least a cycle." :DEF
 (AND (COMPLEX-PLAN ?SELF)
      (EXISTS (?A)
              (AND (REPRESENTED-BY ?SELF ?A)
                   (AND (FLOW-CHART ?A)
                        (EXISTS (?B)
                         (AND (FIRST-NODE ?A ?B) (CYCLE-NODE ?B)))
                        (FORALL (?B ?C)
                         (=> (AND (FIRST-NODE ?A ?B) (FIRST-NODE ?A ?C))
                          (= ?B ?C)))))))
 :CONSTRAINTS (EXISTS (?D) (AND (METHOD-OF ?SELF ?D) (ACT-STAGE ?D)))
 :AXIOM-DEF (SUBCLASS-PARTITION CYCLICAL-PLAN (SETOF CYCLE-UNTIL CYCLE-FOR)))
(DEFINE-CLASS ELEMENTARY-PLAN (?SELF)
 "A plan that does not contain compacted plans (ie, subplans
represented by a simple node that can be expanded into a flow-chart)."
 :DEF (AND (GENERIC-PLAN ?SELF) (VALUE-TYPE ?SELF PART INCOHERENT)))
(DEFINE-CLASS GENERIC-PLAN (?SELF)
 "A generic plan is a script that contains the 
method for executing or performing a procedure or a stage of a procedure."
 :DEF
 (AND (SCRIPT ?SELF)
      (FORALL (?A)
       (=> (METHOD-OF ?SELF ?A) (OR (PROCEDURE ?A) (STAGE ?A)))))
 :CONSTRAINTS
 (AND (EXISTS (?B) (AND (REPRESENTED-BY ?SELF ?B) (DOCUMENT ?B)))
      (EXISTS (?C) (AND (PART ?SELF ?C) (GENERIC-PLAN ?C)))
      (VALUE-TYPE ?SELF PART-OF GENERIC-PLAN)
      (VALUE-TYPE ?SELF SERIAL-VALUE SERIAL-VALUE-FILLER)
      (VALUE-TYPE ?SELF TITLE SYMBOLIC-STRING)
      (VALUE-TYPE ?SELF PRECONDITION SITUATION)
      (VALUE-TYPE ?SELF AUTHORED-BY PLAN-AUTHOR)
      (VALUE-TYPE ?SELF DURATION-VALUE NUMBER)
      (VALUE-TYPE ?SELF DESCRIPTION SYMBOLIC-STRING)
      (VALUE-TYPE ?SELF POSTCONDITION SITUATION))
 :AXIOM-DEF
 (SUBCLASS-PARTITION GENERIC-PLAN
  (SETOF ELEMENTARY-PLAN COMPLEX-PLAN SYNCHRO-PLAN)))
(DEFINE-CLASS PARALLEL-PLAN (?SELF)
:DEF
 (AND (CONCURRENT-PLAN ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF PLAN-DIRECT-SUCCESSOR 2))
 :CONSTRAINTS
 (EXISTS (?Y ?Z)
  (AND (GENERIC-PLAN ?Y)
       (GENERIC-PLAN ?Z)
       (CO-EXIST ?Y ?Z)
       (PLAN-DIRECT-SUCCESSOR ?SELF ?Y)
       (PLAN-DIRECT-SUCCESSOR ?SELF ?Z))))
(DEFINE-CLASS PARTLY-ANY-ORDER-PLAN (?SELF)
:DEF
 (AND (PARTLY-CONCURRENT-PLAN ?SELF)
      (EXISTS (?A)
              (AND (PLAN-DIRECT-SUCCESSOR ?SELF ?A) (SEQUENTIAL-PLAN ?A)))))
(DEFINE-CLASS PARTLY-CONCURRENT-PLAN (?SELF)
 "A branching plan to a set of plans, some of which are executable 
concurrently."
 :DEF
 (AND (BRANCHING-PLAN ?SELF)
      (EXISTS (?A) (AND (METHOD-OF ?SELF ?A) (PARTLY-CONCURRENT-STAGE ?A)))))
(DEFINE-CLASS PARTLY-PARALLEL-PLAN (?SELF)
:DEF
 (AND (PARTLY-CONCURRENT-PLAN ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF PLAN-DIRECT-SUCCESSOR 2))
 :CONSTRAINTS
 (EXISTS (?Y ?Z)
  (AND (GENERIC-PLAN ?Y)
       (GENERIC-PLAN ?Z)
       (CO-EXIST ?Y ?Z)
       (PLAN-DIRECT-SUCCESSOR ?SELF ?Y)
       (PLAN-DIRECT-SUCCESSOR ?SELF ?Z))))
(DEFINE-CLASS PLAN-AUTHOR (?SELF)
:IFF-DEF
 (AND (THING ?SELF)
      (OR (PERSON ?SELF) (ORGANIZATION ?SELF))
      (EXISTS (?A) (AND (AUTHORS ?SELF ?A) (GENERIC-PLAN ?A)))))
(DEFINE-CLASS SEQUENTIAL-PLAN (?SELF)
 "A plan that does not contain branchings
nor synchronizations, nor cycles."
 :DEF
 (AND (COMPLEX-PLAN ?SELF)
      (VALUE-TYPE ?SELF PART INCOHERENT)
      (VALUE-TYPE ?SELF PART INCOHERENT)
      (VALUE-TYPE ?SELF PART INCOHERENT))
 :CONSTRAINTS
 (AND (EXISTS (?A)
              (AND (REPRESENTED-BY ?SELF ?A)
                   (AND (FLOW-CHART ?A)
                        (FORALL (?B)
                         (=> (PART ?A ?B) (SIMPLE-NODE ?B))))))
      (EXISTS (?C) (AND (METHOD-OF ?SELF ?C) (ACT-STAGE ?C)))))
(DEFINE-CLASS SYNCHRO-PLAN (?SELF)
:DEF
 (AND (GENERIC-PLAN ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF PLAN-DIRECT-PREDECESSOR 2)
      (EXISTS (?A)
              (AND (PLAN-PREDECESSOR ?SELF ?A)
                   (OR (CONCURRENT-PLAN ?A) (PARTLY-CONCURRENT-PLAN ?A)))))
 :CONSTRAINTS
 (AND (EXISTS (?B) (AND (REPRESENTED-BY ?SELF ?B) (JOIN-NODE ?B)))
      (EXISTS (?C) (AND (METHOD-OF ?SELF ?C) (PLANNING-STAGE ?C)))))
(DEFINE-CLASS THE-FIRST-PLAN (?SELF)
:IFF-DEF
 (AND (GENERIC-PLAN ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF PLAN-SUCCESSOR 1)
      (VALUE-TYPE ?SELF PLAN-PREDECESSOR INCOHERENT))
 :CONSTRAINTS (EXISTS (?A) (AND (REPRESENTED-BY ?SELF ?A) (THE-FIRST-NODE ?A))))
(DEFINE-CLASS THE-LAST-PLAN (?SELF)
:IFF-DEF
 (AND (GENERIC-PLAN ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF PLAN-PREDECESSOR 1)
      (VALUE-TYPE ?SELF PLAN-SUCCESSOR INCOHERENT))
 :CONSTRAINTS (EXISTS (?A) (AND (REPRESENTED-BY ?SELF ?A) (THE-LAST-NODE ?A))))