Interpreting Descriptions in a Prolog-based Knowledge Representation System

Abstract

Descriptions provide a syntactic device for abbreviating expres­ sions of a formallanguage. We discuss the motivation for descrip­ tions in a system called DLOG. We describe two approaches to specifying their semantics, and a method for implementing their use . We explain why some descriptions should be given a higher order interpretation, and explain how such descriptions can be interpreted in the simpler logic of Prolog. The essential idea is to constrain the domain of descriptions so that an extended unifica.­ tion procedure can determine description equivalence within the Prolog framework.

lntroduction

A description is a syntactic device for abbreviating expressions of a formallanguage . For example, "The king of America is an old cowboy" might be rendered in first order predicate calculus as

and paraphrased as "there is an x who is the unique king of Amer­ ica, and that x has the property 'old-cowboy'." This expression can be abbreviated, in the classical way, as old-cowboy(,x[king-of-America(x)J); we say that "'" is used to form a definite description. In first order logic, predicate argu­ ments denote individual objects; the description operator ' has syn­ tactically "objectified" a portion of the original sentence.

The description operator has created a new syntactic object, but the meaning or denotatioil of that object may not be well­ defined. In this particular case, the existence and uniqueness pr<>­ perties presupposed by the above description have been the issue of much debate (e.g. , see [Kaplan75]).

Another example of descriptive abbreviation relaxes the unique­ ness assumption. For example, the expression "there is a person who is an old cowboy, and who is a Republican" might be rendered as 3x[perBon(x)l\old-cowboy(x)I\Republican(x)J . We might use another description operator, say E (read "an"), to provide the fol­ lowing abbreviations:

per8on(€x [old -cowboy(x )1\Republican(x )]).

old -cowboy( ex [per8on (X )1\Republican (X)]}.

Republican(€x [per8on(x )1\old -cowboy(x )]).

Each such abbreviation uses the description operator "€" to focus syntactic attention on the predicate "person," "old-cowboy," and "Republican," respectively. Again we must be concerned with the meaning of such descriptions. lt is somewhat natural to treat all of the above abbreviations are semantically synonymous-that all assert the existence of an individual object with the three proper­ ties. But this creates the need to explain their obvious syntactic differences in some other way. One hint comes from Hilbert and his use of description operators (e.g., see [Leisenring69, Robin­ son79]). Hilbert used the transformations

Vxl(x ) .. f(Ex~I(x ))

3x/(x ) .. f(Exl(x ))

INTERPRETING DESCRIPTIONS IN A PROLOG-BASED KNOWLEDGE REPRESENTATION SYSTEM

Randy Goebel

Logic Programming and Artificial lntelligence Group Computer Science Department University of Waterloo W aterloo, Ontario Canada N2L 3Gl

to simplify derivations. In other words, the transformations pr<>­ vided a computational advantage even though their meanings are identical. Robinson nicely expresses the intuition:

"lt would seem that Hilbert terms ... do capture a certain intuitive manoeuvre, which is worth formalizing: to intre>­ duce a unique name for an entity whose exiBtence has been established by some previous part of an argument, so as to continue with the argument and be able conveniently to refer to it if need arises." [Robinson79, p. 291]

This rationalization of the syntactic differences is related to the object-orientation of Al representation systems, where the ability to refer to and manipulate objects is argued to be of conceptual advantage in specifying symbolic representations of domains (e.g., [Moore76, Schubert76, Norman79, Bobrow77a, Bobrow77b, Hewitt80, Steels80, Attardi81]). (Descriptions have also been used within the logic database Iiterature (e.g., [Diiger78, Dahl80, Dahl82]).)

In Al, part of the reluctance to adopt a logical interpretation of descriptions must be attributed to the long-standing confusion and controversy about their meaning-logicians do not generally agree on the semantics of descriptive terms (e.g., see [Carroll78]). The reluctance to analyze descriptions in a logical framework probably results from a traditional misunderstanding of the roJe of logic ( cf. [Hayes77]).

Descriptive terms in DLOG

DLOG is a representation system implemented in Prolog. It is a "system" in the sense that it provides a general representation language (including various kinds of descriptions), a query evalua.­ tion mechanism, a simple integrity maintenance scheme, and an abstract description of the intended semantics of the representation language independent of implementation. Although originally developed to to help describe concepts in the Department Database (DDB) domain, the DLOG system is domain independent in the sense of traditional data base management systems.

The descriptions in DLOG are motivated by a desire for brevity in describing undergraduate degree program requirements in the DDB. For example, suppose that "CS115 or a 1.5 unit elective" is a requirement. The desire is to avoid an expression like

requirement(BScOS,CS115)

V [3x[requirement(BScOS,x)

1\unitB(x ,1.5}1\elective(BScOS,x )]]

in favour of something like

requirement(BScOS,

~ex[x-�S115

vx-y[elective(BScOS,y)

1\unita ('II ,1.5)]])

by using some appropriately defmed description operator "~t." Simi­ larly, descriptions of sets were seen to be useful. For example, the expression "at least 12 CS courses" might suggest the use of an expression like that in fig. 1. where the components grouped bv the left brace must be written once for each set of twelve CS courser. This is clearly a tiresome way to express the assertion, and furthermore, would require extensive modification after any new CS course was created (e.g., by adding an assertion like "CS­ course{CS123)"). We would prefer something like

where "~t" isanother appropriate description forming operator.

Similar motivations have given rise to the following description forms in DLOG.

Definite individualB. DLOG's definite individual provides a shorthand syntax for referring to a unique individual whose name is unknown. Intuitively, the variable binding symbol 'L' can be read as the English definite article "the." For example, we might refer to "the head of Computer Science" as

lf our description distinguished the intended individual, then we need never know which individual constant actually names that domain individual. We normally expect that the variable bound with the symbol 'L' appears somewhere in the formula that consti­ tutes the body of the description.

Indefinite individuals. When we need to refer to "any old ct" with some property specified by a formula '4>(a)', we can use an indefmite individual. We use the variable binding symbol 'E' as the English indefmite article "a" or "an." For example, "a course with course number greater than 300" might be referred to by the inde­ fmite individual

Al; for defmite individuals, we normally expect that the variable bound with the symbol 'E' appears somewhere in the formula that constitutes the body of the description.

Definite Bets. A definite set is used to refer to a set consisting of all individuals that satisfy some property. The name "definite" is used to correspond to its use in "definite individual." A definite set is "definite" because it refers to all individuals in the current knowledge base that satisfy the specified property. For example, "the set of all numerical analysis courses" might be designated as

Here the braces "{ }" serve as the description forming symbol.

Indefinite sets. lndefmite sets are "indefmite" in the sense that they refer to one of a set of sets. Like indefinite individuals, they are intended to be used to refer to "any old set" that is an element of the Bet of setB that satisfy the specified properties. For example, the indefinite set

is the DLOG term that represents an arbitrary set that is a member of the set of "all 3 element sets of courses."

Lambda constanta. Lambda constants were introduced to cap­ ture a kind of individual occurring naturally in the DDB domain: regulations. For example, in describing a typical degree program, we must classify all kinds of requirements for that program, e.g., "nobody can register if they're under 16 years old" refers to a regulation that uses the Iambda constant

requirement{BScOS,OS115)

1\requirement(BScOS ,OS215)

1\

l\requirement(BScOS,OS442)

requirement{BScOS,OSU8)

l\requirement(BScOS,OS215)

1\

l\requirement(BScOS,OS442)

Figure 1. " ··· at least 12 es Courses"

In this way regulations can be placed in relation to other individu­ als and sets, e.g.,

program -prerequisite(BScMajors,

first, >-.x 1 [3x2[age -of(xt.x2)/\x2öi!:16]])

says "one of the regulations for the first year of a BScMajors prcr gram is that an individual be at least 16 years old."

Semantics of descriptions

W e have suggested that there is more to the meaning of descriptions than their denotation in a first order language. In DLOG {and, we claim, in any representation system) there are at least two aspects to the meaning of descriptions.

One important aspect is the traditional specification of denota­ tional semantics along Tarskian lines: given a well-defined class of formal expressions, one specifies a systematic way in which expres­ sions and their parts can be attributed denotations in an interpre­ tation. Two assumptions underlying this methodology are (1) that the expressions in question are being evaluated as to their truth; and {2) that the denotation of complete expressions depends solely on the denotations of their parts.

Another important aspect, often overshadowed by concerns of the former, is the intended meaning of such formal expressions when they are being formed (e.g., by a user), during their use in assertions (e.g., when adding facts to a knowledge base), and during their use in queries ( e.g., when requesting that facts be verified with respect to a knowledge base). In this regard, the use of descriptive terms impinge on philosophical problems associated with names and their use (e.g., [Donnellan66, Brinton77, Katz77, Lin­ sky77]). A most common example is the difference between referential and attributive use of descriptions. The issue is whether a description is intended to refer to a known referent {referential), or unknown referent (attributive). Apparently only a few Al researchers have considered the problern (e.g., [Schubert76, Ortony77]). These and related issues are further discussed in [Goe­ bel84, Goebel85]

V

To attempt a coherent description o! a Prolog-based mechanism Cor proving existential formulas in DLOG, one must flrst select a methodology for speci!ying the meaning of descriptions. The most common method is Russell's contextual defmition [Kaplan75]. Con­ textual defmition is essentially macro defmition, e.g., any string of the form ~'z[!JI(z)J) is replaced with

The meaning of the description is specifled by the logic from which the defmition is talcen.

A related issue is the meaning of descriptive terms when their proof-theoretic preconditions !ail. For example, a constructive proo! of 3z~z)A!JI(z) will produce a referent o! the description in ~{[!JI(z)]), but what does the latter mean when a proof o! the !ormer fails! Under one popular theory [Kaplan75, p. 215], the meaning of such descriptions whose logical preconditions !ail have been specifled by convention, e.g., a failing description refers to a designated null constant that lies outside the domain of discourse.

First order semantic:a

One possible choice for the description defming language is flrst order logic. The overwhelming advantage of fll'8t order semantics is simplicity; an abstract, implementation independent speciflcation oC semantics is worthwhile in that it provides a simple way to understand the complexity of the actual system.

Using fll'8t order logic, most of the intended meaning of DLOG descriptions can be specifled in a relatively straightforward way. The individual descriptions ( defmite and indefinite) are specifled as above; sets can be axiomatized with a aet relation and a set membership relation "E" (DLOG set theory is fmite, thus very sim­ ple). However, Iambda terms rely on semantic notions foreign to flrst order logic; their deflnition here requires the use of meta language concepts.

Contextual deflnitions for set descriptions are defmed as fol­ lows. The sentence

contains no set variables--the term {z1:!JI(z1)} describes a set con­ sisting of all individuals a such .that !JI(a) is true. In a fll'8t order language that distinguishes set variables X 11 X2, X3, ··. , the defmi­ tion of sentence ( 1) is rendered as

This can be read as "there is a set X 1 that has property 41, and aJJ individuals z 1 in the set have property '1'." Because the only defm­ ing property of a defmite set is the property attributed to each of its members, its uniqueness is easy to establish. In contrast to defmite individuals, there is only one extension for each defmite set so a further speciflcation of uniqueness is not required.

The contextual defmition of indefinite sets can be approached in a similar way. We can view

as having the defmition

This says that "some set X 1 that has the property 0 and whose elements each have property '1', also has property 41." Intuitively, the indefmite set construction specifles a set that flts the descrip­ tion, similar to the way that an indefmite individual specifles an individual that .flts its description.

DLOG Iambda constants provide the user with a method o! asserting axioms about unary predicate abstractions, intuitively interpreted as regulations. For example, the assertion can be interpreted as asserting that the property 4> is true of the regulation named by >.z1 !JI(z1). These terms are use!ul because they allow a user to assert relations about properties. Intuitively, Iambda constants are most reasonably interpreted as a special kind of constant, indexed for retrieval by the terms they appear with. However, they cannot be manipulated without the defmition of an application mechanism. This defmition relies on a meta relation aatia /iea, which is defmed in terms of the provability meta relation deriooble (cf. [Bowen82]}. The aatiafiea meta predicate then pro­ vides a method for testing whether an individual satisfles the rela.­ tion denoted by a DLOG Iambda constant. That is,

For any individual constant a of a DLOG database DB, aatiafiea(a,>.z1 !JI(z1)) holds iC and only if !JI(a) holds in DB. An assertion of the form

is interpreted to mean that, in the current database,

is derivable. Indeed (2) is a clumsy alternative to (3), but by using Iambda constants in this way, we not only provide a way of assert­ ing axioms about regulations, but also a way of using those regula.­ tions in question answering. The aatiafiea predicate provides the mechanism !or applying Iambda constants as unary predicates o! the current database.

An example will illustrate. The experimental DDB domain requires the description of degree requirements, which can often be expressed as Iambda constants, e.g., the assertion

states that "an enrolment requirement of the BScCS degree is that the candidate's age is greater than or equal to sixteen." The Iambda constant format allows the requirement to be asserted and queried, and the aatiB/iea predicate provides the mechanism to pose a query like

that can be read as "Has John satisfied an enrolment requirement for the BScCS program?"

Notice that, in the DDB domain, degree requirements are most naturally conceived as conditions which must be satisfled. Since degree programs are distinguished by their various requirements, it is most Straightforward to describe degree program requirements as relations on degree names and conditions tobe satisfled-in DLOG, as Iambda terms.

Qf COUrse there are alternatives to the use of this Special term. For example, the meaning of sentence (4) might be rephrased in. terms of a standard fll'8t order language as

where we would use BScCS as the name of a degree program and modify the predicate aatiafiea to correspond more closely to our intuition regarding what one must do with degree requirements. This alternative has a more straightforward meaning since there are no "special" forms. But now there is no way of asking what the requirements o! the BScCS program are, short of providing another non-fU'st order primitive for manipulating sentences. For example, to answer the equivalent of query (5) in the alternative notation, we require an operation that retrieves a sentence o! the form (6) from the current datab1111e, and then returns the conse­ quent of that sentence 1111 an answer.

Lambda terms can be manipulated with a siandard (sorted) proof procedure to answer existential queries about requirements; they are simply retrieved and bound to existential Iambda variables 1111 in normal answer extraction. Furthermore, they can be used in conjunction with the satisjie11 predicate to determine if an indivi­ dual h1111 satisfied a particular requirement.

The eaae for hisher order aemantlea

The clear disadvantage of fli'St order semantics is an inability to directly deal with higher order concepts. Though DLOG domains are restricted to be fmite and no abstraction is permitted in the DLOG proof mechanism, the specification of certain DLOG expres­ sions in a frrst order way is contorted and mitigates against the desired semantic simplicity. This is most obvious in the way that Iambda terms must be explained in terms of meta relations.

One alternative is to use a second-order intensional logic, 1111 used by Montague to explain such concepts as "obligation," "event," and "task." For example, Montague's formalization of the concept of obligation [Montague74, p. 151ff.] corresponds weil with the use of Iambda terms in the DDB application of DLOG.

Montague 's · system provides a natural semantics for DLOG 's Iambda terms, and is obviously powerful enough to be used to describe the rest of DLOG's descriptive terms (individuals, sets). Only DLOG Iambda terms require this treatment, but Montague's system provides a rather more uniform treatment of DLOG's semantics than is possible in weaker systems.

The complete picture of Montague's system requires careful study, but the essence can be explained in a relatively Straightfor­ ward manner. An essential concept is the classification of individu­ als into categories of two different kinds. Each n place predicate constant has an associated type <s0,111> · · · Bn-1> that indicates the kind of object that can appear in each term position: s 1 --1 specifies a standard · individual; 111 -o specifies a proposition; and 111 01!::1 specifies a 111-place predicate.··

For example, a predicate constant P of type <-1,1> takes individual constants in its fli'St position and unary predicates in its second. In the Department Data Base domain, the 3ati11/ie11 predi­ cate constant h1111 type <-1,1>, e.g., the a.ssertion

has an individual eonstant 'fred' in the frrst argument position, and a Iambda constant in the second argument position. The first denotes an individual object (the person with name 'fred'), and the second denotes a predicate specifying the property of "x complet­ ing the course CS115."

The meaning of the above assertion is assigned in a way that introduces the seeond and most important differenee of Montague's system. The assignment of truth values to sentenees is an inherently two phase proeess. Ar. Montague explains [Montague74, p. 157], an interpretation assigns intension11 to symbols, and a model assigns extension11. Extensions include the standard objeets well-known from traditional Tarksian semanties, 1111 weil as sets of sequences of individuals. lntensions are functions from possible worlds to the universe of individuals. They are introduced in order to distinguish the sense or abstract meaning of a predicate from its denotation in a particular possible world.

The complexity of Montague's complete system can be perplex­ ing, the essenee of the system provides a rieb speeification langnage for DLOG's complex objects. Some of the eomplexity dissolves because of the simplieity of DLOG theories: they are fmite, and the intended interpretation is over a highly restricted domain. This simplicity eonstrains the number of possible worlds that can serve as interpretations for DLOG theories (thus, for example, providing a restricted interpretation of "C"). In the DDB example, the intended interpretation together with partial knowledge of each partieular student identifies the intended possible world for seman­ tie interpretation.

· Here 11 St.andard individual" meana tbe uaual notion or &n individual in a. IIra~ order model.

·· See jMon~ague74, p. 150j. Tbe no~ion or prediea~e uaed in ~bia eon~ex~ ia sometimes ealled a 11 relation in intenaion."

In Montague's second order logie, the meaning of DLOG Iambda expressions is given by expressing them as unary predicate eonstants. For example, the DLOG formula

is written 1111

In general, the 'u~' syntax is shorthand for

Montague uses the symbols 'A' and 'V' for 'V' and '3', respectively. He also uses brackets where parentheses are typieal, e.g., P[x] for P(x ). In addition Montague employs the symbols rp and 'C', read as "the" and "neeessarily," respectively. These latter symbols are used to form names of predicates. DLOG's Iambda symbol '}o.' plays the same roJe as Montague's ,., symbol.

Formula (11) is intended to mean "a requirement of the BScCS program is to bear the relation completed to the eourse CS115." The intensional semanties provides a way of admitting different intensions for the completed relation,_ e.g., eompleting a course might have different meanings in different possible worlds. In the ease of DLOG, the partieular possible world in whieh symbols are assigned extensions is fixed to be the Departmental Database.

The second order power of Montague's logic provides the expressive ability to assert relations on predicates: it is the property of completing 08115 that bears the requirement relation to the program B8cC8, and not any particular extension of the property.

Again, the applieation of Iambda terms can be explained with the aid of a relation ealled 11atisfie3 . However, in Montague's language ~Jati11/ie11 is a predicate constant of type <-1,1> and is interpreted (in a possible world i in a strueture <I,l.! ,F>) as a ·relation <I,U,<I,U>> where I is the set of possible worlds and U the universe of possible individuals. (So <I,U> is a unary relation, <I,U,U> is a binary relation, ete.)

Computlns wlth deserlptions by extended unifieation

The meehanism for manipulating DLOG deseriptions is imple­ mented in the Horn clause logie of Prolog. Adopting one of the above approaches to semanties means to adopt the eorresponding view of what the DLOG proof proeedure is doing. The simplest way to view the DLOG proof procedure is as a Horn clause prover extended with meta relations to handle the non-Horn features of DLOG. However, we speeulate that the theoretieal foundation of a higher-order proof proeedure based on unifieation due to Jensen and Pietrzykowski [Jensen75] will provide. the eorresponding view for the Montague system. Here the intuition is to eonsider the DLOG implementation 1111 a restrieted implementation of their unif­ ication proeedure for generat type theory. Wehave not yet investi­ gated the possibility of adapting Jensen and Pietrzykowski's pror eedure for use in an intensionallogic.

Instead of extending Prolog's Horn clause theorem prover to handle the expressions that arise from any method or contextual defmition, the unification algorithm ean be augmented to provide the correct matehing of deseriptive terms. Ar. others have observed (e.g., [Clark78, van Emden84]), any assertion of the form

where t 1 , 1:Si:Sn are terms, ean be rewritten as

<l>(x"x2, · · · x,.)Cx1-t11\x2-t21\ · : . 1\x,.-t,. and implications

can be rewritten as

where the x1, 1:Si:Sn are new variables not occuring in the original formulas. In DLOG, the equality expressions arising from this transformation are determined from within unification. In a sense, some of the complexity of derivation is off-loaded to the "pattern matcher" (cf. [Reiter75]).

The idea of extending a resolution proof procedure's power by augmenting unification was f1rst suggested by Morris [Morris69], who proposed that equality be manipulated with so-called "E­ unification." There have been many other related proposals includ­ ing Stickel [Stickel75], Morgan [Morgan75], and Kahn [Kahn81] . Of related interest is the representation language KRL [Bobrow77a, Bobrow77b, Bobrow79], which relies on a complex "mapping" pro­ cess on several different kinds · of object descriptions called "descriptors." We argue elsewhere that KRL's mapping can best be understood as a elaborated unification scheme [Goebel85] .

Returning to the handling of descriptive terms by augmenting unification, we cite Rosenschein on the advantage of embedded terms:

... the data object is kept small and "hierarchical" so that where an exhaustive match must be performed, failure can occur quickly. That is, deep, heterogeneaus structures are preferred to broad, homogeneaus structures. For example, {(){()()}} is better than {{}{}{}{} }.t

We view Rosenschein's claim as support for the interpretation of descriptions as embedded terms, rather than as their contextual definition by rewriting.

The DLOG unification algorithm is invoked by the DLOG derivable predicate, similar to the way Prolog's derivation pro­ cedure uses a built-in unification algorithm. Intuitively, whenever a unification must be performed and there are special DLOG terms to be matched, standard unification is intercepted, and DLOG unif­ ication is used. For example, suppose that the two terms ex <l>(x) and Fred are to be unified. The applicable DLOG unify axiom is

where apply binds the symbol "Fred" to the Iambda variable "x" and invokes derivable .

The DLOG unification definition uses an organization similar to the LOGLISP system of Robinson and Sibert [Robinson80, Robin­ son82] . LOGLISP consists of a logical proof theory embedded within LISP, and allows the invocation of LISP by the theorem­ prover, and the theorem-prover by LISP. Similarly, the DLOG derivable procedure can invoke the standard Prolog proof pro­ cedure, and· both are accessible from with DLOG's unification matcher.

In general, the correct "unification" of the DLOG extensions requires a derivation procedure more powerful than that provided by Prolog. For example, the equivalence of two Iambda expres­ sions, e.g., >.x <l>(x) and ).y !il(y) can only be established if it can be shown that Vx<l>(x)·!il(x) follows from the current database . The current DLOG unification procedure uses a local context mechan­ ism to derive this equivalence. It is also the case that disjunctive terms require a more general proof mechanism, since a proof of 3x cf>(x )V!il(y) ca.D.not be handled by the current implementation, although a special heuristic will use a notion of partial proof to retrieve facts relevant to such a query [Goebel85] .

t 1Rosenschein78, p. 6341.

Bobrow and Winograd's description of KRL's matehing frame­ work (see [Bobrow77a, §2.5]) also uses the notion of partial match. Their discussion about what is deductive and what is heuristic is suCficiently interesting to pursue here because DLOG already pro­ vides some of the features of KRL's "flexible" matching.

Recall that the basic data type of KRL is a frame-like structure called a "unit." A unit is a collection of "descriptors" that attribute various properties to the unit in which they appear. Of interest here are the various ways in which units can be related by mateh­ ing their descriptors. For example, consider KRL's matehing by "using properties of the datum elements" [Bobrow77a, pps. 23-24] :

Consider matehing the pattern descriptor {which Owns {a Dog)) against a datum which explicitly includes a descriptor {which Owns P!uto). The SELF description in the memory unit for Pluto contains a perspective indicating that he is a dog. In a semantic sense, the match should succeed. It can only do so by further reference to the information about Pluto.

This form of matehing already exists in DLOG. For example, the KRL descriptors {which Owns (a Dog)) and {which Owns P!uto) might be rendered as 3x[Owns(x,fy[dog(y)]) and 3z [Owns ( x ,P!uto )], respectively. If we have the fact that Pluto is a dog (i.e., the assertion dog(P!uto )), DLOG unification will suc­ cessfully unify the above pair by recursively proving that dog(P!uto) follows from the knowledge base.

Several other forms of KRL matehing fall into similar categories, where a recursive proof will provide the inferences required to demonstrate the equality of descriptions. The only clear instance in which partial matches arise are due to resource limitations. Again the partial results determine whether the current line of reasoning is to continue (perhaps given further resources) , or to be abandoned.

Coneluding remark.s

W e have argued that there may be more to the meaning oi descriptions than their traditional Tarskian semantics, especially as regards the way that they are manipulated within a logic-based representation language. We briefly outlined the kinds of descrip­ tive terms included in the Prolog-based DLOG representation sys­ tem, and discussed various ways in which those terms could be interpreted. Lambda terms, useful in a particular application, do not have an obvious formal meaning and suggest the need for higher-order semantics. Regardless of which semantic specification is selected, the notion of extended unification can be used to mani­ pulate embedded descriptions. With some effort, the extended pro­ cedure can be viewed as providing either metalogical or higher­ arder proof theory extensions.

Finally, it is important for representation systems to exploit the computational as weil as the traditional denotational meaning of descriptions. The proceduralists have been saying this for years; we claim that logic can contribute to an understanding of the com­ putational use of certain kinds of descriptions.

Acknowledgementa

David Poole suggested many improvements to an earlier draft of this paper. Richard Robinson pointed out the relationship between DLOG's Iambda terms and Montague's formalization of obligation.