;;; -- Steve Polyak 9 April 1998 -- created outline.
;;; -- Steve Polyak 21 April 1998 -- major changes to the structure.
;;; -- Steve Polyak 30 November 1998 -- rewrite for CPF.
;;; -- Steve Polyak 9 June 1999 -- final changes for initial version.

(in-package "ONTOLINGUA-USER")

(define-theory CPO (frame-ontology slot-constraint-sugar cpo-expressions)
  "This is version 0.3 of the Common Process Ontology (CPO).  CPO is
  used to specify process domain knowledge or to specify an individual
  process or plan. 3-CPO: The three elements of the Common Process
  Ontology: Meta-Ontology, Constraint-Ontology, Object-Ontology.
  Meta-Ontology provides fundamental ontological elements used to
  describe the others and the assumptions behind the description. The
  subject of the Object-Ontology is activity processes along with core
  activity-relatable objects.  The Constraint-Ontology provides the
  restrictions on the space of possible behavior."
  :issues ((:copyright "Copyright (c) 1998 Steve Polyak")))

(in-theory 'CPO)

;;; **********************************************************************
;;; CPO META-ONTOLOGY
;;; **********************************************************************

;;; Ontologies will commonly have a top-level class such as the
;;; following. They are more for organization rather than meaning, but
;;; are useful for assimilating a small ontology into a more
;;; comprehensive ontology.  

;;;CPO-Entity

(define-class CPO-ENTITY (?entity)
  "A CPO-ENTITY is a fundamental thing in the domain being modelled.
   A CPO-ENTITY may participate in relationships with other entities."
  :def (individual-thing ?entity)
  :axiom-def (subclass-partition
              CPO-ENTITY
              (setof cpo-process
		     cpo-activity-relatable-object
		     cpo-domain-level
		     cpo-node
		     cpo-timepoint
		     cpo-constraint)))

(define-relation ENTITY.ISA (?class1 ?class2)
  "This relation between classes is provided to allow subclassing to
  be defined within a process specification. The subclass-of relation is
  defined in the frame ontology as: a class1 is a subclass of parent
  class2 if and only if every instance of class1 is also an instance of
  class2."
  :def (and (class ?class1)
	    (class ?class2)
	    (subclass-of ?class1 ?class2)))

;;;CPO-String

(define-class CPO-STRING (?string)
  "The most general class of CPO text objects."
  :def (string ?string))

;;; CPO-Set

(define-frame CPO-Set
  "The most general Set-Class in the Ontology. Based on the Formal
  Enterprise Ontology (v.1.1) EO-SET. Every instance of Set-Class is a
  subclass of CPO-Set. This is an abstract class provided mainly for 
  convenience, so it is easy to see what all the Set-Classes are. It is
  up to Ontology developers, users and maintainers to make sure each
  instance of Set-Class is declared to be a subclass of CPO-Set."

  :iff-def (and (Instance-Of Set-Class CPO-Set) 
		(SubClass-Of CPO-Entity CPO-Set))
  :axioms
  (<=> (CPO-Set ?x)
       (Exists (?sc)
	       (and (Instance-Of ?sc Set-Class)
		    (Instance-Of ?x ?sc)))))

(define-frame Set-Class
  "Set-Class is a meta-Class.  Its instances are special kinds of classes,
  all of whose instances are themselves sets (not Classes) such that
  every member of such a set is specified to be a member of a certain Class."
  :own-slots
   ((Subclass-Of Class))
  :axioms
  (<=>
   (Set-Class ?set-of-things)
   (Exists (?thing)
	   (and (Class ?thing)
		(forall (?things)
			(<=> (instance-of ?things ?set-of-things)
			     (and (set ?things)
				  (forall (?x)
					  (=> (member ?x ?things)
					      (instance-of ?x ?thing))))))))))
;;; CPO-Boolean

(define-class CPO-BOOLEAN (?flag)
  :iff-def (member ?flag 
                   (setof true false)))

;;; **********************************************************************
;;; CPO OBJECT-ONTOLOGY
;;; **********************************************************************

;;; Cpo-Process

(define-class CPO-PROCESS (?x)
  "A process is a specification of behaviour."
  :def (and (cpo-entity ?x)
            (action ?x)  ;;; defined in basic sit. calc.
	    (has-one ?x process.pattern)
            (has-one ?x process.start-timepoint)
            (has-one ?x process.finish-timepoint))
  :issues   (("extensions required for levels and phases.")))

(define-function PROCESS.PATTERN (?process) :-> ?pattern
  "The unifiable pattern which can be used to match node patterns."
  :def (and (cpo-process ?process)
            (cpo-string ?pattern)))

(define-function PROCESS.START-TIMEPOINT (?proc) :-> ?tp
  :def (and (cpo-process ?proc)
            (cpo-timepoint ?tp))
  :axioms
  (forall (?s)
          (=  ?tp (start (do ?proc ?s))))
  (forall ?proc ?t1)
  (<=> (= (process.start-timepoint ?proc) ?t1)
       (exists (?t2)
               (OccursT ?proc ?t1 ?t2))))

(define-function PROCESS.FINISH-TIMEPOINT (?proc) :-> ?tp
  :def (and (cpo-process ?proc)
            (cpo-timepoint ?tp))
  :axioms
  (forall (?s)
          (=  ?tp (end (do ?proc ?s) ?proc)))

  (forall ?proc ?t1)
  (<=> (= (process.end-timepoint ?proc) ?t1)
       (exists (?t2)
               (OccursT ?proc ?t2 ?t1))))

(define-relation PROCESS.ACTIVITY-SPEC (?process ?spec)
  "The specification of the activity. Note that there can be more than
   one specification attached to a process."
  :def (and (cpo-process ?process)
            (cpo-activity-specification ?spec)))

(define-function PROCESS.EXPANDS (?process) :-> ?node
  "The particular node that a process expands."
  :def (and (cpo-process ?process)
            (cpo-node ?node)))

;;; Cpo-Plan

(define-class CPO-PLAN (?x)
  "A process which is designed for some objectives is termed a plan."
  :def (and (cpo-process ?x)
	    (has-one ?x plan.objective-spec)))

(define-relation PLAN.OBJECTIVE-SPEC (?plan ?spec)
  "The specification of the plan objectives." 
  :def (and (cpo-plan ?plan)
            (cpo-objective-specification ?spec)))

;;; CPO-Node

(define-class CPO-NODE (?x)
  :def (and (cpo-entity ?x)))

;;; CPO-Activity

(define-class CPO-ACTIVITY (?x)
  :def (and (cpo-node ?x)
            (action ?x)
            (has-one ?x activity.pattern)
            (has-one ?x activity.begin-timepoint)
            (has-one ?x activity.end-timepoint))
  :issues   (("actions can be in phases or in levels")
	     ("activities create, require, destroy, modify, etc.")))

(define-function ACTIVITY.PATTERN (?act) :-> ?pattern
  :def (and (cpo-activity ?act)
            (cpo-string ?pattern)))

(define-function ACTIVITY.BEGIN-TIMEPOINT (?act) :-> ?tp
  :def (and (cpo-activity ?act)
            (cpo-timepoint ?tp))
  :axioms
  (forall (?s)
          (=  ?tp (start (do ?act ?s))))
  (forall ?act ?t1)
  (<=> (= (activity.begin-timepoint ?act) ?t1)
       (exists (?t2)
               (OccursT ?act ?t1 ?t2))))

(define-function ACTIVITY.END-TIMEPOINT (?act) :-> ?tp
  :def (and (cpo-activity ?act)
            (cpo-timepoint ?tp))
  :axioms
  (forall (?s)
          (=  ?tp (end (do ?act ?s) ?act)))

  (forall ?a ?t1)
  (<=> (= (activity.end-timepoint ?a) ?t1)
       (exists (?t2)
               (OccursT ?a ?t2 ?t1))))

(define-function ACTIVITY.EXPANSION (?node) :-> ?proc
  "Indicates the process which expands this node."
  :def (and (cpo-activity ?node)
            (cpo-process ?proc))
  :axioms
  ;;; the expanded process is temporally bounded by the node
  (forall ?node ?proc
	  (=> (= activity.expansion(?node) ?proc)
	      (and (= begin.timepoint(?node) process.start-timepoint(?proc))
		   (= end.timepoint(?node) process.finish-timepoint(?proc)))))
  ;;; expansion and expands imply each other 
  (forall ?node ?proc
	  (<=> (= activity.expansion(?node) ?proc)
	       (= process.expands(?proc) ?node)))
  ;;; there can be only one defined expansion
  (forall ?node ?proc1
	  (=> (= activity.expansion(?node) ?proc1)
	      (not (exists (?proc2) (= activity.expansion(?node) ?proc2))))))

(define-relation CPO-SUBACTION (?act1 ?act2)
  :def (and (cpo-activity ?act1)
            (cpo-activity ?act2)
	    (subaction@complex-actions ?act1 ?act2))
  :issues (("Need to resolve subaction with include node in an 
             activity spec.")))

(define-class CPO-ACTION (?x)
  :def (cpo-activity ?x))

(define-relation CPO-PRIMITIVE (?act1)
  :def (and (cpo-action ?act1)
	    (primitive@complex-actions ?act1))
  :issues (("This needs some work.")))

(define-class CPO-EVENT (?x)
  :def (and (cpo-activity ?x)
	    (forall ?agent 
		    (not (agent.performs-act ?agent ?x)))))

(define-class CPO-OTHER-NODE (?x)
  :def (cpo-node ?x))

(define-class CPO-DUMMY-NODE (?x)
  :def (cpo-other-node ?x))

(define-class CPO-START (?x)
  :def (and (cpo-dummy-node ?x)
	    (has-one ?x start.timepoint)))

(define-class CPO-FINISH (?x)
  :def (and (cpo-dummy-node ?x)
	    (has-one ?x finish.timepoint)))

(define-class CPO-BEGIN (?x)
  :def (and (cpo-dummy-node ?x)
	    (has-one ?x start.timepoint)))

(define-class CPO-END (?x)
  :def (and (cpo-dummy-node ?x)
	    (has-one ?x finish.timepoint)))

(define-function START.TIMEPOINT (?node) :-> ?tp
  "Returns start timepoint for instantaneous nodes."
  :def (and (cpo-dummy-node ?node)
            (cpo-timepoint ?tp))

(define-function FINISH.TIMEPOINT (?node) :-> ?tp
  "Returns finish timepoint for instantaneous nodes."
  :def (and (cpo-dummy-node ?node)
            (cpo-timepoint ?tp))

;;; Cpo-Timepoint

(define-class CPO-TIMEPOINT (?x)
  "A CPO-TIMEPOINT is an entity that represents a specific, instananeous
   point along a time line which is an infinite sequence of time points."
  :def (and (time ?x) (cpo-entity ?x))
  :issues (("This needs to be properly connected to Pinto
             and Reiter's work.")
	   ("Need to work out time interval note duration in complex act.")
	   ("How about a CPO-Metric-Token?")))

;;; Cpo-Activity-Relatable-Object

(define-class CPO-ACTIVITY-RELATABLE-OBJECT (?x)
  "An activity-relatable-object is an abstract class used to
   group the objects which have a direct relationship to activities."
  :def (and (cpo-entity ?x)))

(define-function OBJECT.NAME (?object) :-> ?name
  :def (and (cpo-activity-relatable-object ?object)
            (cpo-string ?name)))

;;; Cpo-Agent

(define-class CPO-AGENT (?agent) 
  "A cpo-agent is an entity that can perform behaviour, hold purpose(s), 
   and have capabilities."
  :def (cpo-activity-relatable-object ?agent))

(define-instance ENVIRONMENT (cpo-agent)
  "There is a predefined AGENT called the environment. It can only
  establish enforced constraints and cannot intend, desire, or synthesize
  constraints."
  :axioms
  (forall ?objective ?plan
	  (=> (and (cpo-objective ?objective) (cpo-plan ?plan))
	      (not (agent.has-preference environment ?objective ?plan)))))

(define-relation AGENT.HAS-CAPABILITY (?agent ?capability)
  "This is a general mechanism for linking to capabilities."
  :def (and (cpo-agent ?agent)
            (cpo-string ?capability)))

(define-relation AGENT.HAS-REQUIREMENT (?agent ?objective ?plan)
  "This is the mechanism for an agent to enforce a constraint"
  :def (and (cpo-agent ?agent)
            (cpo-objective-constraint ?objective)
            (cpo-plan ?plan)
            (= soft-hard-information(?objective) HARD)))

(define-relation AGENT.HAS-PREFERENCE (?agent ?objective ?plan)
  "This is the mechanism for an agent to desire a constraint"
  :def (and (cpo-agent ?agent)
            (cpo-preference ?pref)
            (cpo-plan ?plan)
            (= soft-hard-information(?objective) SOFT)))

(define-relation AGENT.HAS-REQUIREMENT (?agent ?objective)
  "This is the mechanism for an agent to enforce a constraint"
  :def (and (cpo-agent ?agent)
            (cpo-objective-constraint ?objective)
            (= soft-hard-information(?objective) HARD)))

(define-relation AGENT.HAS-PREFERENCE (?agent ?objective)
  "This is the mechanism for an agent to desire a constraint"
  :def (and (cpo-agent ?agent)
            (cpo-objective-constraint ?objective)
            (= soft-hard-information(?objective) SOFT)))

(define-relation AGENT.HAS-PLAN (?agent ?plan)
  :def (and (cpo-agent ?agent)
            (cpo-plan ?plan))
  :issues ("need to relate having a plan to agent req/pref?"))

(define-relation AGENT.PERFORMS-ACT (?agent ?action)
  :def (and (cpo-agent ?agent)
            (cpo-action ?action)))

(define-relation AGENT.PERFORMS-PROC (?agent ?proc)
  :def (and (cpo-agent ?agent)
            (cpo-process ?proc)))

;;; CPO-Domain-Level

(define-class CPO-DOMAIN-LEVEL (?x)
  "A domain level is a partition of process specifications in a domain." 
  :def (and (cpo-entity ?x)
	    (has-one ?x domain-level.label)
	    (has-one ?x domain-level.number)))

(define-function DOMAIN-LEVEL.LABEL (?level) :-> ?label
  "This is a user-readable description of the level."
  :def (and (cpo-domain-level ?level)
            (cpo-string ?label)))

(define-function DOMAIN-LEVEL.NUMBER (?level) :-> ?number
  "This is a property which may be used to order levels."
  :def (and (cpo-domain-level ?level)
            (integer ?number)))

(define-relation DOMAIN-LEVEL.CONTAINS (?level ?process)
  :def (and (cpo-domain-level ?level)
            (cpo-process ?process)))

;;; **********************************************************************
;;; CPO CONTRAINT-ONTOLOGY
;;; **********************************************************************

(define-class CPO-ACTIVITY-SPECIFICATION (?act-spec)
  "A Set-Class all of whose instances are sets whose members are all of
   Class CPO-CONSTRAINT."
  :iff-def
  (and (CPO-Set ?act-spec)
       (and (Set ?act-spec)
	    (forall (?x)
		    (=> (Member ?x ?act-spec)
			(Instance-Of ?x CPO-CONSTRAINT)))))
  :issues (("This is a special Set-Class")))

(define-class CPO-OBJECTIVE-SPECIFICATION (?obj-spec)
  "A Set-Class all of whose instances are sets whose members are all of
   Class CPO-OBJECTIVE-CONSTRAINT."
  :iff-def
  (and (CPO-Set ?obj-spec)
       (and (Set ?obj-spec)
	    (forall (?x)
		    (=> (Member ?x ?obj-spec)
			(Instance-Of ?x CPO-OBJECTIVE-CONSTRAINT)))))
  :issues (("This is a special Set-Class")))

;;; CPO-Constraint

(define-class CPO-CONSTRAINT (?x)
  "A constraint expresses an assertion that can be evaluated with
   respect to a given process as something that may hold and can be
   elaborated in some language. Note the added-by Rel provides knowledge
   of which agent synthesized the constraint."

  :def (and (cpo-entity ?x))
  :axiom-def (exhaustive-subclass-partition
              CONSTRAINT
              (setof cpo-issue-constraint
		     cpo-node-constraint
                     cpo-other-constraint)))

(define-function CONSTRAINT.ADDED-BY (?x) :-> ?agent
  :def (and (cpo-constraint ?x)
            (cpo-agent ?agent)))

(define-function CONSTRAINT.EXPRESSION (?x) :-> ?exp
  :def (and (cpo-constraint ?x)
            (relation ?exp)))

;;; CPO-Constraint-Type

(define-class CPO-CONSTRAINT-TYPE (?type)
  "This is just an abstract class with represents two possible const.
   types: soft and hard."
  :iff-def (member ?type 
                   (setof 'soft 'hard)))

(define-instance SOFT (cpo-constraint-type))
(define-instance HARD (cpo-constraint-type))

(define-function CONSTRAINT.SOFT-HARD-INFORMATION (?x) :-> ?type
  :def (and (cpo-constraint ?x)
            (cpo-constraint-type ?type)))

;;; CPO-Objective-Constraint

(define-class CPO-OBJECTIVE-CONSTRAINT (?x)
  "OBJECTIVE-CONSTRAINTS impose restrictions over a set of 
   world states or require particular activities to be performed."  
  :def (and (constraint ?x)
            (has-one ?x constraint.expression)
	    (Instance-Of constraint.expression(?x) cpo-objective-expression))

;;; CPO-Issue-Constraint

(define-class CPO-ISSUE-CONSTRAINT (?x)
  "An issue is an oustanding aim, preference, task, flaw or
   other issue which remains to be addressed by the process. Issues provide
   implied constaints on the real world behaviour specified by the
   process. Issues are represented by a verb, zero, one or more noun phrases
   and zero, one or more qualifiers."
  :def (and (constraint ?x)
            (has-one ?x constraint.expression)
	    (Instance-Of constraint.expression(?x) cpo-issue-expression))

;;; CPO-Node-Constraint

(define-class CPO-NODE-CONSTRAINT (?x)
  :def (cpo-constraint ?x)
  :axiom-def (exhaustive-subclass-partition
              CPO-NODE-CONSTRAINT
              (setof cpo-include-constraint
                     cpo-not-include-constraint)))

(define-class CPO-INCLUDE-CONSTRAINT (?x)
  :def (and (cpo-node-constraint ?x)
            (has-one ?x include-node))
  :axioms
  ;;; included activities are temporally contained within a process
  (forall ?act-spec ?proc ?node
	  (=> (and (cpo-activity-specification ?act-spec) 
		   (cpo-process ?proc)
		   (member ?x ?act-spec)
		   (activity-spec ?proc ?act-spec)		   
		   (= include-node(?x) ?node)
		   (cpo-activity ?node))
	      (and (< process.start-timepoint(?proc) begin.timepoint(?node))
		   (< end.timepoint(?node) process.finish-timepoint(?proc)))))

  ;;; included start/begin nodes are fixed at the process start time
  (forall ?act-spec ?proc ?node
	  (=> (and (cpo-activity-specification ?act-spec) 
		   (cpo-process ?proc)
		   (member ?x ?act-spec)
		   (activity-spec ?proc ?act-spec)		   
		   (= include-node(?x) ?node)
		   (or (cpo-start ?node) (cpo-begin ?node)))
	      (= process.start-timepoint(?proc) start.timepoint(?node))))

  ;;; included finish/end nodes are fixed at the process finish time
  (forall ?act-spec ?proc ?node
	  (=> (and (cpo-activity-specification ?act-spec) 
		   (cpo-process ?proc)
		   (member ?x ?act-spec)
		   (activity-spec ?proc ?act-spec)		   
		   (= include-node(?x) ?node)
		   (or (cpo-finish ?node) (cpo-end ?node)))
	      (= process.finish-timepoint(?proc) finish.timepoint(?node)))))
		    
(define-function INCLUDE-NODE (?x) :-> ?node
  :def (and (cpo-include-constraint ?x)
            (cpo-node ?node)))

(define-class CPO-NOT-INCLUDE-CONSTRAINT (?x)
  :def (and (cpo-node-constraint ?x)
	    (has-one ?x not-include-node))
  :axioms
  ;;; not-include prevents mirror include node constraints
  (forall ?act-spec ?node
	  (=> (and (cpo-activity-specification ?act-spec) 
		   (member ?x ?act-spec)
		   (= not-include-node(?x) ?node))
	      (not (exists ?y
			   (and (cpo-include-constraint ?y)
				(= include-node(?y) ?node)
				(member ?y ?act-spec)))))))

(define-function NOT-INCLUDE-NODE (?x) :-> ?node
  :def (and (cpo-not-include-constraint ?x)
            (cpo-node ?node)))

;;; CPO-Other-Constraint

(define-class CPO-OTHER-CONSTRAINT (?x)
  :def (and (constraint ?x)
	    (has-one ?x constraint.expression))
  :axiom-def (exhaustive-subclass-partition
              CPO-OTHER-CONSTRAINT
              (setof cpo-ordering-constraint
                     cpo-variable-constraint
                     cpo-auxiliary-constraint)))

;;; CPO-Ordering-Constraint

(define-class CPO-ORDERING-CONSTRAINT (?x)
  "It is possible to specify temporal relationships directly between 
   timepoints, and through the association of timepoints with the begin
   and end of an activity, between activities themseleves. (e.g.
   before(tp1,tp2), equal(tp1,tp2))" 
  :def (and (cpo-other-constraint ?x)
            (has-one ?x constraint.expression)
	    (Instance-Of constraint.expression(?x) cpo-ordering-expression)))

;;; Cpo-Variable-Constraint

(define-class CPO-VARIABLE-CONSTRAINT (?x)
  "A relationship such as codesignation between entity variables
   non-co-designation, possibly others such as type membership
   general restriction facilities, ranges, etc."
  :def (cpo-other-constraint ?x))

;;; Cpo-Auxiliary-Constraint

(define-class CPO-AUXILIARY-CONSTRAINT (?x)
  :def (cpo-other-constraint ?x)
  
  :axiom-def (exhaustive-subclass-partition
              CPO-AUXILIARY-CONSTRAINT
              (setof cpo-authority-constraint
                     cpo-world-state-constraint
                     cpo-resource-constraint
                     cpo-spatial-constraint
                     cpo-misc-constraint)))

(define-class CPO-AUTHORITY-CONSTRAINT (?x)
  :def (cpo-auxiliary-constraint ?x))

(define-class CPO-WORLD-STATE-CONSTRAINT (?x)
  :def (cpo-auxiliary-constraint ?x))

;;; CPO-Input-Constraint

(define-class CPO-INPUT-CONSTRAINT (?x)
  "It is a temporal constraint which may or may not be satisfied
   immediately before the given timepoint."
  :def (cpo-world-state-constraint ?x)

;;; CPO-Output-Constraint

(define-class CPO-OUTPUT-CONSTRAINT (?x)
  "It is a temporal constraint which may or may not be satisfied
   immediately after the given timepoint."
  :def (cpo-world-state-constraint ?x)

;;; CPO-Range-Constraint

(define-class CPO-RANGE-CONSTRAINT (?x)
  "It is a temporal constraint involving two timepoints,
   the constraint should hold at all times between the two points."
  :def (cpo-world-state-constraint ?x)

;;; CPO-Metric-Constraint

(define-class CPO-METRIC-CONSTRAINT (?x)
  "It is a temporal constraint involving one timepoint,
   to relate a given timepoint to an actual time or calendar ref."
  :def (cpo-ordering-constraint ?x))

(define-class CPO-ALWAYS-CONSTRAINT (?x)
  :def (cpo-world-state-constraint ?x)
  :issues (("Quantify over all states and show that this is always true")))

(define-class CPO-RESOURCE-CONSTRAINT (?x)
  :def (cpo-auxiliary-constraint ?x)
  :axiom-def (subclass-partition
              CPO-RESOURCE-CONSTRAINT
              (setof cpo-agent-constraint)))

(define-class CPO-AGENT-CONSTRAINT (?x)
  :def (cpo-resource-constraint ?x))

(define-class CPO-SPATIAL-CONSTRAINT (?x)
  :def (cpo-auxiliary-constraint ?x))

(define-class CPO-MISC-CONSTRAINT (?x)
  :def (cpo-auxiliary-constraint ?x)
  
  :axiom-def (exhaustive-subclass-partition
              CPO-MISC-CONSTRAINT
              (setof cpo-quality-constraint
                     cpo-annotation-constraint)))

(define-class CPO-QUALITY-CONSTRAINT (?x)
  :def (cpo-misc-constraint ?x))

(define-class CPO-ANNOTATION-CONSTRAINT (?x)
  :def (cpo-misc-constraint ?x))

;;; End File