Knowledge Interchange Format Specification

Chapter 3: Logic


Bottom

In KIF, all functions are total, i.e. there is a value for every combination of arguments. In order to allow a user to express the idea that a function is not meaningful for certain arguments, KIF assumes that there is a special "undefined" object in the universe and provides the object constant bottom to refer to this object.

Functional Terms

The value of a functional term without a terminating sequence variable is obtained by applying the function denoted by the function constant in the term to the objects denoted by the arguments.

For example, the value of the term (+ 2 3) is obtained by applying the addition function (the function denoted by +) to the numbers 2 and 3 (the objects denoted by the object constants 2 and 3) to obtain the value 5, which is the value of the object constant 5. If a functional term has a terminating sequence variable, the value is obtained by applying the function to the sequence of arguments formed from the values of the terms that precede the sequence variable and the values in the sequence denoted by the sequence variable.

Assume, for example, that the sequence variable @l has as value the sequence 2, 3, 4. Then, the value of the term (+ 1 @l) is obtained by applying the addition function to the numbers 1, 2, 3, and 4 to obtain the value 10, which is the value of the object constant 10.

Logical Terms

The value of a logical term involving the if operator is the value of the term following the first true sentence in the argument list. For example, the term (if (> 1 2) 1 (> 2 1) 2 0) is equivalent to 2.

If none of the embedded sentences of a logical term involving the if operator is true and there is an isolated term at the end, the value of the conditional term is the value of that isolated term. For example, if the object constant a denotes a number, then the term (if (> a 0) a (- a)) denotes the absolute value of that number.

If none of the embedded sentences is true and there is no isolated term at the end, the value is undefined (i.e. bottom). In other words, the term (if (p a) a) is equivalent to (if (p a) a bottom).

The value of a logical term involving the cond operator is the value of the term following the first true sentence in the argument list. For example, the term (cond ((> 1 2) 1) ((> 2 1) 2)) is equivalent to 2.

If none of the embedded sentences is true, the value is undefined (i.e. bottom). In other words, the term (cond ((p a) a)) is equivalent to (cond ((p a) a) (true bottom)).

True and False

The truth value of true is true, and the truth value of false is false.

Equations and Inequalities

An equation is true if and only if the terms in the equation refer to the same object in the universe of discourse.

An inequality is true if and only if the terms in the equation refer to distinct objects in the universe of discourse.

Relational Sentences

A simple relational sentence without a terminating sequence variable is true if and only if the relation denoted by the relation constant in the sentence is true of the objects denoted by the arguments. Equivalently, viewing a relation as a set of tuples, we say that the relational sentence is true if and only if the tuple of objects formed from the values of the arguments is a member of the set of tuples denoted by the relation constant.

If a relational sentence terminates in a sequence variable, the sentence is true if and only if the relation contains the tuple consisting of the values of the terms that precede the sequence variable together with the objects in the sequence denoted by the variable.

Logical Sentences

A negation is true if and only if the negated sentence is false.

A conjunction is true if and only if every conjunct is true.

A disjunction is true if and only if at least one of the disjuncts is true.

If every antecedent in an implication is true, then the implication as a whole is true if and only if the the consequent is true. If any of the antecedents is false, then the implication as a whole is true, regardless of the truth value of the consequent.

A reverse implication is just an implication with the consequent and antecedents reversed.

An equivalence is equivalent to the conjunction of an implication and a reverse implication.

Quantified Sentences

A simple existentially quantified sentence (one in which the first argument is a list of variables) is true if and only if the embedded sentence is true for some value of the variables mentioned in the first argument.

A simple universally quantified sentence (one in which the first argument is a list of variables) is true if and only if the embedded sentence is true for every value of the variables mentioned in the first argument.

Quantified sentences with complicated variables specifications can be converted into simple quantified sentences by replacing each complicated variable specification by the variable in the specification and adding an appropriate condition into the body of the sentence. Note that, in the case of a set restriction, it may be necessary to rename variables to avoid conflicts. The following pairs of sentences show the transformation from complex quantified sentences to simple quantified sentences.

    (forall (... (?x r) ...) s)
    (forall (...  ?x    ...) (=> (r ?x) s))

    (exists (... (?x r) ...) s)
    (exists (...  ?x    ...) (and (r ?x) s))
Note that the significance of free variables in quantifier-free sentences depends on context. Free variables in an assertion are assumed to be universally quantified. Free variables in a query are assumed to be existentially quantified. In other words, the meaning of free variables is determined by the way in which KIF is used. It cannot be unambiguously defined within KIF itself. To be certain of the usage in all contexts, use explicit quantifiers.

Definitions

The definitional operators in KIF allow us to state sentences that are true ``by definition'' in a way that distinguishes them from sentences that express contingent properties of the world. Definitions have no truth values in the usual sense; they are so because we say that they are so.

On the other hand, definitions have content -- sentences that allow us to derive other sentences as conclusions. In KIF, every definition has a corresponding set of sentences, called the content of the definition.

The defobject operator is used to define objects. The legal forms are shown below, together with their content. In the first case, the content is the equation involving the object constant in the definition with the defining term. In the second case, the content is the conjunction of the constituent sentences.

    (defobject s := t)
    (= s t)

    (defobject s p1 ... pn)
    (and p1 ... pn)

    (defobject s :-> v  :=> p)
    (=> (= s v) p)

    (defobject s :-> v  :<= p)
    (<= (= s v) p)
The deffunction operator is used to define functions. Again, the legal forms are shown below, together with their defining axioms. In the first case, the content is the equation involving (1) the term formed from the function constant in the definition and the variables in its argument list and (2) the defining term. In the second case, as with object definitions, the content is the conjunction of the constituent sentences.

    (deffunction f (v1 ...vn) := t)
    (= (f v1 ...vn) t)

    (deffunction f p1 ...pn)
    (and p1 ...pn)

    (deffunction f (v1 ... vn) :-> v :=> p)
    (=> (= (f v1 ... vn) v) p)

    (deffunction f (v1 ... vn) :-> v :<= p)
    (<= (= (f v1 ... vn) v) p)
The defrelation operator is used to define relations. The legal forms are shown below, together with their defining axioms. In the first case, the content is the equivalence relating (1) the relational sentence formed from the relation constant in the definition and the variables in its argument list and (2) the defining sentence. In the second case, as with object and function definitions, the content is the conjunction of the constituent sentences.

    (defrelation r (v1 ...vn) := p)
    (<=> (r v1 ...vn) p)

    (defrelation r p1 ...pn)
    (and p1 ...pn)

    (defrelation r (v1 ... vn) :=> p)
    (=> (r v1 ... vn) p))

    (defrelation r (v1 ... vn) :<= p)
    (<= (r v1 ... vn) p))

Michael R. Genesereth