A Decidable First-Order Logic for Knowledge Representation

A Decidable First-Order Logic for Knowledge Representation

Peter F . Patel-Sclmeider

Schlumberger Palo Alto Research 3340 Hillview Avenue Palo Alto, CA 94304

ABSTRACT

Even though logic has played an important role in knowl­ edge representation (KR) research, there has been little effort expended on devising decidable logics for KR. Most modifications to logic suggested for KR are either exten­ sions to first-order logic (e.g., to handle non-monotonidty) or ad hoc changes in its inference mechanism. This pa­ per presents a variant of first-order relevance logic that has a decidable algorithm for determining tautological en­ tailment. Although this logic is considerably weaker than standard first-order logic , it can be used effectively in a KR system when semantically correct answers to queries are required within a finite amount of time.

Knowledge representation has always played a major role in Artificial Intelligence research. However, the exact nature of that role has been left undefined. So-called knowledge representation (KR) systems can range from packages for manipulating data structures to complete AI systems that plan or do resource man­ agement . The view of KR used here (similar to that espoused in [Levesque, 1984a)) is that a KR system is to provide a fact man­ agement service. That is, the job of a KR system is to manage a knowledge base (KB) in some representation language (including both syntax and semantics) and to answer questions about what semantically follows from the current KB. 1 An important part of this view, when applied to KR, is that the KR system must not only be sound, it must also be complete. This means that every answer given by the system, including "answering" 'unknown' or even refusing to answer, must be sanctioned by the semantics. One important effect of this formulation is that the behavior of the KR system cannot depend on extra-linguistic considerations, such as length of derivations or elapsed time.

The main problem in this formulation of KR is to select or create ~ suitable representation language, with an appropriate semantics. There are several properties desirable in such a lan­ guage. First, the language should have expressive power suffi­ cient to represent many situations. Second, the semantics should correspond to our intuitive notions about the meanings of the constructs of the language. Third, there should be a decidable and, moreover, reasonably fast procedure for computing whether some statement follows from a KB.

Obviously a representation language in which it is impossible to formulate many problem definitions and questions is inade­ quate. However, frame-based KR systems, as popular as they are, suffer from just this inability. The kind of language typically used m such systems cannot adequately express most disjunctions or sinlllar weak statements, which are required in many contexts. This shortcoming has often been sidestepped by adding extra­ linguistic hooks to frame-based systems such as user-definable procedures that perform some part of the inference process. Such actions destroy the semantics of the representation language and therefore systems that resort to such subterfuges do not satisfy the view of KR espoused here.

'This is in accordance with the view expounded by McDermott [McDermott, 1978) and, more recently, by Frisch [Frisch, 1985). However, most current KR systeD18 do not satisfy this view.

It is generally accepted in KR that the expressive power of at least standard first-order logic (FOL) is needed in a repre­ sentation language. FOL itself is a good candidate because it has a semantics that corresponds well with our intuitive ideas about the world. Unfortunately, this logic has a severe problem­ determining whether one sentence follows from another is in general, undecidable. This makes a KR system built on FOL unsuitable for AI systems that depend on receiving answers.

This problem with FOL has led to many attempts to create KR systems based on FOL that always produce answers. Most of these systems retain the syntax of FOL while modifying its in­ ferences in some way. The crudest of them simply take a theorem prover for FOL and place some ad hoc restrictions on it such as terminating the search for a proof after a pre-set amoun~ of time or a certain number of proof steps. Such modifications produce systems that cannot be given an adequate semantics and have no means of completely characterizing answers except by refer­ ring to the actions of the modified theorem prover. This destroys most of the advantages of using logic in the first place.

A more principled approach is to devise a semantics for first­ order sentences that can model something like these limitations ?n inferences. For example, Konolige's system [Konolige, 1985] mcludes a set of inference rules in the model structure and Frisch and Allen [Frisch and Allen, 1982] encode a variant of first-order logic back into FOL, thus capturing a particular set of inferences. Such systems have been characterized in [Levesque, 1984b] as syntactic variants because their semantic structures have to in­ clude syntactic entities. Because their semantics is used to model the inference process, every choice of how this process proceeds shows up in the semantics. This makes for a very complicated semantics which only rell.ects the inference process and does not give any guidance as to what the correct inferences should be.

What is needed is a semantics that does not involve the infer­ ence process but is instead based on the usual model theoretic ideas of interpretations and truth and falsity, thus allowing the semantics to dictate the correct inferences as opposed to vice veua. This semantics must correspond with some part of our intuitions about the world while also having decidable inference. It should also be weaker than FOL so that all reasoning in it is sound with respect to FOL. The semantics might not be as intuitive as that of FOL but the idea is to develop a semantics that captures part of our intuitions and trade off whatever is lost for decidability and, hopefully, tractability of inference.

I Relevance Logic

One possible logic for this purpose is the logic of tautologi­ cal entailments- a simple type of propositional relevance logic [Anderson and Belnap, 1975] . Propositional tautological entail­ ment has been used by Levesque [Levesque, 1984b] to model ex­ plicit propositional belief. Relevance logic has also been used by Shapiro [Shapiro and Wand, 1976] ~ part of a semantic network KR system. In fact, one of the main proponents of relevance logic suggested that it would be a useful logic for KR [Belnap, 1977].

The syntax of the logic of propositional tautological entailment is the same as that of standard propositional logic (PL), but without an implication operator. Its semantics is based on the four-valued setups of propositional relevance logic (as opposed to the two-valued assignments of PL). In these setups propositional letters and, from them, sentences can be assigned true or false (as in PL) but can also be assigned neither true nor false or both true and false. In some ways these setups model the state of affairs that may be encountered by KR systems better than two-valued assignments do because such systems may have no information on whether some proposition is true or false and also may have been, inadvertently, told that some other proposition is both true and false [Belnap, 1977]. A key difference between this way of defining truth and falsity and that used in PL is that there are no sentences which are true in all setups nor are there any which are false in all setups. For example, p V -,p is neither true nor false in a setup that supports neither p's truth nor p's falsity.

From this basis, the idea of propositional tautological entail­ ment (a relevance logic analogue of implication) can be defined. Here a entails f3 (written a -+ {3) iff f3 is true whenever a is and a is false whenever f3 is. If a -+ f3 then f3 follows from a in PL, because the set of two-valued assignments is included in the set of setups. However, entailment is a much weaker notion than implication. For example, a 1\ -,a f+ b and a f+ b V -,b, showing that a contradiction does not entail everything nor does every sentence entail a tautology. Further, a 1\ (-,a V b) f+ b, showing that modus ponens is not a valid rule for entailment.

In fact, there is a simple algorithm for determining if one sen­ tence entails another. To determine if a -+ f3 first put a and f3 into conjunctive normal form {CNF). Then 01 1\ ... 1\ On -+ {31 1\ ... 1\ f3m (where each a; and {3; are disjunctions of primi­ tive propositions) iff for each {3; there is an a; such that a; ~ {3; (treating a; and {3; as sets). This algorithm is a bit disappointing at first glance because putting a and f3 into CNF can cause an ex­ ponential increase in their size and the main rationale for using tautological entailment was to have a faster algorithm. How­ ever, KBs are almost always a conjunction of many facts, each of which is much smaller than the KB as a whole. This means that KBs are naturally in almost CNF so normalizing them will not increase their size drastically. Then, if a and f3 are in CNF, com­ puting whether a -+ f3 takes time proportional to the product of their sizes [Levesque, 1984b]. On the other hand the problem of determining if a implies f3 is co-NP complete even if a and f3 are in CNF.

Therefore propositional tautological entailment would be a good choice for a KR system provided that propositional sen­ tences were expressively adequate for KR. This logic sanctions a subset of the inferences of PL that is easy to compute and corresponds to a semantics that is at least plausible for KR.

However, propositional logic is generally considered not ex­ pressive enough for a KR system. This leads immediately to the idea of using first-order tautological entailment instead of propo­ sitional tautological entailment as a logic for KR. First-order tautological entailment is to FOL as propositional tautological entailment is to PL. The syntax of the logic is the same as that of FOL, again without an implication sign. The semantics of the logic is very much like the semantics of FOL except for the provisions for the four relevance logic truth values.

The development of the semantics starts with first-order situ­ ations, the analogue of first-order models.

Definition 1 A situation consists of a non-empty set D, the domain of the situation, and three mappings, h, t, and f. h maps each function letter, fj, into a function from Dn to D, and t and f map each predicate letter, A'J, into an n - ary relation on D.

The mapping h is the usual mapping of function letters (and constant letters) into functions over the domain (and constants in the domain). The mappings t and f determine which atomic formulae are true and which are false and correspond to the in­ terpretation function of FOL. Two mappings are needed because an atomic formula can be assigned true, false, neither, or both.

Definition 2 A variable map is a mapping from variables into some set. Jfv is a variable map into D, z is a variable, and dis an element of D, then v; is a variable map into D with

vJ(y) = d, ify = z, and vJ(y) = v(y), otherwise. Given a situation, 8 1 and a variable map, v, a mapping, v;, from terms into the domain of 8 can be defined as follows:

v;(z) = v(z), if z is a variable,

v;(fj{tt, .. . )) = (h(fj))(v;(t1 ), ·. · ), otherwise.

Definition 3 The support relationships of first-order relevance logic are defined as follows:

8,vhA'](t1,····tn) iff (v;(ti), . . . ,v;(tn)) Et,(A'J)

8 1 1/ f=t A'J(tt, ... ,tn) iff (v;(tl), . . . ,v;(t,.)) E f,(A'J)

where 8 is a situation, v is a variable map into the domain of s, A'J is a predicate letter, and t; is a term.

This is just the obvious way of assigning meaning to atomic formulae. (The way to read s,v Ft a (s,v F/ a) is "s sup­ ports the truth (falsity) of a under v".) These relationships are extended to arbitrary first-order formulae by the following rules :

1. s,vf=1 -,a iff s,vf=Ja

8 1 vf=1 -,a iff 8,vf=1 a

2. s,vf=1 aV{3 iff s,vf=1 aors , vf=1 {3

s,vf=1 av{3 iff s,vf=,aands,vf=J/3

3. s, v Ft a 1\ f3 iff s, v Ft a and 8 1 v Ft f3

s,vf=1 al\f3 iff s,vf=Jaors,vf=Jf3

4. 8,v f=1 Vza iff for all dE D 8,vJ Ft a

8,vf=1 Vxa iff forsomedED 8 1 vJf=Ja 5. s,v Ft 3za iff for some dE D s,vJ Ft a

s,vf=1 3xa iff foralldED 8,vJf=Ja

It is easy to see that this semantics is very similar to standard Tarskian semantics except for the change from truth values of true and false to truth values of subsets of true and false . As argued above, this change has some benefits with respect to KR. As in the propositional case, there are no tautologies (sentences which are true in all situations) in this semantics.

First-order tautological entailment is then defined by:

Definition 4. If a and f3 are first-order sentences, a entails f3 iff for all situations, 8, and all variable maps, v, if 8 1 v Ft a then s,v Ft f3 and if s,v F/ f3 then s,v F/ a .

First-order tautological entailment captures a similar set of in­ ferences to those of the propositional version, where reasoning by contradiction and modus ponens are not valid. Based on the suc­ cess with propositional tautological entailment, one would hope that the first-order version is decidable. However, it turns out that first-order tautological entailment can be used to simulate first-order implication and thus is undecidable. This unfortunate finding destroys most of the utility of this logic for KR.

II A Variant of Relevance Logic

First-order tautological entailment, even though it is undecid­ able, is a very interesting starting place for further investigation because it forms a subset of FOL, based on a semantics that is reasonable for KR, and that is, in some sense, much weaker than FOL. What is needed then is a variant of first-order tautologi­ cal entailment which is decidable. One problem with first-order tautological entailment is that quantification is equivalent to infi­ nite conjunction or disjunction . It is this equivalence that makes quantification too powerful. For example, (Pa 1\ Qa) V (Pb 1\ Qb) entails 3z Pz 1\ Qz thus preventing the creation of an entailment algorithm similar to the propositional one.

To prevent this sort of entailment the quantifiers can be given an intuitionistic reading, under which interpretation the formula 3:z: P:z: would be read "there exists a known individual for which the P is true". To formalize this change requires a significant modification of first-order relevance logic semantics. Instead of talking about situations, sets of situations are needed. For 3:z: P:z: to be true in a set of situations there must be some domain object, a single object common across all the situations, such that P is true for that object in each of the situations.

The semantics of this variant starts out with first-order situ­ ations, variable maps, and the support relationships for atomic formulae just as in regular first-order relevance logic. However, the next step is the definition of compatible sets of situations. A compatible set of situations is a set of situations with the same domain and the same mapping of function letters to functions . In other words, the situations differ only on their assignments of truth and falsity. Given S, a compatible set of situations each with domain D, and v, a variable map into D, the two support relations for this logic, S, v Ft a and S, v F 1 a, are defined as follows:

1. S,v Ft V:z:a iff for all dE D S,v; Ft a S,vF1Vxa iff forsomedED S,v;F1 a

2. S,vF1 3:z:a iff forsomedED S,v;F1 a

S,vF13xa iff foralldED S,v;Fia

1. S, 11 Ft a iff for all 8 E S 8, v Ft a S, v F 1 a iff for all 8 E S 8, v F 1 a

for a quantifier free

where 8, v Ft a and 8, v F 1 a are as above. So 3:z:a is true in S under variable map v if there is some domain element, common across all the situations inS, which, when taken as the mapping of :z:, makes a true in each situation. The same formula is false if all domain elements, when taken as the mapping of :z:, make a false in each situation. This means that it is fairly easy for an existential to be true (although more difficult than in regular first-order relevance logic), but quite hard for it to be false, which is as things should be. (Note that the semantics given here is defined only on formulae in prenex form (PF) . There is a more complicated semantics for arbitrary formulae 2 which is equivalent to this one for formulae in PF and which has a very strong normal form theorem allowing all formulae to be converted to prenex CNF (PCNF) without changing their meaning. 3 )

The next step is to define entailments in this logic. As it turns out, there are three different versions of entailment here. Recall that if f3 follows from a, then f3 must be true whenever a is and, conversely, a must be false whenever f3 is. These two conditions are equivalent by definition in standard two-valued logic where being false is equivalent to not being true and also happen to be equivalent in regular first-order tautological entailment. How­ ever, the conditions are not equivalent in this variant, giving rise to three versions of entailment, t-entailment (written -+t), which carries the first condition, /-entailment (written -+ 1 ), which car­ ries the second condition, and tf-entailment (written -+ ), which carries both conditions.

So what · are these three versions of entailment like? First of all, they are all very weak-weaker than regular first-order tau­ tological entailment and much weaker than implication. Second, any sentence will entail its PCNF version and thus the order of conjuncts and disjuncts does not matter. Third, as in other rel­ evance logics, modus ponens is not a valid rule. This, in large part, is what makes the logic very weak. Fourth, sentences can be weakened by removing elements of conjunctions and adding elements to disjunctions. Finally, the entailments for quantifiers This shows that all versions of entailment have a universal en­ tailing a single instantiation of itself and a single instantiation entailing an existential. Also, a universal t-entails the conjunc­ tion of any number of instantiations whereas a disjunction of instantiations does not t-entail an existential. For /-entailment the opposite is true, and so, of course, neither way works for tf-entailment.

'The full semantics, along with proofs of all the theorems, can be found in [Patel-Sthneider, 1985J, an expanded version of this paper.

3 The splitting and combining of quantifiers allowed in FOL are not valid in this logic. For example 3z Pz V 311 Ql/ is eqwvalent to 3z311 Pz V Ql/ but not to 3z Pz V Qz.

Of these three versions of entailment, t-entailment seems to be the best for KR. It is preferable to tf-entailment, because it is stronger. It and /-entailment are duals but the entailments re­ tained by t-entailment (such as V:z: P:z: -+1 Pa A Pb) are more natural for KR than those retained by /-entailment (such as Pa V Pb -+ 1 3:z: P:z:). This is especially true when taking the intuitionistic view that to demonstrate the existence of an object a particular object must be produced. Further, this last type of entailment is a sort of reasoning by cases, a type of reasoning generally not valid in relevance logic. These considerations indi­ cate that !-entailment is the best of the three variants for KR so it will be emphasized from now on.

This logic would not be very interesting it if did not have a decidable algorithm for determining entailment. The first step in developing such an algorithm for this variant of relevance logic is a Skolemization theorem for entailment which states that for all three versions of entailment a -+ f3 iff a 53 -+ f3 sv, where a53 is a with all existentially quantified variables Skolemized and f3sv is f3 with all universals Skolemized. Then the following theorem characterizes t-entailment between sentences in normal form: Theorem 1 If a and f3 are sentences in Skolemized PCNF (a= Vi 1\ a; and f3 = 3z 1\ {3;) then a -+1 f3 iff there exists 8, a substitution for i, such that for each {3; there exists some a; and ,P, a substitution fori, such that a;,P ~ {3;8 (treating a;,P and {3;8 as sets of literals) .

An algorithm for computing entailment between two sentences in Skolemized PCNF can now be derived. Consider a and f3 as above . For each a; and {3;, compute a set of most general substi­ tutions 9;; such that for 8 E 9;;, a;8 ~ {3;8 . For each element of 9;;, define a new substitution the same as that element except that occurrences of elements of i are systematically replaced by variables occurring nowhere else. Let ill;; be the set of these substitutions and let ill; = U; ill;;. Then a -+1 f3 iff there is some substitution t/J which is the most general unifier of some {.p; : .Y,; E ill;}. The substitution t/J plays the role of 8 and all the .P in the theorem above.

This algorithm does demonstrate that !-entailment in this logic is decidable. Although its worst case behavior is exponential in the size of a and f3 it will always terminate and under normal conditions, where clauses are not long and there are many dif­ ferent predicates, will be quite fast . This characterization also gives a good indication of how !-entailment works showing that the five informal comments above are the basis for a complete de­ scription oft-entailment. Note, however, that it is the semantics that defines !-entailment, not this algorithm.

Although axiomatizations are not important in this view of KR, the logic presented here is sufficiently removed from familiar logics that an axiomatization of the three versions of entailment is useful for illustrative purposes. The axiomatization for entail­ ment given below was designed to be easily understandable. It includes an axiom simply stating the equivalence of a formula and is PCNF version. Although this is a decidedly unusual axiom, it is an effective statement and thus qualifies as a real axiom. Be­ cause of the lack of rules such as modus ponens in this logic, the only other way to get this equivalence would be to include a set of about fifteen axioms, an approach much harder to understand.

The axiomatization of entailment is then:

• L if a --+ (J then a --+1 (J and a --+ 1 (J
• if a--+ (J and (J--+ "( then a--+ "(, this rule also holds for t-entailment and /-entailment
• a """ apcNF where apcNF is a in PCNF, this includes axioms such as 3za """ -Nz-,a and 3z(a V (J) """ (3za) V (J for x not free in (J
• a --+ a V (J a II (J --+ a
• a~ --+ 3za Vza --+ a~
• if a~ --+ (3 then 3za --+ (J for a not in a or (J if a --+ (J; then a --+ V z(J for a not in a or (J, the same rules hold for t-entailment and /-entailment
• if a --+1 (J and a --+1 "( then a --+1 (J II "(
• if a --+ 1 "( and (J --+ 1 "f then a V (J --+ 1 "f

The last two rules serve to distinguish the three variants of en­ tailment from each other.

This axiomatization is sound for each variant of entailment and is complete for t- and /-entailment. One other interesting item about the axiomatization oft-entailment is that it is almost exactly equivalent to the syntactically motivated limitation of inference by Frisch and Allen called knowledge retrieval (Frisch and Allen, 1982].

III Conclusion

So what has been gained from this new logic? In essence, the logic provides a decidable subset of implication that does not contain any of the harder types of inference. It does not have the rule of modus ponens so no chaining can be done. It also does not do reasoning by contradiction or reasoning by cases. What is provided is a simple set of inferences, derived directly from the semantics, that performs retrieval of first-order sentences from a knowledge base specified as first-order sentences, much as database systems perform retrieval of facts from a database. Many inferences are not provided but this is the price that must be paid to guarantee decidability.

This decidability of entailment is not the only feature of the logic that makes it suitable for use in a KR system, although it is the most important one. The syntax of the logic is the same as that of FOL so, in some sense, it is possible to state in the new logic anything that can be stated in FOL. Also, because a subset of implication is provided, knowledge-based systems can treat sentences as sentences of FOL provided that they realize that the inferences provided are not complete. Further, since the semantics of the logic is closely related to regular first-order relevance logic semantics, the logic does not suffer from some of the problems and paradoxes of implication. Finally, the seman­ tics is firmly based on the usual model theoretic ideas of truth and falsity and serves to dictate the allowable inferences and not vice versa. This allows a simple characterization of entailment in terms of the truth of sentences. Together these points make the logic more suitable for KR than systems built by ad hoc modifi­ cations to a theorem prover or systems based on a particular set of inferences (and otherwise semantically unmotivated) .

However, the logic presented above is simply the start of work on a decidable first-order logic-based KR system. Although this logic, especially t -entailment, has many of the right properties required for such a system there may be stronger logics that retain decidability. For example, there are stronger versions of relevance logic that might be used as the basis of such a logic. The search for such a logic is, of course, aided by this demonstration of one logic meeting the requirements.

One way to strengthen the logic developed here without de­ stroying decidability is by adding to it a terminological reasoner like the terminological component of KRYPTON (Brachman et al., 1985]. To do this correctly would require building a full semantics for the combination of terminological reasoning and t-entailment, perhaps similar to the semantics in (Brachman et al., 1985]. A wrinkle in developing terminological reasoners for this new logic is determining which language to use . As shown in (Brachman and Levesque, 1984], terminologi~al reasoning can be computationally intractable for even very simple terminolog­ ical languages under standard semantics. If the KR system as a whole is to perform adequately, the terminological component must be tractable. One possibility for producing tractable ter­ minological reasoners is to perform the same sort of reduction on the terminological component as the logic devised here does on the assertional component. This would produce a semantics of frame subsumption that only catches the easy subsumptions and leaves the hard and time-consuming ones out.

Any KR system based on this new logic is going to be quite weak. One way of making such a system stronger is to make entailment be only the first method for answering questions. If entailment fails to produce an answer then a stronger method could be used, perhaps some domain specific method. The ad­ vantage of this is that entailment is a semantically motivated and well-defined notion so that it is possible to understand what its failure to produce an answer means. An interesting idea for the fall-back method is to use a stronger logical system. A first idea for such a fall-back is, of course, FOL, but other logics, such as regular first-order tautological entailment, could be used.

In summary, the decidable. first-order logic presented here forms an important first step toward building decidable seman­ tically-motivated KR systems.