;;; -*- Mode:Lisp; Package:ONTOLINGUA-USER; Syntax:COMMON-LISP; Base:10 -*-;;; Constraint Ontology;;; (c) 1994 Thomas R. Gruber and Gregory R. Olsen;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CONSTRAINT ONTOLOGY;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;(in-package "ONTOLINGUA-USER") (define-theoryPARAMETRIC-CONSTRAINTS(frame-ontology kif-meta) "This theory provides the representational primitives for writing parametric models with constraint expressions. It makes two basic commitments: (1) Parameters are represented by normal object constants, and the value of a parameter is its denotation. (2) Constraints are reified objects, with quoted expressions that are KIF sentences; constraint satisfaction is defined in terms of the truth value of the sentences. This theory allows one to define embedded constraint languages with the same syntax as KIF sentences but with restrictions on the parameters, functions, and relations supported in the language. This is critical for guaranteeing completeness or tractability of constraint satisfaction. The basic entities in this theory are PARAMETER-NAME (a symbol), CONSTRAINT (an object), and CONSTRAINT-EXPRESSION (a sentence). Parameter names are just KIF object constants. Constraints are objects with an associated constraint-expression. A constraint-expression is a special case of a KIF sentence. At the minimum, a constraint-expression contains no quantifiers and has at most one free variable; further restrictions on the form of a constraint expression can be specified using RESTRICTED-CONSTRAINT-SENTENCE. The truth-value semantics of constraints is defined in the predicates SATISFIED-CONSTRAINT (for ground constraints) and SATISFIES-CONSTRAINT (for constraints with a free variable). Reifying parameters and constraints allows agents to talk about them as objects in the universe of discourse, and to make inferences based on meta-descriptions. For example, one would like to list the parameters and constraints in a theory, distinguishing them from other axioms and definitions. An agent could then analyze the constraints for completeness without making closed world assumptions or second-order quantification. Similarly, one could define sublanguages for which there are tractable algorithms, but retain the common, declarative semantics of KIF. This theory puts no limitations on what can be represented as parameters. There is no special vocabulary for limit the \"possible values\" of a parameter. Any restriction on the value of a parameter can be described with a constraint. The meaning of parameters is also independent of any object structure (i.e., parameters are not inherently properties of anything). Specializations of this theory may define classes of constraints of restricted form, and relate parameters to structured objects such as components. " :issues ("(c) 1994 Thomas R. Gruber and Gregory R. Olsen")) (in-theory 'PARAMETRIC-CONSTRAINTS) (define-classPARAMETER-NAME(?p) "In this theory, the relationship between a parameter and its value is the same as between an object constant and its denotation. In a constraint expression, one might see a symbol such as P1 occur as a term. According to the normal semantics of KIF, an object constant is a symbol that denotes an object in the universe of discourse. In engineering modeling, model parameters (sometimes called variables) \"have a value\" -- which is essentially the same idea as denotation. We wish to use the same semantics as KIF for constraint languages used for engineering modeling. Therefore, we use KIF object constants as parameters and take their detonation to be their parameter value. However, since the notion of an object constant is more general than engineering parameter, we need some way to distinguish the latter. For this purpose we label some of the object constants (i.e., the symbols) as parameternames. This lets us describe a set of parameters as a set of names, rather than a set of values. Describing the set of values is not sufficient because two parameters with the same values would be indistinguishable. For example, one might see the symbol P1 in a KIF sentence. The symbol \"P1\" is an object constant. We might say that that P1 is equal to 10 with the KIF sentence \"(= P1 10)\". We can say that the object constant \"P1\" is a parameter-name in KIF as: (parameter-name 'P1). Then it follows that the parameter.value of 'P1 is also its denotation: namely, 10. Now let's define a second parameter P2 whose value is also 10. The two parameter names 'P1 and 'P2 are not the same parameter name, but they happen to have the same value. Thus we can state the constraint (= P1 P2) using an ordinary KIF sentence, while also allowing the distinction (not (= 'P1 'P2))." :def (and (object-constant ?p) (defined (parameter.value ?p))) ; it always has a value :issues ((:example (parameter-name 'foo) (not (parameter-name 10)) (not (parameter-name '(foo))) (= foo (+ 10 20)) (= (parameter.value 'foo) 30)))) (define-functionPARAMETER.VALUE(?parameter-name) :-> ?value "Parameter.value is the function from parameter names to parameter values. It is defined as a special case of KIF denotation: when given an object constant that is a parameter-name, the parameter.value is the denotation of the object constant. When given anything else, the function is indefined (i.e., returns BOTTOM). This theory does not put any restriction on the possible values of a parameter. Such restrictions can be done with constraints on a per-model basis." := (if (parameter-name ?parameter-name) (denotation ?parameter-name))) (define-classCONSTRAINT(?c) "A constraint is a description that limits the permissible values for parameters and other properties of objects in a design. In this theory, constraints are objects with a slot called constraint.expression, whose value is a KIF sentence of type constraint-expression. This expression describes a constraint over parameters mentioned in the constraint. The constraint expression may also zero or one free variable. If the expression has not variables, then the constaint is called a parametric-constraint -- it is only over global parameters. If the expression contains a free variable, the constraint is called an object-constraint -- the variable represents the object being constrained. The existence of a constraint does not imply that the constraint.expression is a true sentence. The semantics of the constraint expressions, including how \"binding\" to objects works, is provided by the predicates SATISFIED-CONSTRAINT and SATISFIES-CONSTRAINT. Satisfied-constraint is for parametric constraints; in this case, the constraint is satisfied iff the sentence is true. (Determining the truth of a constraint-expression may require finding the values of parameters mentioned in the sentence, but these parameters are not logical variables.) Object constraints are satisfied with respect to some object. The predicate SATISFIES-CONSTRAINT takes an object and a constraint-expression and holds when the expression, with the object substituted for the free variable, is a true sentence. One may specify constraints with quoted expressions. For example, for the constraint C1, we can say that its constraint expression is a sentence relating two parameters, P1 and P2 as follows: (= (constraint.expression C1) '(<P1 P2)) C1 is satisfied if the sentence '(<P1 P2) is true. If (= P1 10) and (= P2 20), then (<P1 P2) and therefore C1 is satisfied." :def (and (defined (constraint.expression ?c)) ; must have an expression (constraint-expression (constraint.expression ?c))) :axiom-def (exhaustive-subclass-partition CONSTRAINT (setof parametric-constraint object-constraint)) :issues ((:example (constraint C1) (= (constraint.expression C1) '(<X Y))) (:example (constraint C2) (= (constraint.expression C2) '(=> (> capacity 5000) (= model-name "model 43b")))) :see-also (SATISFIED-CONSTRAINT SATISFIES-CONSTRAINT))) (define-functionCONSTRAINT.EXPRESSION(?constraint) :-> ?expression "Constraint.expression is a slot on constraint objects whose value is a KIF sentence (the syntactic thing, a list expression). The form of the sentence is limited by constraint-expression." :def (and (constraint ?constraint) (constraint-expression ?expression)) :issues ((:see-also constraint-expression))) (define-functionTHE-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-classCONSTRAINT-EXPRESSION(?sent) "A contraint-expression is a KIF sentence with at most one free variable denoting an object to which the constraint applies. Other terms in the constraint-expression may be object constants representing parameters, constant values like numbers and strings, or other objects. The functions and relations that are allowed in a constraint-expression are limited by restricted-constraint-sentence. Restricted classes of constraints (subclasses of constraint-expression) can be described by other applications of the restricted-constraint-sentence predicate. At the minimum, all constraint expressions have restricted quantification: namely, no existential or universal quantification may be introduced except for the optional single free variable. That is, the KIF operators FORALL, EXISTS, SETOFALL, KAPPA, and LAMBDA are never allowed in constraint expressions. Other restrictions on the constraint language may be specified in specializations of the this class by giving different arguments to the predicate restricted-constraint-sentence." :def (restricted-constraint-sentence ?sent logical-operator relation-constant function-constant atomic-term) :issues ((:see-also satisfied-constraint satisfies-constraint))) (define-classPARAMETRIC-CONSTRAINT(?constraint) "A parametric-constraint is a constraint whose constraint.expression contains no variables. It's called parameteric because the the things being constrained are parameters, rather than properties of objects." :iff-def (and (constraint ?constraint) (ground-sentence (constraint.expression ?constraint))) :issues ((:see-also SATISFIED-CONSTRAINT))) (define-relationSATISFIED-CONSTRAINT(?constraint) "A constraint is a SATISFIED-CONSTRAINT if its constraint.expression is a true sentence. The sentence may contain no variables; that is, the constraint must be a parametric-constraint." :iff-def (and (parametric-constraint ?constraint) (truth (constraint.expression ?constraint))) :issues ("Whether a constraint is satisfied is not dependent on any inference procedure or proof method. It does not mean provable or derived. A parametric-constraint is satisfied iff it is true." "Satisfied-constraint is not the same as predicates that are used to establish the truth of a sentencerelativeto a theory or context.")) (define-classOBJECT-CONSTRAINT(?constraint) "An object-constraint is a constraint on the properties of an object. Such objects can represent arbitrary systems of objects and parameters; this theory puts no restriction on the nature of the object (e.g., it might be a component, or syntatic structure, or a list of parameters). The purpose for distinguishing object constraints from parametric constraints is to allow for a modular scope of a constraint. Formally, an object-constraint is a constraint whose constraint.expression is a sentence with one free variable. That variable is not universally quantified; instead, it stands for the object being constrained. The semantics of the constraint expressions is given by the predicate SATISFIES-CONSTRAINT, which associates the variable with some specific object." :iff-def (and (constraint ?constraint) (sentence-with-one-variable (constraint.expression ?constraint)))) (define-relationSATISFIES-CONSTRAINT(?object ?constraint) "An object-constraint is satisfied if its constraint.expression, when applied to an object, is a true sentence. The \"application\" of the expression is a syntactic construction that transforms the expression into a KIF predicate. The constraint is satisfied by an object iff the predicate holds for the object." :iff-def (and (object-constraint ?constraint) (holds (denotation (listof 'kappa (listof (the-free-variable-in (constraint.expression ?constraint))) (constraint.expression ?constraint))) ?object)) :issues ("(KAPPA (?x) (p ?x)) denotes the relation that holds for all ?x such that (P ?x) is true." "(DENOTATION<expression>) refers to the the semantic value of the expression. The semantic value of a KAPPA expression is a unary relation." "(HOLDS R a) means that the relation R holds on the object a. A relation holds iff the associated predicate is true on the arguments." (:example (object-constraint C1) (= (constraint.expression C1) '(= (F ?x) (* (M ?x) (A ?x)))) (= (F body) 20) (= (M body) 10) (= (A body) 2) (satisfies-constraint body C1)))) (define-relationRESTRICTED-CONSTRAINT-SENTENCE(?sentence ?class-of-logical-operators ?class-of-relation-constants ?class-of-term-operators ?class-of-object-constants) "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, which must contain no quantification (i.e., no use of FORALL, EXISTS, SETOFALL, LAMBDA, or KAPPA). The second argument is a class of logical operators (a class whose instances are a subset of {AND, OR, NOT, =>,<=,<=>}). The third argument is a class of relation constants, such as '<and '=. The fourth argument is a class of function constants, such as + and FIRST. The fifth argument is a class of object constants allowed, which is some subset of OBJECT-CONSTANT. Instances of object-constant include symbols, numbers, and strings, but not lists or variables. One can use this argument to exclude some kinds of values by their syntatic form (e.g., strings) or limit the set of symbols to some pre-enumerated set. One can use this predicate to specify sublanguages within KIF, such as constrain languages. One can denote classes of logical operators, relation constants, and function constants using the ONE-OF function and giving it quoted symbols as arguments. For example, the following specifies the class of sentences without negation or implication, whose only functions are the arithmetic operators, whose only relation is are equality, and whose object constants are symbols and numbers: (restricted-constraint-sentence ?sentence (one-of 'and 'or 'not) (one-of '=) (one-of '+ '- '* '/) (kappa (?x) (and (object-constant ?x) (not (string ?x)))))" :iff-def (and (sentence ?sentence) (not (quantsent ?sentence)) (subclass-of ?class-of-logical-operators logical-operator) (subclass-of ?class-of-relation-constants relation-constant) (subclass-of ?class-of-term-operators function-constant) (subclass-of ?class-of-object-constants atomic-term) (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-term-operators ?class-of-object-constants))));; like true or false(truth-value-constant ?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-term-operators ?class-of-object-constants)))) ))) (define-relationRESTRICTED-CONSTRAINT-TERM(?term ?class-of-term-operators ?class-of-object-constants) "This relation limits terms to atomic terms (variables or constants) or to terms constructed via sanctioned term operators. No quantification is allowed." :iff-def (and (term ?term) (subclass-of ?class-of-term-operators function-constant) (subclass-of ?class-of-object-constants atomic-term) (or;; a variable of constant reference(instance-of ?term ?class-of-object-constants);; a valid operator over other terms: (+ v1 v2)(exists (?oper @args) (and (= ?term (listof ?oper @args)) (instance-of ?oper ?class-of-term-operators) (=> (item ?arg (listof @args)) (restricted-constraint-term ?arg ?class-of-term-operators ?class-of-object-constants))))))) (define-classATOMIC-TERM(?x) "An atomic-term is a KIF term that represents either a parameter or a value. It cannot be a list expression; it must be a constant or variable." :iff-def (and (term ?x) (not (list ?x)))) (define-classRELATION-CONSTANT(?r) "A relation constant is a symbol that denotes a KIF relation." :iff-def (relconst ?r)) (define-classOBJECT-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-classFUNCTION-CONSTANT(?f) "A function constant is a symbol that denotes a KIF function." :iff-def (funconst ?f)) (define-classLOGICAL-OPERATOR(?op) :iff-def (member ?op (setof 'not 'and 'or '=> '<='<=>))) (define-classTRUTH-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)));; generic KIF expression machinery(define-classGROUND-SENTENCE(?expression) "A ground sentence contains no variables." :iff-def (and (sentence ?expression) (empty (variables-in-sentence ?expression)))) (define-functionVARIABLES-IN-SENTENCE(?s) :-> ?vset "This function takes an unquantified KIF sentence (the syntactic thing, an expression) and returns the set of variables occuring freely in the sentence. This is only defined for unquantified sentences, and only handles individual variables (not sequence variables)." := (cond;; If it starts with and, or, not, =>, <=>, /=,;; then union the results of recursing on the enclosed sentences.((logsent ?s) (apply union (map VARIABLES-IN-SENTENCE (rest ?s))));; If it is a relational sentence, such as (P a ?x),;; then union the free variables found in each term expression.((relsent ?s) (apply union (variables-in-term (rest ?s))));; if it is a logical constants, like TRUE,;; then return the empty set((logconst ?s) (setof));; if it is a quantified sentence, like (forall ?x (p ?x)),;; then the function is undefined. This will make the function;; undefied if a quantified sentence occurs anywhere in the sentence.((quantsent ?s) bottom))) (define-functionVARIABLES-IN-TERM(?exp) :-> ?vset "This function returns the set of free variables (individual variables) that occur in an unquantified term expression. If there is a sequence variable or quantified term expression, then this function is undefined." := (cond;; if it is an individual constant, like ?X,;; then return the singleton set containing it.((indvar ?exp) (setof ?exp));; (<function> [<term>]+)((funterm ?exp) (apply union (map variables-in-term (rest ?exp))));; (IF <sent> <term> [<term>])((and (logterm ?exp) (= (first ?exp) 'IF)) (union (variables-in-sentence (second-item ?exp)) (apply union (map variables-in-term (rest (rest ?exp))))));; (COND [(<sent> <term>)]+)((and (logterm ?exp) (= (first ?exp) 'COND)) (apply union (map variables-in-cond-clause (rest ?exp))));; SETOFALL, THE, KAPPA, LAMBDA -> undefined((quanterm ?exp) bottom);; other legitimate term, such as SETOF, LISTOF, QUOTE, or a constant;; then return the empty set((term ?exp) (setof)))) (define-functionVARIABLES-IN-COND-CLAUSE(?cond-clause) :-> ?vset "COND clauses are of the form (sentence term)." := (if (and (list ?cond-clause) (sentence (first ?cond-clause)) (term (second-item ?cond-clause))) (union (variables-in-sentence (first ?cond-clause)) (variables-in-term (second-item ?cond-clause))))) (define-classSENTENCE-WITH-ONE-VARIABLE(?sentence) :iff-def (and (sentence ?sentence) (= 1 (cardinality (variables-in-sentence ?sentence))))) (define-functionTHE-FREE-VARIABLE-IN(?sentence) :-> ?variable "For sentences with exactly one free variable, this function denotes that variable. It is otherwise undefined." := (if (sentence-with-one-variable ?sentence) (the ?variable (member ?variable (variables-in-sentence ?sentence)))) :constraints (indvar ?variable))