KIF (Knowledge Interchange Format) is developed on Stanford University in California by Computer Science Department. It is part of of the Interlingua Working Group of the DARPA (Defence Advanced Research Projects Agency, the central research and development organization for the Department of Defense (DoD).)Knowledge Sharing Effort. First version was released in january '92, current release (version 3.0) in june '92. KIF is a computer-oriented language for the interchange of knowledge among disparate programs. It has declarative semantics (i.e. the meaning of expressions in the representation can be understood without appeal to an interpreter for manipulating those expressions); it is logically comprehensive (i.e. it provides for the expression of arbitrary sentences in the first-order predicate calculus); it provides for the representation of knowledge about the representation of knowledge; it provides for the representation of nonmonotonic reasoning rules; and it provides for the definition of objects, functions, and relations. KIF is a formal language for the interchange of knowledge among disparate computer programs (written by different programmers, at different times, in different languages, and so forth). KIF is not intended as a primary language for interaction with human users (though it can be used for this purpose). Different programs can interact with their users in whatever forms are most appropriate to their applications (for example frames, graphs, charts, tables, diagrams, natural language, and so forth). KIF is also not intended to be an internal representation for knowledge within computer programs or within closely related sets of programs (though it can be used for this purpose as well). Typically, when a program reads a knowledge base in KIF, it converts the data into its own internal form (specialized pointer structures, arrays, etc.). All computation is done using these internal forms. When the program needs to communicate with another program, it maps its internal data structures into KIF. The purpose of KIF is roughly analogous to that of Postscript. Postscript is commonly used by text and graphics formatting programs in communicating information about documents to printers. Although it is not as efficient as a specialized representation for documents and not as perspicuous as a specialized wysiwyg display, Postscript is a programmer-readable representation that facilitates the independent development of formatting programs and printers. While KIF is not as efficient as a specialized representation for knowledge nor as perspicuous as a specialized display (when printed in its list form), it too is a programmer-readable language and thereby facilitates the independent development of knowledge-manipulation programs. The definition of KIF is highly detailed. Some of these details are essential; others are arbitrary. Essential general features: The language has declarative semantics. It is possible to understand the meaning of expressions in the language without appeal to an interpreter for manipulating those expressions. In this way, KIF differs from other languages that are based on specific interpreters, such as Emycin and Prolog. The language is logically comprehensive It provides for the expression of arbitrary sentences in predicate calculus. In this way, it differs from relational database languages (many of which are confined to ground atomic sentences) and Prolog-like languages (that are confined to Horn clauses). \item{3.} The language provides for the representation of knowledge about the representation of knowledge. This allows us to make all knowledge representation decisions explicit and permits us to introduce new knowledge representation constructs without changing the language. Additional criteria (not essenial, but KIF tryies to maximize them in a joint fashion) Translatability A central operational requirement for KIF is that it enable practical means of translating declarative knowledge bases to and from typical knowledge representation languages. Readability Although KIF is not intended primarily as a language for interaction with humans, human readability facilitates its use in describing representation language semantics, its use as a publication language for example knowledge bases, its use in assisting humans with knowledge base translation problems, etc. Useability as a representation language Although KIF is not intended for use within programs as a representation or communication language, it can be used for that purpose if so desired. Syntax KIF has two froms. Linear and structured. KIF originated in a Lisp application and inherits its syntax from Lisp. The relationship between linear KIF and structured KIF is most easily specified by appeal to the Common Lisp reader [Steele]. In particular, a string of ascii characters forms a legal expression in linear KIF if and only if (1) it is acceptable to the Common Lisp reader (as defined in Steele's book) and (2) the structure produced by the Common Lisp reader is a legal expression of structured KIF (as defined in the next section). In structured KIF, the notion of word is taken as primitive. An expression is either a word or a finite sequence of expressions. In our treatment here, we use enclosing parentheses to bound the items in a composite expression. A variable is a word in which the first character is ? or @. A variable that begins with ? is called an individual variable. A variable that begins with an @ is called a sequence variable. Individual variables are used in quantifying over individual objects. Sequence variables are used in quantifying over sequences of objects. Operators are used in forming complex expressions of various sorts. There are four types of operators in KIF -- term operators, sentence operators, rule operators, and definition operators. Term operators are used in forming complex terms. Sentence operators are used in forming complex sentences. Rule operators are using in forming rules. Definition operators are used in forming definitions. ::= listof | setof | quote | if | cond | setofall | kappa | lambda ::= = | /= | not | and | or | => | <= | <=> | forall | exists ::= =>> | <<= | consis ::= defobject | defunction | defrelation | := | :=> | :& A constant is any word that is neither a variable nor an operator. There are four categories of constants in KIF -- object constants, function constants, relation constants, and logical constants. Object constants are used to denote individual objects. Function constants denote functions on those objects. Relation constants denote relations. Logical constants express conditions about the world and are either true or false. Some constants are basic in that their type and meaning are fixed in the definition of KIF. All other constants are non-basic in that the language user gets to choose the type and the meaning. All numbers, characters, and strings are basic constants in KIF; the remaining basic constants are described in the remaining chapters of this document. KIF is unusual among logical languages in that there is no way of determining the category of a non-basic constant (i.e. whether it is an object, function, relation, or logical constant) from its inherent properties (i.e. its spelling). The user selects the category of every non-basic constant for himself. The user need not declare that choice explicitly. However, the category of a constant determines how it can be used in forming expressions, and its category can be determined from this use. Consequently, once a constant is used in a particular way, its category becomes fixed. There are four special types of expressions in the language -- terms, sentences, rules, and definitions. Terms are used to denote objects in the world being described; sentences are used to express facts about the world; rules are used to express legal steps of inference; and definitions are used to define constants; and forms are either sentences, rules, or definitions. The set of legal terms in KIF is listed below. There are ten types of terms -- individual variables, object constants, function constants, relation constants, functional terms, list terms, set terms, quotations, logical terms, and quantified terms. Individual variables, object constants, function constants, and relation constants were discussed earlier. ::= | | | | | | | | | ::= (listof * []) ::= (setof * []) ::= ( * []) ::= (quote ) ::= (if [])| (cond ( ) ... ( )) ::= (the )| (setofall )| (kappa (* []) *)| (lambda(* []s) ) A functional term consists of a function constant and an arbitrary number of argument terms, terminated by an optional sequence variable. Note that there is no syntactic restriction on the number of argument terms -- the same function constant can be applied to different numbers of arguments; arity restrictions in KIF are treated semantically. Example: (+ 2 3) (exp (?x)) ... A list term consists of the listof operator and a finite list of terms, terminated by an optional sequence variable. Example: (listof mary (listof tom dick harry) sally) A set term consists of the setof operator and a finite list of terms, terminated by an optional sequence variable. Example: (setof mary john) Quotations involve the quote operator and an arbitrary list expression. The embedded expression can be an arbitrary list structure; it need not be a legal expression in KIF. Logical terms involve the if and cond operators. The if form allows for the testing of a single condition only, whereas the cond form allows for the testing of a sequence of conditions. Example: (if (> 1 2) 1 0), (if (p a) a) is equivalent to (if (p a) a bottom), (cond ((> 1 2) 1) ((> 2 1) 2)) Quantified terms involve the operators the, setofall, kappa, and lambda. A designator consists of the the operator, a term, nd a sentence. A set-forming term consist of the setof operator, aterm, and a sentence. A relation-forming term consists of kappa, a list of variables, and a sentence. A function-forming term consists of lambda, a list of variables, and a term. Strictly speaking, we do not need kappa and lambda -- both can be defined in terms of setof; they are included in KIF for the sake of convenience. The following BNF defines the set of legal sentences in KIF. There are six types of sentences. We have already mentioned logical constants. ::= ||||| ::= (= ) ::= (/= ) ::= ( * [])|( * ) ::= (not )| (and *)| (or *)| (=> * )| (<= *)| (<=> ) ::= (forall )| (forall (*) )| (exists )| (exists (*) ) The following BNF defines the set of legal KIF rules. ::= (=>> * ) | (<<= *) ::= | (consis ) The following BNF defines the set of legal KIF definitions. ::= | ::= (defobject := ) | (deffunction (* []) := ) | (defrelation (* []) := ) :: | ::= (defobject [:conservative-axiom ]) | (deffunction [:conservative-axiom ]) | (defrelation [:conservative-axiom ])| (defrelation (* []) :=> [:conservative-axiom ]) ::= (defobject *) | (deffunction *) | (defrelation *) | (defrelation (* []) :=> [:axiom ]) Definitions are used to make category declarations and specify defining axioms for constants (e.g. „ A triangle is a polygon with 3 sides. “). KIF definitions can be complete in that they specify an expression that defines the concept completely, or they can be partial in that they constrain the concept without necessarily giving a complete equivalence. Partial definitions can be either conservative or unrestricted. Conservative definitions are restricted in that their addition to a knowledge base does not result in the logical entailment of any additional sentences not containing the constant being defined. A form in KIF is either a sentence, a rule, or a definition.
::= | | Conceptualization The formalization of knowledge in KIF, as in any declarative representation, requires a conceptualization} of the world in terms of objects, functions, and relations. Objects A universe of discourse is the set of all objects presumed or hypothesized to exist in the world. The notion of object used here is quite broad. Objects can be concrete (e.g. a specific carbon atom, Confucius, the Sun) or abstract (e.g. the number 2, the set of all integers, the concept of justice). Objects can be primitive or composite (e.g. a circuit that consists of many subcircuits). Objects can even be fictional (e.g. a unicorn, Sherlock Holmes). Different users of a declarative representation language, like KIF, are likely to have different universes of discourse. KIF is conceptually promiscuous in that it does not require every user to share the same universe of discourse. On the other hand, KIF is conceptually grounded in that every universe of discourse is required to include certain basic objects. The following basic objects must occur in every universe of discourse. Words. Yes, the words of KIF are themselves objects in the universe of discourse, along with the things they denote. All complex numbers. All finite lists of objects in the universe of discourse. All sets of objects in the universe of discourse. Bottom -- a distinguished object that occurs as the value of various functions when applied to arguments for which the functions make no sense. Functions and Relations A function is one kind of interrelationship among objects. For every finite sequence of objects (called the arguments), a function associates a unique object (called the value). More formally, a function is defined as a set of finite lists of objects, one for each combination of possible arguments. In each list, the initial elements are the arguments, and the final element is the value. For example, the 1+ function contains the list < 2,3>, indicating that integer successor of 2 is 3. A relation is another kind of interrelationship among objects in the universe of discourse. More formally, a relation is an arbitrary set of finite lists of objects (of possibly varying lengths). Each list is a selection of objects that jointly satisfy the relation. For example, the < relation on numbers contains the list <2,3>, indicating that 2 is less than 3. Note that both functions and relations are defined as sets of lists. In fact, every function is a relation. However, not every relation is a function. In a function, there cannot be two lists that disagree on only the last element. This would be tantamount to the function having two values for one combination of arguments. By contrast, in a relation, there can be any number of lists that agree on all but the last element. For example, the list <2,3> is a member of the 1+ function, and there is no other list of length 2 with 2 as its first argument, i.e. there is only one successor for 2. By contrast, the < relation contains the lists <2,3>, <2,4>, and so forth, indicating that 2 is less than 3, 4, and so forth. Many mathematicians require that functions and relations have fixed arity, i.e they require that all of the lists comprising a function or relation have the same length. The definitions here allow for functions and relations with variable arity, i.e. it is perfectly acceptable for a function or a relation to contain lists of different lengths. For example, the + function contains the lists <1,1,2> and < 1,1,1,3>, reflecting the fact that the sum of 1 and 1 is 2 and the fact that the sum of 1 and 1 and 1 is 3. Similarly, the relation < contains the lists <1,2> and < 1,2,3>, reflecting the fact that 1 is less than 2 and the fact that 1 is less than 2 and 2 is less than 3. This flexibility is not essential, but it is extremely convenient and poses no significant theoretical problems Semantics The basis for KIF semantics is a correlation between the terms and sentences of the language and a conceptualization of the world. Every term denotes an object in the universe of discourse associated with the conceptualization, and every sentence is either true or false. When we encode knowledge in KIF, we select constants on the basis of our understanding of their meanings. In some cases (e.g. the basic constants of the language), these meanings are fixed in the definition of the language. In other cases (i.e. the non-basic constants), the meanings can vary from one user to another. Given exact meanings for the constants of the language (whether they are the meanings in the definition of the language or our own concoctions), the semantics of KIF tells us the meaning of its complex expressions. We can unambiguously determine the referent of any term, and we can unambiguously determine the truth or falsity of any sentence. Unfortunately, few of us have complete knowledge about the world. In keeping with traditional logical semantics, this is equivalent to not knowing the exact referent for every constant in the language. In such situations, we write sentences that reflect all of the meanings consistent with whatever knowledge we have. In such situations, the semantics of the language cannot pick out exact meanings for all expressions in the language, but it does place constraints on the meanings of complex expressions. And, of course, the meanings we ascribe to non-basic constants may differ from those ascribed by others. However, we can convey our meanings to others by writing sentences to constrain those meanings in accordance with our usage. By writing more and more sentences, the set of possible referents for our constants is decreased. In the remainder of this section, we provide precise definitions for the ideas just introduced. We start off with a definition for the interpretation of constants, and we introduce the related notion of variable assignment. We then show how these concepts are used in defining the semantic value of terms and the truth value of sentences. Finally, we introduce several approaches to entailment, which eliminates the dependence of meaning on the interpretation of non-basic constants. Interpretation An interpretation is a function i that associates the constants of KIF with the elements of a conceptualization. In order to be an interpretation, a function must satisfy the following two properties. First, the function must map constants into concepts of the appropriate type. It must map object constants into objects in the universe of discourse. It must map function constants into functions on the universe of discourse. It must map relation constants into relations on the universe of discourse. Notice that we allow for functions and relations of variable, finite arity. The function must map logical constants into one of the boolean values true or false which may or may not be members of the universe of discourse. 1. If s is an object constant, then i(s) \in O. 2. If s is a function constant, then i(s):O* -> O. 3. If s is a relation constant, then i(s) \subseteq O* 4. If s is a logical constant, then i(s) \in {true,false}. Second, i must „ satisfy “ the conditions and axioms given in this chapter and the remaining chapters of this document. As a start, this includes the following conditions. Every interpretation must map every numerical constant s into the corresponding number n (assuming base 10). i(s)=n Every interpretation must map the object constant bottom into bottom. i(bottom)=bottom Every interpretation must map the logical constant true into true and the logical constant false into false. i(true)=true i(false)=false Note that, even with these restrictions, KIF is only a „ partially interpreted ” language. Although the interpretations of some constants (the basic constants) are constrained in the definition of the language, the meanings of other constants (the non-basic constants) are left open (i.e. left to the imaginations of the language users). Variable assignment A variable assignment is a function that (1) maps individual variables V into objects in a universe of discourse O and (2) maps sequence variables W into finite sequences of objects. V : V -> O v: W -> O* Interpretation and variable assignment is expanded for every term to gain semantic value. f.e. siv ((listof t1 ... tn)) = And also tiv function to interpret boolean values of conditional terms. It is true that, as we add more sentences to a knowledge base, the set of models generally decreases. The goal of knowledge encoding is to write enough sentences so that unwanted interpretations are eliminated. Unfortunately, this is not always possible. In the light of this fact, how are we to interpret the expressions in such situations? The answer is to generalize over interpretations as earlier we generalized over variable assignments. If ? is a set of sentences, we say that ? logically entails sentence F if and only every model of ? is also a model of F. With this notion, we can rephrase the goal of knowledge representation as follows. It is to encode enough sentences so that every conclusion we desire is logically entailed by our set of sentences. It is a sad fact that this is not always possible, but it is the ideal toward which we strive. Numbers A formal axiomatization of numbers were developed during writing this document, so it is possibly available, but I have no information about it. It should look like this: Functions If t1, t2, ... , tn denote numbers, then the term (* t1 t2 ... tn) denotes the product of those numbers. If t1, t2, ... , tn denote numbers, then the term (+ t1 t2 ... tn) denotes the sum of those numbers. Other examples: unary functions 1+, 1-, abs, acos, ash (aritmetic shift, binary, number and bit count), gcd, ... Relations (defrelation > (?x ?y) := (< ?y ?x)) (defrelation =< (?x ?y) := (or (= ?x ?y) (< ?x ?y))) (defrelation >= (?x ?y) := (or (> ?x ?y) (= ?x ?y))) (defrelation positive (?x) := (> ?x 0)) (defrelation negative (?x) := (< ?x 0)) (defrelation odd-integer (?x) := (integer (/ (+ ?x 1) 2)) (defrelation even-integer (?x) := (integer (/ ?x 2)) ... Lists Very similar to those which we know from CL. A list is a finite sequence of objects. The objects in a list need not be KIF expressions, though they may be. In other words, it is just as acceptable to talk about a list of two people as it is to talk about a list of two symbols. In KIF, we use the term (listof t1 ... tn) to denote the list of objects denoted by t1, ..., tn. For example, the following expression denotes the list of an object named mary, a list of objects named tom, dick, and harry, and an object named sally. (listof mary (listof tom dick harry) sally) The relation list is the type predicate for lists. An object is a list if and only if there is a corresponding expression involving the listof operator. (defrelation list (?x) := (exists (@l) (= ?x (listof @l))) The object constant nil denotes the empty list. null tests whether or not an object is the empty list. The relation constants single, double, and triple} allow us to assert the length of lists containing one, two, and three elements, respectively. (defobject nil := (listof)) (defrelation null (?l) := (= ?l (listof))) (defrelation single (?l) := (exists ?x (= ?l (listof ?x)))) (defrelation double (?l) := (exists (?x ?y) (= ?l (listof ?x ?y)))) (defrelation triple (?l) := (exists (?x ?y ?z) (= ?l (listof ?x ?y ?z)))) The functions first, rest, last, and butlast each take a single list as argument and select individual items or sublists from those lists. (deffunction first (?l) := (if (= (listof ?x @items) ?l) ?x) (deffunction rest (?l) := (cond ((null ?l) ?l) ((= ?l (listof ?x @items)) (listof @items)))) (deffunction last (?l) := (cond ((null ?l) bottom) ((null (rest ?l)) (first ?l)) (true (last (rest ?l))))) (deffunction butlast (?l) := (cond ((null ?l) bottom) ((null (rest ?l)) nil) (true (cons (first ?l) (butlast (rest ?l)))))) Sets The formalization of sets of simple objects is a simple matter; but, when we begin to talk about sets of sets, the job becomes difficult due to the threat of paradoxes (like Russell's hypothesized set of all sets that do not contain themselves). Fortunately, there is no shortage of mathematical theories for our use in KIF -- various higher order logics, in KIF, we have adopted a version of the von Neumann-Bernays-Gode lset theory. Basic concepts In KIF, a fundamental distinction is drawn between individuals and sets. A set is a collection of objects. An individual is any object that is not a set. A distinction is also drawn between objects that are bounded and those that are unbounded. There are bounded individuals and unbounded individuals. There are bounded sets and unbounded sets. The fundamental relationship among these various types of entities is that of membership. Sets can have members, but individuals cannot. Bounded objects can be members of sets, but unbounded objects cannot. (It is this condition that allows us to avoid the traditional paradoxes of set theory.) These sentences are true: (or (set ?x) (individual ?x)) (or (not (set ?x)) (not (individual ?x))) (or (bounded ?x) (unbounded ?x)) (or (not (bounded ?x)) (not (unbounded ?x))) The sentence (member t1 t2) is true if and only if the object denoted by t1 is contained in the set denoted by t2. An important property shared by all sets is the extensionality property. Two sets are identical if and only if they have the same members. (=> (and (set ?s1) (set ?s2)) (<=> (forall (?x) (<=> (member ?x ?s1) (member ?x ?s2))) (= ?s1 ?s2))) We close this section with two axioms that allow us to conclude that sets of various sorts do, in fact, exist. The first is the axiom of regularity every non-empty set has an element with which it has no members in common. This axiom is not absolutely essential for set theory. However, it makes many proofs a lot easier, and so it is commonly included among the axioms of set theory. The second axiom is the axiom of choice. It asserts that there is a set that associates every bounded set with a distinguished element of that set. In effect, it chooses an element from every bounded set. We also have some axioms to easier manipulation with bounded and unbounded objects. First of all, we have the finite set axiom. Any finite set of bounded sets is itself a bounded set. The subset axiom assures that the set of all of subsets of a bounded set is also a bounded set. The union axiom tells us that the generalized union of any bounded set of bounded sets is also a bounded set. Since every finite set is bounded, this allows us to conclude, as a special case, that the union of any finite number of bounded sets is a bounded set. The intersection axiom tells us that the intersection of a bounded set and any other set is a bounded set. So long as one of the sets defining the intersection is bounded, the resulting set is bounded. Finally, we have the axiom of infinity. There is a bounded set containing a set, a set that properly contains that set, a third set that properly contains the second set, and so forth. In short, there is at least one bounded set of infinite cardinality. Metaknowledge In formalizing knowledge about knowledge, we use a conceptualization in which expressions are treated as objects in the universe of discourse and in which there are functions and relations appropriate to these objects. In our conceptualization, we treat atoms as primitive objects (i.e. having no subparts). We conceptualize complex expressions (i.e. non-atoms) as lists of subexpressions (either atoms or other complex expressions). In particular, every complex expression is viewed as a list of its immediate subexpressions. For example, we conceptualize the sentence (not (p (+ a b c) d)) as a list consisting of the operator not and the sentence (p (+ a b c) d). This sentence is treated as a list consisting of the relation constant p and the terms (+ a b c) and d. The first of these terms is a list consisting of the function constant + and the object constants a, b, and c. In order to assert properties of expressions in the language, we need a way of referring to those expressions. One way is to use the quote operator in front of an expression. From the section on semantics, we know that a quotation denotes the expression embedded within the term. Therefore, to refer to the symbol john, we use the term 'john or, equivalently, (quote john). To refer to the expression (p a b), we use the term '(p a b) or, equivalently, (quote (p a b)). (believes john '(material moon cheese)) (=> (believes john ?p) (believes mary ?p)) (mary believes everything John does) The second way of referring to expressions is KIF is to use the listof function. For example, we can denote a complex expression like (p a b) by a term of the form (listof 'p 'a 'b), as well as '(p a b). The advantage of the listof representation over the quote representation is that it allows us to quantify over parts of expressions. For example, let us say that Lisa is more skeptical than Mary. She agrees with John, but only on the composition of things. The first sentence below asserts this fact without specifically mentioning moon or cheese. Thus, if we were to later discover that John thought the sun to be made of chili peppers, then Lisa would be constrained to believe this as well. (=> (believes john (listof 'material ?x ?y)) (believes lisa (listof 'material ?x ?y))) Nonmonocity Many knowlege representation and reasoning systems are capable of drawing conclusions based on the absence of knowedge from a database. This is nonmonotonic reasoning. The addition of new sentences to the database may be cause for the system to retract earlier conclusions. In some systems, the exact policy for deriving nonmonotonic conclusions is built into the system. In other systems, the policy can be modified by its user, though rarely within the system's knowledge representation language (e.g. by selecting which predicates to circumscribe). Since KIF is a knowledge representation language and not a system, it is necessary to provide means for its user to express his nomonotonic reasoning policy within the language itself. We use default rules for this purpose. For instance, the following default rule expresses that an object can be assumed to fly if this object is known to be a bird and it is consistent to assume that it flies. (<<= (flies ?x) (bird ?x) (consis (flies ?x))) Another examle (we cannot replace <<== with <=) (<<= (status-known ?x) (citizen ?x)) (<<= (status-known ?x) (not (citizen ?x))) allow us to infer (status-known Joe) only if one of the sentences (citizen Joe), (not (citizen Joe)) can be inferred. Replacing the rules by implications would make (status-known ?x) identically true. We can use CWA if we want to: (<<= (not (s @l)) (consis (not (s @l)))) for all relations. Extending a set of sentences by the closed world assumption for some relation constant s, expressed by a default rule as shown above, has the same effect as circumscribing s (with all object, function and relation constants varied). In particular, circumscribing abnormality can be expressed by the default rule (<<= (not (ab ?aspect ?x)) (consis (not (ab ?aspect ?x)))) Consider, for instance, the nonmonotonic database that contains, in addition to this standard default, two facts. (bird tweety) (<= (flies ?x) (bird ?x) (not (ab aspect1 ?x))) (Birds fly unless they are abnormal in aspect1). This database nonmonotonically entails the conclusion that everything is not abnormal, including tweety: (not (ab ?aspect ?x)) From this, we can conclude that tweety flies. Suppose, on the other hand, that our database includes also the fact that tweety is abnormal in aspect1: (ab aspect1 Tweety) In this case, we can no longer infer that tweety is not abnormal, and, therefore, we cannot conclude that tweety is a flier. Note, however, that we have not asserted that tweety cannot fly; we have only prevented the default rule from taking effect in this case. Ending Example Every cat is on mat. (defobject mats : = (setof mat1 mat2 mat3 mat4 mat5)) (defrelation mat (?m) := (member ?m mats) (defobject cats := (setof silvester tom kitty garfield)) (defrelation cat (?c) := (member ?c cats)) (defrelation on (?x ?y) := (exists ?xs ?ys ?zs (has-coords (?xs ?ys ?zs ?x)) (has-coords (?xs ?ys ?zs ?y)))) (=> (cat ?x) (exists ?y (and (mat ?y) (on ?x ?y)))) (forall (?x cat) (exists (?y mat) (on ?x ?y))) Prílohy: BNF http://cui.unige.ch/db-research/Enseignement/analyseinfo/AboutBNF.html What is BNF notation? BNF is an acronym for "Backus Naur Form". John Backus and Peter Naur introduced for the first time a formal notation to describe the syntax of a given language (This was for the description of the ALGOL 60 programming language, see [Naur 60]). To be precise, most of BNF was introduced by Backus in a report presented at an earlier UNESCO conference on ALGOL 58. Few read the report, but when Peter Naur read it he was surprised at some of the differences he found between his and Backus's interpretation of ALGOL 58. He decided that for the successor to ALGOL, all participants of the first design had come to recognize some weaknesses, should be given in a similar form so that all participants should be aware of what they were agreeing to. He made a few modificiations that are almost universally used and drew up on his own the BNF for ALGOL 60 at the meeting where it was designed. Depending on how you attribute presenting it to the world, it was either by Backus in 59 or Naur in 60. (For more details on this period of programming languages history, see the introduction to Backus's Turing award article in Communications of the ACM, Vol. 21, No. 8, august 1978. This note was suggested by William B. Clodius from Los Alamos Natl. Lab). Since then, almost every author of books on new programming languages used it to specify the syntax rules of the language. See [Jensen 74] and [Wirth 82] for examples. The following is taken from [Marcotty 86]: The meta-symbols of BNF are: ::= meaning "is defined as" | meaning "or" < > angle brackets used to surround category names. The angle brackets distinguish syntax rules names (also called non-terminal symbols) from terminal symbols which are written exactly as they are to be represented. A BNF rule defining a nonterminal has the form: nonterminal ::= sequence_of_alternatives consisting of strings of terminals or nonterminals separated by the meta-symbol | For example, the BNF production for a mini-language is: ::= program begin end ; This shows that a mini-language program consists of the keyword "program" followed by the declaration sequence, then the keyword "begin" and the statements sequence, finally the keyword "end" and a semicolon. (end of quotation) In fact, many authors have introduced some slight extensions of BNF for the ease of use: optional items are enclosed in meta symbols [ and ], example: ::= if then [ else ] end if ; repetitive items (zero or more times) are enclosed in meta symbols { and }, example: ::= { | } this rule is equivalent to the recursive rule: ::= | [ | ] terminals of only one character are surrounded by quotes (") to distinguish them from meta-symbols, example: ::= { ";" } in recent text books, terminal and non-terminal symbols are distingued by using bold faces for terminals and suppressing < and > around non-terminals. This improves greatly the readability. The example then becomes: if_statement ::= if boolean_expression then statement_sequence [ else statement_sequence ] end if ";" Now as a last example (maybe not the easiest to read !), here is the definition of BNF expressed in BNF: syntax ::= { rule } rule ::= identifier "::=" expression expression ::= term { "|" term } term ::= factor { factor } factor ::= identifier | quoted_symbol | "(" expression ")" | "[" expression "]" | "{" expression "}" identifier ::= letter { letter | digit } quoted_symbol ::= """ { any_character } """ BNF is not ony important to describe syntax rules in books, but it is very commonly used (with variants) by syntactic tools. See for example any book on LEX and YACC, the standard UNIX parser generators. If you have access to any Unix machine, you will probably find a chapter of the documentation on these tools. Some references: [Naur 60] NAUR, Peter (ed.), "Revised Report on the Algorithmic Language ALGOL 60.", Communications of the ACM, Vol. 3 No.5, pp. 299-314, May 1960. [Jensen 74] JENSEN, Kathleen, WIRTH, Niklaus, "PASCAL user manual and report", Lecture notes in computer science ; vol. 18., Berlin [etc.] : Springer, 1974., 1974. [Johnson 75] S.C. Johnson, "Yacc: Yet Another Compiler Compiler", Computer Science Technical Report #32, Bell Laboratories, Murray Hill, NJ, 1975. [Wirth 82] WIRTH, Niklaus., Programming in Modula-2, Berlin, Heidelberg: Springer, 1982. [Marcotty 86] M. Marcotty & H. Ledgard, The World of Programming Languages, Springer-Verlag, Berlin 1986., pages 41 and following. Th. Estier, CUI - University of Geneva Dictionary: Confined – napätý, ohranicený, uzavretý Provides for – poskytovat Comprehensive – celkový, hutný obsažný to maximize in a joint fashion maximalizovat v sklbenej podobe unambigouesly – jednoznacne entailment – dôsledok notion – predstava, dojem, názor, nápad