Structured KIF



next up previous
Next: Conceptualization Up: Syntax Previous: Linear KIF

Structured KIF

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.

<word> ::= a primitive syntactic object

<expression> ::= <word> | (<expression>*)

The set of all words is divided into the categories listed below. This categorization is disjoint and exhaustive. Every word is a member of one and only one category. (The categories defined here are used again in the grammatical rules of subsequent tables.)

<indvar> ::= a word beginning with the character ?

<seqvar> ::= a word beginning with the character @

<termop> ::= listof | setof | quote | if | cond | the | setofall | kappa | lambda

<sentop> ::= = | /= | not | and | or | => | <= | <=> | forall | exists

<ruleop> ::= =>> | <<= | consis

<defop> ::= defobject | defunction | defrelation | := | :=> | :&

<objconst> ::= a word denoting an object

<funconst> ::= a word denoting a function

<relconst> ::= a word denoting a relation

<logconst> ::= a word denoting a truth value

From these fundamental categories, we can build up more complex categories, viz. variables, operators, and constants.

<variable> ::= <indvar> | <seqvar>

<operator> ::= <termop> | <sentop> | <ruleop> | <defop>

<constant> ::= <objconst> | <funconst> | <relconst> | <logconst>

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.

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 defined 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.

<term> ::= <indvar> | <objconst> | <funconst> | <relconst>|
           <funterm> | <listterm> | <setterm> |
           <quoterm> | <logterm> | <quanterm>

<listterm> ::= (listof <term>* [<seqvar>])

<setterm> ::= (setof <term>* [<seqvar>])

<funterm> ::= (<funconst> <term>* [<seqvar>])

<quoterm> ::= (quote <expression>)

<logterm> ::= (if <sentence> <term> [<term>])|
              (cond (<sentence> <term>) ... (<sentence> <term>))

<quanterm> ::= (the <term> <sentence>)|
               (setofall <term> <sentence>)|
               (kappa (<indvar>* [<seqvar>]) <sentence>*)|
               (lambda (<indvar>* [<seqvar>]s) <term>)

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.

A list term consists of the listof operator and a finite list of terms, terminated by an optional sequence variable.

A set term consists of the setof operator and a finite list of terms, terminated by an optional sequence variable.

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. Remember that the Lisp reader converts strings of the form ' into (quote ).

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.

Quantified terms involve the operators the, setofall, kappa, and lambda. A designator consists of the the operator, a term, and a sentence. A set-forming term consist of the setof operator, a term, 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.

<sentence> ::= <logconst>|<equation>|<inequality>|
               <relsent>|<logsent>|<quantsent>

<equation> ::= (= <term> <term>)

<inequality> ::= (/= <term> <term>)

<relsent> ::= (<relconst> <term>* [<seqvar>])|
              (<funconst> <term>* <term>)

<logsent> ::= (not <sentence>)|
              (and <sentence>*)|
              (or <sentence>*)|
              (=> <sentence>* <sentence>)|
              (<= <sentence> <sentence>*)|
              (<=> <sentence> <sentence>)

<quantsent> ::= (forall <indvar> <sentence>)|
                (forall (<indvar>*) <sentence>)|
                (exists <indvar> <sentence>)|
                (exists (<indvar>*) <sentence>)

An equation consists of the = operator and two terms.

An inequality consist of the /= operator and two terms.

A relational sentence consists of a relation constant and an arbitrary number of argument terms, terminated by an optional sequence variable. As with functional terms, there is no syntactic restriction on the number of argument terms in a relation sentence - the same relation constant can be applied to any finite number of arguments.

The syntax of logical sentences depends on the logical operator involved. A sentence involving the not operator is called a negation. A sentence involving the and operator is called a conjunction, and the arguments are called conjuncts. A sentence involving the or operator is called a disjunction, and the arguments are called disjuncts. A sentence involving the => operator is called an implication; all of its arguments but the last are called antecedents; and the last argument is called the consequent. A sentence involving the <= operator is called a reverse implication; its first argument is called the consequent; and the remaining arguments are called the antecedents. A sentence involving the <=> operator is called an equivalence.

There are two types of quantified sentences - a universally quantified sentence is signalled by the use of the forall operator, and an existentially quantified sentence is signalled by the use of the exists operator.

The following BNF defines the set of legal KIF rules.

<rule> ::= (=>> <premise>* <sentence>) |
           (<<= <sentence> <premise>*)

<premise> ::= <sentence> | (consis <sentence>)

The last argument in a forward rule is called the consequent of the rule. Analogously, the first argument in a reverse rule is called the consequent. The premises that are sentences are its prerequisites, and the premises that have the form (consis ) are its justifications.

The following BNF defines the set of legal KIF definitions.

<definition> ::= <complete> | <partial>

<complete> ::= 
 (defobject <objconst> := <term>) |
 (deffunction <funconst> (<indvar>* [<seqvar>]) := <term>) |
 (defrelation <relconst> (<indvar>* [<seqvar>]) := <sentence>)

<partial> :: <conservative> | <unrestricted>

<conservative> ::= 
 (defobject <objconst> [:conservative-axiom <sentence>]) |
 (deffunction <funconst> [:conservative-axiom <sentence>]) |
 (defrelation <relconst> [:conservative-axiom <sentence>])|
 (defrelation <relconst> (<indvar>* [<seqvar>])
   :=><sentence> [:conservative-axiom <sentence>])

<unrestricted> ::=
 (defobject <objconst> <sentence>*) |
 (deffunction <funconst> <sentence>*) |
 (defrelation <relconst> <sentence>*) |
 (defrelation <relconst> (<indvar>* [<seqvar>])
   :=> <sentence> [:axiom <sentence>])

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.

Object constants are defined using the defobject operator by specifying (1) a term that is equivalent to the constant or (2) a sentence that provides a partial description of the object denoted by the constant. Function constants are defined using the deffunction operator by specifying (1) a term that is equivalent to the function applied to a given set of arguments or (2) a sentence that provides a partial description of the function denoted by the constant. Relation constants are defined using the defrelation operator by specifying (1) necessary and sufficient conditions for the relation to hold, (2) necessary conditions for the relation to hold, or (3) arbitrary sentences describing the relation.

A form in KIF is either a sentence, a rule, or a definition.

<form> ::= <sentence> | <definition> | <rule>

A knowledge base is a finite set of forms. It is important to keep in mind that a knowledge base is a set of sentences, not a sequence; the order of forms within the knowledge base is unimportant.



next up previous
Next: Conceptualization Up: Syntax Previous: Linear KIF



Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994