;;; -*- Mode:Lisp; Package:ONTOLINGUA-USER; Syntax:COMMON-LISP; Base:10 -*- 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;;;   CONFIGURATION DESIGN ONTOLOGY 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

;;; Last modification: 19 August 1993 

(in-package "ONTOLINGUA-USER") 

(define-theory CONFIGURATION-DESIGN (frame-ontology kif-meta) 

  "Configuration-Design is an ontology for describing configuration design 
tasks: describing components, parameters, constraints, and configurations. 
Like parametric design tasks, a configuration design task is a search for 
values of parameters that satisfy a set of constraints.  In configuration design,  
artifacts are described by collections of components, related by subpart  
relationships.  Each component has associated parameters and 
constraints.  The specification of a particular design task, such 
as the VT task for designing an elevator, is the description of a system 
component like an elevator, a set of constraints on that component (e.g., 
customer requirements), and a library of background constraints (e.g., laws of 
physics) and available components.  A valid design is a complete description 
of the system component, with values for relevant parameters and choices for 
subcomponents, that satisifies all the constraints. 
   The definitions in this ontology embody this tight relationship 
between components, constraints, and parameters.  Constraints are 
defined as unary predicates that hold for components.  Parameters are 
unary functions on components; in this theory, parameters are called 
attributes.  Components are related to other components through binary 
subpart relations. 
    The configuration-design ontology is intended for design tasks 
involving parametric constraint satisfaction (with decomposition by 
components), and part selection.  In configuration design, the set of 
chosen components determines the set of relevant parameters and 
constraints.  There is no built-in notion of component connection, 
only hierarchical subpart relations. 
   The configuration design theory does not restrict the 
expressiveness or form of the constraints.  A constraint is any 
limitation on the values of parameters (i.e., attributes of components 
in this theory).  Some constraints appear as part of the definition of 
a class.  For example, a value-type restriction on an attribute of a 
class of components is a constraint.  Similarly, component classes may 
have constant values for some attributes as part of their definitions. 
Such constraints are inherited to subclasses.  We assume that systems 
will have special-purpose mechanisms for dealing with definitional 
constraints such as downward-inherited values and value-type 
restrictions.  Other constraints, such as arithmetic relationships 
among numeric parameters, are reified as explicit linguistic objects 
(constraint expresssions).  We distinguish and reify these constraints 
because they determine the kind of reasoning to use (e.g., constraint 
satisfaction algorithm).  We anticipate that system will analyze the 
form of these reified constraints to decide how to process them, and 
to associate other knowledge with these constraints qua objects (e.g., 
when they are useful to apply).") 

(in-theory 'configuration-design) 

(define-class CONFIGURATION-THING (?x) 
  "Top level class for configuration ontology.  Used to identify 
mutually disjoint root classes that might be assimilated into  
other ontologies." 

 :def (individual ?x) 

 :axiom-def (subclass-partition 
              CONFIGURATION-THING 
              (setof constraint component attribute-slot))) 

(define-class COMPONENT (?x) 
  "A component is a primitive module or assembly of primitive modules 
that participate in a design.  Components need not correspond to 
physically whole objects such as standard parts from a parts catalog. 
Components may also represent functional and behavioral abstractions. 
This ontology only says that components are the locus of attributes 
and constraints.  To say that a component C has-attribute A means 
that there is a function A from C to the value of the attribute. 
In object-oriented terminology, one can think of A as a slot of C,  
and calling it an attribute means that it may be mentioned 
in constraints on C.  Similarly, a component C has-subpart S means  
the function S maps C to another component which plays the S role 
in C.  Subpart slots may identify structural, functional, or similar 
kinds of relationships among components." 

  :def (and (value-type ?x HAS-ATTRIBUTE attribute-slot) 
            (value-type ?x HAS-SUBPART subpart-slot) 
            (value-type ?x HAS-CONSTRAINT constraint) 
            (value-type ?x SATISFIES-CONSTRAINT constraint))) 

	     
(define-class COMPONENT-CLASS (?c) 
  "The meta class of component classes." 
  :iff-def (subclass-of ?c component)) 


(define-relation HAS-ATTRIBUTE (?component ?attribute-slot) 
  "A component has an attribute if the attribute value is given by a 
unary function, called an attribute-slot, that is defined for 
that component.  Calling a slot an attribute means that it is 
a design parameter: it will need to be assigned a value and 
may be mentioned in constraints." 

  :def (and (component ?component) 
            (attribute-slot ?attribute-slot) 
            (value-cardinality ?component ?attribute-slot 1)) 

  :issues ("The attribute is not reified as an object with a 
            slot for its value.  Instead, it's just a named 
            slot.  Since the slot is a function, and function 
            constants can be used as terms in KIF, then one can  
            still describe properties of an attribute as such." 
	   ("The value-cardinality spec says that each 
             attribute MUST have one, and only one, value 
             for the component.  What does this mean for 
             attributes that are not constants, i.e., those 
             that are computed from other values via constraints?" 
	    "If someone asserts that component C has-attribute A, 
             then this spec says that there exists a value for 
             the function A applied to C.  It does NOT say that 
             any particular agent KNOWS what that value is." 
	    :see-also VALID-DESIGN))) 

(define-relation HAS-SUBPART (?component ?subpart-slot) 
  "A component has an subpart if the subpart is given by a 
unary function, called a subpart-slot, that is defined for 
that component." 
  :def (and (component ?component) 
            (subpart-slot ?subpart-slot) 
            (value-cardinality ?component ?subpart-slot 1))) 


(define-relation HAS-CONSTRAINT (?component ?constraint) 
  "To say a component has a constraint means that the constraint 
has been associated with the component.  The constraint holds 
for the component iff it is a SATISFIED-CONSTRAINT of the component." 
  :def (and (component ?component) 
            (constraint ?constraint))) 


(define-class ATTRIBUTE-SLOT (?unary-function) 
  "An attribute slot is a unary function from COMPONENTs 
to ATTRIBUTE-VALUEs, which are either scalar quantities 
or strings." 
  :def (and (unary-function ?unary-function) 
            (domain ?unary-function component) 
            (range ?unary-function attribute-value))) 

(define-class ATTRIBUTE-VALUE (?x) 
  :def (or (real-number ?x)     ; real numbers 
           (string ?x)))   ; used as symbolic values, e.g., model names 

(define-class SUBPART-SLOT (?unary-function) 
  "A supart slot is a unary function from COMPONENTs 
to other components.  It is antisymmetric and antireflexive." 

  :def (and (unary-function ?unary-function) 
            (domain ?unary-function component) 
            (range ?unary-function component) 
            (antisymmetric-relation ?unary-function) 
            (antireflexive-relation ?unary-function)) 
  :issues (("Should subpart-slot be a partial order?"))) 

(define-relation QUANTITY-SLOT (?attribute-slot) 
  "Relation to limit the values of an attribute-slot to 
quantities of a given physical-dimension." 

  :def (and (attribute-slot ?attribute-slot) 
            (range ?attribute-slot real-number))) 

(define-class CONSTRAINT (?c) 

  "A constraint is a description that limits the permissible 
values for attributes of components in a design.  Every constraint 
is specified with a KIF expression of type constraint-expression. 
This expression describes a constraint over components; 
attributes and subparts of the component are denoted by 
functional terms within the constraint expression." 

  :def (and  
          ;; All constraints have an associated expresssion, 
          ;; a KIF sentence with one free variable, which 
          ;; constrains the possible bindings for one free variable, 
          ;; which denotes a component 

         (value-cardinality ?c CONSTRAINT.EXPRESSION 1) 
         (value-type ?c CONSTRAINT.EXPRESSION constraint-expression) 
         ) 

  :issues ((:example (constraint C1) 
                     (= (constraint.expression C1)  
			'(< (inside-height ?x) 
                            (outside-height (enclosed-box ?x))))) 
           (:example (constraint C2) 
                     (= (constraint.expression C2)  
			'(=> (> (capacity ?elevator) 5000) 
                             (= (model-name ?elevator) "model 43b")))))) 

(define-function CONSTRAINT.EXPRESSION (?constraint) :-> ?expression 
  "slot on constraint objects whose value is a KIF sentence (the 
syntactic thing, a list expression)." 

  :def (and (constraint ?constraint) 
            (constraint-expression ?expression))) 

;;; THE SYNTACTIC MACHINERY TO DEFINE CONSTRAINT-EXPRESSION IS AT THE END OF THIS FILE 

(define-function THE-CONSTRAINT (?expression) :-> ?constraint 
  "A constructor for constraint objects.  Given a constraint 
expression, it denotes the associated constraint object. 
This means that constraints are uniquely defined by their 
expressions." 

  :iff-def (and (constraint-expression ?expression) 
                (= (constraint.expression ?constraint) ?expression))) 


(define-relation SATISFIES-CONSTRAINT (?component ?constraint) 
  "A constraint specifies a class of components (i.e., those that  
satisfy the constraint expression).  The constraint expression 
has one free variable, which denotes the component being constrained. 
The relation satisfies-constraint says how the expression is associated  
with the component.  The class of components satisfying a constraint 
is denoted by a KAPPA expression that quantifies over the free 
variable in the constraint expression." 

  :iff-def  
  (and (component ?component) 
       (constraint ?constraint) 
       (holds (denotation 
                (listof 'kappa 
                        (listof (free-variable-in 
                                  (constraint.expression ?constraint))) 
                        (constraint.expression ?constraint))) 
              ?component)) 

  :issues ("Note that a component doesn't have to HAS-CONSTRAINT the  
            constraint in order for it to be satisfied.")) 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;;;   DESIGNS are components 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

(define-class VALID-COMPONENT (?component) 
  "A component is 'configured' or fully specified if all of its 
constraints are satisfied and all of its subparts are also configured. 
By definition, there exist values for all the attributes of a component. 
Whether an agent can tell you what the values of attributes are 
is not part of the definition of configured component. 
Knowing all the constraints associated with a component will 
require making a closed world assumption on the has-constraint slot." 

  :iff-def (and (component ?component) 
		(=> (has-constraint ?component ?constraint) 
                    (satisfies-constraint ?component ?constraint)) 
		(=> (has-subpart ?component ?part-slot) 
		    (valid-component (value ?part-slot ?component))))) 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;;;   SYNTACTIC RESTRICTIONS ON CONSTRAINT EXPRESSIONS 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 


(define-class CONSTRAINT-EXPRESSION (?sent) 
  "A contraint expression is a KIF sentence with a single free variable 
denoting a component.  All the terms in the sentence denote either 
attribute values or components (i.e., the component denoted by the 
free variable or one of its subparts).  No existential or universal 
quantification may be introduced.  The full set of logical operators 
are allowed. A restricted set of relations are allowed, and the 
restriction is also left to be defined in specializations of this 
ontology." 

  :def (and (= 1 (cardinality (freevars-in-expression ?sent))) 
            (restricted-constraint-sentence 
              ?sent 
              logical-operator 
              relation-constant 
              function-constant))) 


(define-relation RESTRICTED-CONSTRAINT-SENTENCE 
                 (?sentence 
                   ?class-of-logical-operators 
                   ?class-of-relation-constants 
                   ?class-of-attribute-term-operators) 
 "restricted-constraint-sentence is a predicate used to specify 
a class of sentences that are restricted by the set of operators 
and terminals in the grammar.  The first argument is a KIF sentence. 
The second is a class of logical operators (a class whose instances 
are the allowed operators).  The third argument is a class of 
relation operators, such as '<.  And the fourth argument is a 
class of operators that can be used to form terms.  These ``operators'' 
are actually symbols (relation constants), not the relations denoted by 
be these symbols.  In KIF, symbols can be denoted by quoting them." 

 :iff-def (and (sentence ?sentence) 
                (subclass-of ?class-of-logical-operators logical-operator) 
                (subclass-of ?class-of-relation-constants relation-constant) 
                (subclass-of ?class-of-attribute-term-operators function-constant) 
                (or 
                   ;; Relational Sentence 
                  (exists (?r @tlist) 
                     (and (= ?sentence (listof ?r @tlist)) 
                          (instance-of ?r ?class-of-relation-constants) 
                          (=> (item ?t (listof @tlist)) 
                              (restricted-constraint-term 
                                ?t 
                                ?class-of-attribute-term-operators)))) 
                   
                   ;; like true or false 
                  (logical-operator ?sentence) 
                   
                   ;; Conjuction, Disjunction, Implication, 
                   ;; Reverse-Implication, or Equivalence 
                  (exists (?op @sentences) 
                     (and (= ?sentence (listof ?op @sentences)) 
                          (instance-of ?op ?class-of-logical-operators) 
                          (=> (item ?s (listof @sentences)) 
                              (restricted-constraint-sentence 
                                ?s 
                                ?class-of-logical-operators 
                                ?class-of-relation-constants 
                                ?class-of-attribute-term-operators)))) 
                  ))) 

(define-relation RESTRICTED-CONSTRAINT-TERM (?term ?class-of-attribute-term-operators) 
  :iff-def (and (term ?term) 
                (subclass-of ?class-of-attribute-term-operators 
                             function-constant) 
                (or 
                  (restricted-attribute-term ?term 
                                             ?class-of-attribute-term-operators) 

                  (component-term ?term)))) 

(define-relation RESTRICTED-ATTRIBUTE-TERM (?term ?class-of-attribute-term-operators) 
  :iff-def (or 
              ;; a value expressed with numerals: 34.5 
              ;; or as a string: "model 45" 
             (attribute-value-constant ?term) 

              ;; an attribute reference: "(attribute component)" 
             (exists (?attr-slot ?comp) 
                (and (= ?term (listof ?attr-slot ?comp)) 
                     (attribute-slot-name ?attr-slot) 
                     (component-term ?comp))) 

              ;; an operator over attribute values: (+ (attr c1) v2) 
             (exists (?oper @args) 
                (and (= ?term (listof ?oper @args)) 
                     (instance-of ?oper ?class-of-attribute-term-operators) 
                     (=> (item ?arg (listof @args)) 
                         (restricted-attribute-term ?arg ?class-of-attribute-term-operators)))))) 


(define-class RELATION-CONSTANT (?r) 
  "A relation constant is a symbol that denotes a KIF relation." 
  :iff-def (relconst ?r)) 

(define-class OBJECT-CONSTANT (?C) 
  "An object constant is a symbol, a number specifier, or a string 
that denotes some object in the universe of discourse." 
  :iff-def (objconst ?c)) 

(define-class FUNCTION-CONSTANT (?f) 
  "A function constant is a symbol that denotes a KIF function." 
  :iff-def (funconst ?f)) 

(define-class LOGICAL-OPERATOR (?op) 
  :iff-def (member ?op (setof 'not 'and 'or '=> '<= '<=>))) 

(define-class TRUTH-VALUE-CONSTANT (?x) 
  "A truth-value constant is a symbol that denotes a logical 
value of true or false.  It is not a predicate!" 
  :iff-def (member ?x (setof 'true 'false))) 


(define-class CONFIG-RELATION-CONSTANT (?r) 
  "The relations allowed for a constraint expression will vary 
by specializations of this ontology.  At the minimum, the relations 
should hold over attribute values or components." 
  :def (relconst ?r)) 


(define-class CONSTRAINT-TERM (?term) 
  "A constraint term is an expression denoting either a component 
or the value of an attribute of a component." 
  :def (and (term ?term) 
	    (or (component-term ?term) 
                (attribute-term ?term)))) 

(define-class ATTRIBUTE-TERM (?x) 
  "An attribute term is an expression that denotes the value  
of an attribute of a component.  It is either a constant value 
or an term comprising a unary function (the attribute slot) 
and a component term." 
  :def (or (attribute-value-constant ?x) 

            ;; an attribute reference 
	   (exists (?attr-slot ?comp) 
              (and (= ?x (listof ?attr-slot ?comp)) 
                   (attribute-slot-name ?attr-slot) 
                   (component-term ?comp))) 

            ;; an arithmetic operator over attribute values 
           (exists (?oper @args) 
              (and (= ?x (listof ?oper @args)) 
                   (attribute-term-operator ?oper) 
                   (=> (item ?arg (listof @args)) 
                       (attribute-term ?arg)))) 
           )) 

(define-class ATTRIBUTE-TERM-OPERATOR (?f) 
  :def (funconst ?f)) 

(define-class ATTRIBUTE-VALUE-CONSTANT (?const) 
  "left underdefined, so specializations can restrict values to taste." 
  :def (ground-term ?const)) 


(define-class ATTRIBUTE-SLOT-NAME (?const) 
  "the constant naming some attribute slot." 
  :iff-def (and (funconst ?const) 
                (attribute-slot (denotation ?const)))) 

(define-class SUBPART-SLOT-NAME (?const) 
  "the constant naming some subpart slot." 
  :def (funconst ?const)) 


(define-class COMPONENT-TERM (?x) 
  :def (or (component-constant ?x) 
            ;; the variable denoting the component 
           (indvar ?x) 
            ;; a subpart reference 
	   (and (list ?x) 
		(exists (?f ?comp) 
		   (and (= ?x (listof ?f ?comp)) 
                        (subpart-slot-name ?f) 
                        (component-term ?comp)))))) 

(define-class COMPONENT-CONSTANT (?x) 
  "A component constant is a KIF object constant that 
denotes a component." 
  :def (and (objconst ?x) 
	    (component (denotation ?x)))) 

;; generic KIF expression machinery 

(define-class GROUND-TERM (?expression) 
  :iff-def (and (term ?expression) 
                (empty (freevars-in-expression ?expression)))) 


(define-function FREEVARS-IN-EXPRESSION (?exp) :-> ?vset 
  "A nonquantified expression may contain free variables, which are 
universally quantified.  This function returns the set of such 
variables contained in a term expression." 
  :lambda-body (cond ((indvar ?exp) 
                      (setof ?exp)) ((list ?exp) (union 
                      (freevars-in-expression (first ?exp)) 
                      (freevars-in-expression (rest ?exp)))) 
                     (true 
                      (setof)))) 

(define-function FREE-VARIABLE-IN (?exp) :-> ?variable 
  "For expressions with exactly one free variable, this function 
denotes that variable.  It is otherwise undefined." 
  :lambda-body (if (= 1 (cardinality (freevars-in-expression ?exp))) 
                   (the ?variable 
                        (member ?variable (freevars-in-expression ?exp))))) 

This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber