A Programming Tool for Management of a Predicate-Calculus-Oriented Data Base

Abstract

This paper describes a USP program, called PCDE, for storage and retrieval in a data base of £redicate £alculus (PC) formulas. The PCDB package uses standardized representations of PC formulas, where ground unit clauses are stored efficiently , e.g. on the property-lists of their argJrnents, and other clauses have other representation. The major part of the PCJE package is a function generator, which acceDts declarations of PC relations and func~ions, a::d l.tlich also accepts "rules" ( = non-gro~~d axior.s intended for use in deduction)

A PR(X;!WfliNG TOOL FOR MANAGEMENT OF A PREDICATE-CALCUWS-ORIENTED DATA~

Erik Sandewall Uppsala University Uppsala, Sweden

In the design of such programs , it is crucial to find a good representation of one's data. Prograrrm:ing languages like LISP, PL/I, or SIMULA 67 offer a machine-oriented data struc­ ture; for example, LISP offers the use of property-lists , and SIMULA 6 7 offers the use of Hoare's record structure. HCM'ever, it is often desirable to find a more problem-oriented rep­ resentation, such as nested trituples, colored graphs, or "semantic nets".

Declarations and ~les are used to generate efficient code for storage and retrieval of "facts" (usually = ground unit clauses) in and fron t~e data base . This generation process may be c.'larac:erized as a "cx:pi l ation" of the r.rles (fron predi cate calc·.rl·.rs to LISP).

Yev words and ol::'ases

Axic~ cc~ila::cn, deduction, function gene­ rator, ~IS?, ?artial evaluation, retrieval.

:~ctivation

''any progra-:n:..~g tas!-:s in artificial intelli­ gence req·.r:re the r-.anipula-cbr: of small data t=.ses . Quest:.on-a.'"ls·..Jering prograr.s rra.intain a data tase cf accumulated facts, anc'. inquire t~e ja"':a base fer answers to questions. Robot progra.--::s ;;-.a.ir.-:ain a data base whic'"'. describes -r':e ro::ot ' s er:v:ronr.er.t. Advanced CAJ. programs r..aintai!i a data base of the S>.;t"iect-matter that the·; ~:ave to teach. Si""1Lllated scientists (e.g. th~ Dendral p!"'gra"r.) !T'.air.tain a data base o: kno·,l- h0\·1 in a na!"''CM but deep field of ::·r..an ·k:'.~1ledge . 'J!ese prograr.s, and other silrilar or.es, need t o perforr.. cor..plex retrieval operations (anc'. sometimes, reorgar.ization) in

t~,e Cat 3 :;a.se.

( Y.) :r.:s res ear~: ·.-~as suppc'"ed i:-: part by the :;· ... 1'=1: s:--. : :a.: ·~al Science :<esea!"cr. Cot.L'lcil (ccr.tra.':t ::r..r 2E5u- 3)

Predicate calculus notation is often used as such a "high-level data language". The SRI A. I. project uses predicate calculus for their robot project (see Nilsson, 1969) and for question-answering (see Green, 1969). Two diffe­ rent methods for using pred1cate calculus as a data language in program manipulation programs have been proposed by Burstall (1969) and by Manna and Waldinger (1970). Eurstall (1970) has proposed a set of conventions for expressing the deep structure of natural language in predicate calculus, and a similar proposal has been made by the present author (Sandewall, 1970) . The list can be continued.

Predicate calculus offers the user two major advantages: First, it is a versatile notation, and second, the user ca'1 express the logical properties of his data throug.": a set of axioms. Tl:ese axioms can be used as a theoretical tasis fer the program, or they can be given to a theorer.-prov ing pro gran (such as QA3 , see Green , 1969 ). In the latter case , the theorem-provrr.g­ program "interprets" the axioms. This was disc·.rssed in Green, op.cit ., page 131. In the former case, the same axiorrs have been manually re-written ("canpiled") into a program. Usir.g a theorem-proving program is r.ore convenient, but a tailor-made program can be expected to be much more efficient.

Topic of this paper: the PCDB

pa=kage

:'his paper describes an existing USP "program" (or to be precise, function package) which com­ t:.:.es the generality and cor.venience of a -:heore~-proving program with the relative effi­ cie:~cy of tailor-made prol'!'ans. Our progra.':' is called PCDB (for "Predicate Calculus Data Base"), and it i s a function generator. PCDB takes the follo..~ing types of input :

declarations of the predicate calculus rela­ t1ons and fu~ctions that the user wants to utilize;

facts, i.e. gruund unit clauses which are 1ntended as contributions to the data base;

questions , i.e. unit clauses which are to be proved from the data base. Question clauses may be gruund (for closed questions) or nan­ ground (for open questions);

rules, i.e. non-gruund (and usually non-unit) clauses which are to be accUlThllated, and later used for forward deduction from facts and/or for backward deduction in answering questions.

When t he package receives rules, it generates "code" (i.e. LISP S-expressions) that col"l"es­ ponds to these rules (i.e. it "compiles" the rules), and when it receives facts and quest­ ions, t his code i s utilized. Dec:arations set certain flags and properties w~ich govern subsequent code generation.

The PCDE package is useful in pro!:llem environ­ ments where there is a large and open-ended data base of "facts" (in the above sense of the word) and a relatively small and lL~ted number of "rules". Question-answering appli­ cations and 8\.II'Stall' s nota-:io:1 for prograrr. descriptions sa-tisfy this requirement. - The package is not useful in problem environments where the major pa.~ of the data base consists of "rules". Manna's approach to program analy­ sis is an exa-:1ple of such an environment. For such applications, conventional resolution progra::LS seem rrore suitable.

Example of predicate calculus usage

Before we proceed to a detailed description of PCDB, let us give an example of the use of predicate calculus as a high-level data language. With this example, the reasons for the desi!?Jl of PCDB will be rrore transparent.

Suppose we want to perform tha-: standard exer­ cise: writing a kinship handling, question­ answering program. Some s~le kinship rela­ tionships may be expressed in predicate calculus as

Sibling(Jesper,Bodil) Male(Jesper) Father(Jesper) = Edvin Wife (Edvin) = Edla etc. ("Sibling" stands for "brother or sister"). For simple facts there is no essential diffe­ rence in effort between making these predicate­ calculus statements and making the obvious property-list storage instructions. HaNever, in rrore complex expressions, like Sibling( Father(Hedvig), Wife(Neighbor (Halvard))

(for "Hedvig's father is a sibling of Halva.""d's neighbor's wife) the predicate calculus fo::T.:·c~­ lation is probably rrore convenient than what ·we could immediately do with e.g. property-list storage instructions. In this sense , the nota­ tion is "high-level" and "problem-oriented".

Moreover, predicate calculus permits us to sta~e general axioms, which characterize these kL~­ ship functions and relations, e.g.

• (x) Male(x) - ,rerrale(x)
• (x) Child(x,Father(x))

(x)(y)(z) Child(-x,y) J. Child( x ,z) ~ y = z V Sibling(y,z)

If we write a direct progra":'. for the kinship exercise (without the support of any standa.re progra;;,) , then the infonna:tion contained in these axioms lln.lst someho..~ go into that progra:: .. Norr.1ally, it goes into the retrieval part, bu~ some of the axioms could also go into the storage part. For a trivial exa'9le, the f i rst axiom could col"l"espond to a segment of t he retrieval procedure which says "if it has bee:-. asked whether x is male, and if there is nc­ :imnediate infornlation in t'le data base sayi."'lg that he is or isn't, then ask as a sub-quest:o:-. whe1 er x is female, and negate the answer ", a"'ld to a col"l"esponding segment for the case where x is female. But alternatively, it coulC correspond to a section of the storage proce­ dure which says "if you have to store that x is male, then store also that x is not female" a~d sh'.ilarly for the syrrvnetric case. The retri eva::. procedure does backwa."'Cl deduction, whereas t he storage procedure does forwa."'Cl deduction. It i s one purpose of PCDB to generate code for a~d t o administrate backward and forward deduction. With this example as a backgruund, let us nc:JV.' describe the PCDB program tly tracing what happens when some selected expressions are give~ as "input", i.e. as argurre:1t to functions in t he package.

Declarations of relations

LIS? atoms areused for relations symbols, function symbols, and otject symbols. The pur­ pose of declaring a relation is to provide it with a number of functions (lambda-expressi ons ) which are properties on the property-list of the relation. For example, a bina.~ relation Fat'ler

(such that Father(x,y) means "y is the father of x") might be associated wi<:h at least the follo.ving lamtx:la-expressions:

These properties are used for assertions, for closed questions, and for ope~ questions, respectively. Additional properties are needed for deduction, for undoing previous assertions, etcetera. It would have been possible to design the PCDB package so that all of these properties are generated and assigned at the point where FATI-!ER is decla.-ned to be a binary relation. Ho.vever, we have preferred to do things as follo.vs in PCDB:

at declaration time, some flags are put on the property- llst of t he new rela<:ion. These flags correspond directly to the information in the declaration. No functional expressions are generated .

when a fu.~ctional proper:!)' is needed, the system asks for it by doLng e.g.

getd fl"t{ FATI-!ER, TESTDEF)

where the fu.11ction getdfl t is defined essecti­ ally as

getdflt [a,i) get[a,i) V putprop[a,i[a), i)

The first time the TESTDEF property of FATHER is asked for, the value of ge<:[FATHER, TESTDEF) is NIL, so testdef[ FATHER) is eval'.Jated, stored as a property, and renrrned as a value . This is the req'..lired function definition. In other words, the functions testdef , storedef, etc. all return lambda-expresslons as values.

011 each succeeding call for the TESTDEF proper­ ty , it can be retrieved from the property­ list, and it need not be computed again. (The value of the function testdef is meMOized).

This design has several advantages:

• (a) functional properties are not generated unless they are really needed;
• (b) the user may make several declarative
• statements, provided they have all been given before the first time the relation (or function) is used;
• (c) declarations may be implicit. Functions like testdef must clearly inquire the property-hst of their argument for the flags that were assigned by the declara­ tion. If these flags are not present, then testdef (and similar functions) can com­ pute default values.

In fact, this is a simple example of backward deduction.

The PCDB package contains various service functions for doing declarations in a conveni­ ent way. Ho.vever, let us ignore the conven­ tions of those service functions, and look at their effect in the example of the relation Father, where the declaratbn r.Ug.l)t have i.rrrne­ diate effect of putting the following proper­ ties of the property-list of the atom FA'IHE:P:

The functions testdef[r), storedef[r), etc. have been defined so as to branch on get[rfRELTYPE), get[r,LOCAITD), etc. and to return a unctional expresslon in each case. With the given decla­ rations, the above-mentioned lambda-expressions will be obtained.

The PCDB package recognizes different kinds of relations, with different numbers of arguments (one, two, three, or rrore), different storage conventions (on property-lists of arguments, on property-list of relation symbol; hashed in an array is planned, etc. ) and otl)er idiosyncra­ cies. Since each relation has its o.vn storage and retrieval routines, it becorres possible to assign tailor-made routines automatically to all relations.

The path of an assertion

let us continue the exan;>le with the relation Father. The PCDB package contains a standard function assert, where evaluation of

assert[FATHER,DICK,JOHN]

will cause the following flow of control:

1. assert checks the well-formed-ness of the argurrents, and calls

sysassert[ 1, (FATHER DICK JOHN) ]

The number 1 is inserted as a default value, and limits the number of H-expressions that are generated in forward deduction (see below). It could have been given explicitly as a first argurrent to~·

2. sysassert is defined in principle as follows:

sysassert[n,guc] = if test[guc] the~ T - --else

prog2[ store[guc], apply[get[car[gucr,­

ASSERTDEF] , [cdr guc ]]]

with

store[guc] apply[ get[car[guc],STOREDEF], cdr[guc]]

and test[guc] = apply[ get(car[guc] ,TESTDEF], cdr[gucll

Thus we first use the TESTDIF property of the atom FATHER as a function, with the list (DICK JOHN) as an argurrent list. Normally, the relationship was not known t o the system before. It is then stored by the STOREDEF property. Finally sysassert applies the ASSERI'DIF property of the atom FATHER to the list (DICK JOHt\). The ASSER:'DIF property has in principle the form

(lAMBDA (X Y) (PR(X;.\J

(PRCh )

(FROG )

(PRCh ))

vtlere each prog-expression is a compiled axian in forward usage. (In some cases, the systerr. may have been able to simplify the expressions so II!Uch that the ~ vanishes). Initially, the ASSERTDEF property has the f om

(LAMBDA (X Y) (PROGN))

and it is then updated each time an axiom is given to the system. Compiled forward axioms call sysassert with their conclusion, so triggering may be continued recursively. There are other functions which are similar to assert, but which do slightly different things. For example, the function claim makes a search to check that the new fact does not contradict the old data base, before it stores the new fact and triggers side-effects.

A user may often want to call an arbitrary LISP function during forward deduction, and to write e.g. the "rule":

P[x,y] :::> print[x]

This is easily done in PCDB by assigning a suitable STOREDEF property to the atom PRD~, or by writing the rule as

P[x,y] ::::> Do[print[x]]

where the STOREDEF property of the atc:rr. DO is simply

(lAMBDA (X) X)

Relations used in backward deduction axioms car. be defined similarly. This is equivalent to t he "predicate evaluation" feature in various reso­ lution programs.

The path of a closed question

Closed questions are represented as ground ur.i: clauses ("guc"-s), just like facts. The follo­ wing sta~dard functions are presently providej in PCDB for answering closed questions:

test, which simply checks whether the clause has been explicitly stored

search, which does a breadth-first search through backward deduction axioms in order to prove the clause. There is a call to test at each tip of the search tree. Multiple-oc-curre~­ ces of a sub-question are recognized.

recsearc.'l1, which is like search except that the search 1s depth-first, and II!Ultiple occurrences of sub-questions are not recognized.

ask, which calls search with its argument and Wrth its negated argurrent, and then answers YES, NO, or DON'T-KNOW as described by Palme (1971).

The function test is similar to store, and bet:-. search and reese arch are similar to assert. There are funct1ons syssearch, sysrecsearch, etc. and relations have function definitions on their property-lists under the indicators TESTDEF, SEARCHDEF, etc. For example , svsrecsearch is in principle defined as

(LAMBDA (COND (N GUC) ((TEST QJC) ( (ZEROP N) (T (APPLY T) NIL) (GIT (CAR GUC) 'RECSEARCHDEF) (CONS N (CDR GUC] Moreover, the RECSEARCHDEF property of a binary relation has the form (LAMBDA (!';~ X Y) (OR (PROG [COI'.'D ) ) ( ( SYSRECSEAROi C SUBl mO (sub-question)) ( RE'I'UR"l T ] )

Each argu.r:-ent c:c OR is a compiled axiom, and each compiled axiom calls sysrecsearc.'l once for eac:. sub- question it generates.

SEARCHDEF properties (which are used by syssearch for breadth-first search) are similar t o RECSEARCH0EF's, but instead of calling sysrecsearch , they store the sub-question on a FIFO subquestion queue whic.~ the function syssearch ma.il'1tai.'1S as the value of a ~ var~able , which then is free in t he SEARQIDEF.

Co~ilation of rules

The compilation process sta~s with a rule (i.e. a non-ground, a~d usually non-unit clause), and ends when t:.is rule has been transformed to LISP code and i.'"lserted i.'1 a~ ASSERTDEF, SEARO'.D::F, and/or R::CSt"...ARCHDEF property. Compi­ lation is done in several passes. Let us illustrate "· >lith a concrete example, narrely the axiom

R[x ,y ] II P[y ] II S[y,z] -=:> Q[z,x]

Let us assu;re , furthenrore, that this rule is to be used for forward ded·J.ction, so that when P. [x,y ] is asserted , and P[ y] has previously been asserted, then for all z such that S[y,z] has been ~sserted, Q[z,x] is to be asserted. The treat~nt of rules for backward deduction is analogous.

Pass I: External to i.'"ltemal notation. This st:ep trans forr,.s infixes (such as II , or inf i.x relations) to prefix form. It also makes a list of the variables , and class:fi.es the literals as ~~ ant:eceder.t, a list of conditions, and a consec·J.e::: . :-he result is

((X Y Z)

(!<. X Y)

variables antecedent

((P Y) (S Y Z))

(Q Z X))

conditions

consequent

In this example, R(x,y) is selected as the antecedent, since it is to be the triggering literal (i.e. the compiled axiom is to be on the ASSERI'DEF property of R). In general one may want to have several versions of the same axiom, with different choice of an antecedent.

Pass 2: Convert to FROG-expression. This pass generates a very inefficient but yet executable prog-expression, and can be considered as the compilation proper. In our example it will generate the expression

(R (N X Y) CPROG (Z ZQUE) El (BINDNIL 'CPY) '82 'EN~2 ) Ml (CONT NIL '(P Y) 'END) 82 (BIND '(Z) '(S Y Z) 'B3 'Ml 2) M2 (CONT '(Z) '(S Y Z) 'Ml) 83 ((LAMBDA 000 (SYSASSERT N (CLOSE XK))) '(Q Z X)) (GO M2) END ( RE'I'UR"l) ) )

Thus the antecedent determines the contents of the first line (intended as lambda-variables etc.); each condition generat:es a bind-oor.t pair, a~d the consequent is used as-an argument to the l~bda-expression. The functions in this orog a~ defined as follows:

!)iJ"ld [varlist literal OCI'Itlabel back'J. label, uepth . " varhst ~s lHL , then bnd does a recsearch on the literal with the ~dicated deoth. If the value ~s T (i.e. if the condition isVerified), then bind does a g?to the contla...hel, where the next condi tl.CI'l is tested, ot'lerw~se it does a goto the backuplabel, i.e. the ~-statement of the previous condition.

If the varlist is non-NIL, then bi.'"ld binds (using the LISP function set) the-variables on the varlist . In general, the varlist contains all var::.ab l es which occur in 1::. teral, and which have not occurred in the ar.tecedent or in any previous literal. In position 92 above, bir.d will assign t o ZQUE the list of all z wh~ch satisfy S(y ,z) for the given y , and to Z the first elenent of ZQUI. Moreover, bi.'"ld will go to contlabel if the val ue of zgue is-noTI-NIL (i.e. sor1e z has been found)) , and to backuplabel otherwise.

cont [ varlist , literal, bac.\-uplabel]. This func­ t ion has the primary purpose of doing (in the above exa.rnple)

Z : = car[zque] ZQ~~ := cdr[zque]

When zque has been exhausted, ~ goes to backuplabel (where an "earlier" variable will be cont-ed), othen.;ise it leaves control to the next statement in the ~ (where the next condition is bind-ed, or the consequent of the clause is processed). tbreover, if the varlist is empty, the corresponding bind only served as a test, and then cont should trivially go to backuplabel. --

'!he reason cont is given literal as an argu­ ment is that m cases like

(CONT '(Y) '(RXY) 'M6)

if R has been declared to be functional in the second argument, it is obvious that there is nothing to continue with. Then cont can again trivially go to backuplabel. --

close[form). '!his function is defined as oons[car[form),evlis[cdr[form)JJ

In the exa~le, it is used to pick up the current values of x and z. - It should also be remarked that the variable n is used to control the number of new nodes that are introduced. N is decrementeclwhen we have fon.;ard axiOOlS like

P(x,y) :::> R(x,f(y)

where y is a function from the predicate­ calculus viewpoint.

Pass 3: Partial evaluation. This is an equiva­ lence transformation which transforms the ~­ expression into another expression, which has the same value and the same side-effects for all arguments, but which runs more efficiently. Partial evaluation is possible since all argu­ ments to bind and oont have been given explicit­ ly. For example, t~unction ~is defined as

cant [ vl ,e ,m) = if null[vl) then goto[m) elseif null[cdr[vl)) then --rrr . . . . . then gotolrril else prog2T"Set[car[vl) ,car[eval[que[car [vl)])]) set[que[car[vl)),odr[eval [que[car[vl])]]]]

else

where ~ is a packing and rnerroizing function defined.so that

que[Z] = ZQUE

In partial evaluation, the definitions of cont, ~. etc. are inserted in the ~-express10i1; Iaiiii::x:la-expressions are expanded, and function expressions are collapsed whenever possible, e.g. so that

(CAR (CONS X y)) ... X (EVAL (QUOI'E X)) ... X (GOTO (QUOTE 1)) ... (GO 1) (SIT (QUOI'E x) y) ... (SITQ x y)

With such simplifications, the expression in position B2 above is reduced to

B2 ( COND ( (NUll.. ZQUE) (GO M1) ) (T (SITQ Z (CAR ZQUE)) ( SETQ ZQUE (CDR ZQUI]

which is quite reasonable code.

Pass 4: Frog-reduction. Partial evaluation will leave a lot of redundant E£ statements in the ~·e.g. like

(GO L)

L (GO M)

In this pass, the obvious simplifications are made.

In a fifth step, the ~-expression is inserted into the relevant ASSERTDEF or other ·.. DI:F properties.

It should be noticed that pass 2 and step 5 a..r.e the only steps that are logically needed. Pass 1 only provides some added notational convenience, and is dispensable. Passes 3 and 4 serve to speed up the program, but they are not necessary. For testing p1.l!'poses, it is sometimes better not to use them.

Predicate-calculus functions

Operators which are functions from the predicate calculus viewpoint (these must be carefully distinguished from functions in the USP systerr. , which in a certain sense interprets the predi­ cate calculus expressions) , are handled in the following fashion:

Every PC function is assigned a LISP function definition, which follows a standard pattern. If g is an n-ary PC function, then it is also an n-ary LISP function which returns an expression of the form

(GB G A B)

where GB is a ~atom, a'ld A and B are the evaluated arguments to g. This expression is called an H-e:aression. (H stands for Herbrand). It is generate the first time g[A,B] is evalua­ ted, and the same (with ~) expression is ob­ tained on each successive evaluation of g[A,B).

The atom GB carries a property-list, on which relations can be stored. Moreover, the proper­ ty-list of the first argument (in this case, A) , contains a pointer to the above expression under a certain indicator. Notice that A need not be an atom, but it may itself have been generated by a PC function.

When functions appear in axicrns, then linear code fo!' <:he :natc.'ling ("unification") is generated at comoile time. For a trivial ~xample, if the axiom

. P[g[x,y)) :::> Q[y,x]

is decl~~d for forward usage , then it is re­ v-ritten in an early COqJilation seep as

P[z] A GG[z,x,y] =:> Q[y,x]

._,her-e ~ is considered as a relation whic.l-t has a pecul::..ar r:Dde of storage , but whic!"l is other­ wise si::>.ilar i.'"l all respects to user-decla.~d relatio~s. If ~'le user decla.res ~ as a PC function, the;. "the necessary declaration of ::::;::: is irr.olicit . - ::otice that this axiom would ;;t be ~-written if it were decla.red for bac.~,.a..~:J '..lsage. ~us neH H-e:>Qressions ::13-Y be ~'"lt!'Oduced duri.'"lg deduction .

C~x:::oarisons with sorre existi>;g orograrns

Several exis::ir.g programs show si::-.ilari ties '.vi t:'l PC::J3 ~ '1 sc::-e r-es;:Jects. 'tie s:-,aE attempt a compariso:-:, e·;e:~ if there is an ob·;ious risk t:-.at we a..~ :cisir.:o~d abo·.n: sor:te aspect of the o<:he!' p!'Cgr~s. ~e !'eader should take the :Jisc"Jssio:~ he!'€ as a first a?proxir."lation.

Q~J anc. 3~·!. : (see . Green , 19 ~ g ? and ~arvey and ~. -~ : :;) . ·~f..3 c..s a resol:..l"".:J..on-o!'l.ented theore~-p!'CV~ '16 p!""OgraJT, , wr.ic. r..ai:"."tains a "::er..cry" ( se-: o: clauses tr.at a..re stored in the syste~) a:-.d a "clauselist" (set of clauses that a..~ active during a ded·..lction) . Clauses in .'!le:!"Ory a..~ ~-.dexed by predica-:e letter and the:~ :Cy ::.en~h; clauses on -:he cla'..lselist by lengc!l o:-:ly . :1o!'€over, there a..re special heuristics fo!' handling e.g. sequences of reso­ b"tion:= ·.·lit:-. :::na..ry clauses ("cr.ai.'"lbg"). QA3 . 5 is si::-.i:..x- b all of these respects . The major diffe!"'er.ces te"':',.;een QA3 and ?':)~ are:

1. QA3 i.'"lte~:--e<:s all "rules"; ?C:::JB compiles the~ ..

2. Qf-.3 can ;:Jerform resolutio:-: proofs according to artitra..rv strategies. The proofs perfonred by the PC::l5 search executive a'"ld t'"le compiled axioms corresYJr.d to so::e r.ig:-.::.:; r-estrkted resclutio:. s"".:Yategies.

not store ground tmit clauses ("facts") in a special way as PCDB does. (it is possible to interface QA3 with a program for such storage, for example by using the predicate evaluation feature. However, it seems to be a non-trivial task to make this work fully automatically, and to implement it for clauses where the rela­ tion's arguments have been constructed with PC functions).

The difference indicated in point 2 implies that QA3 is more general-purpose than PCDE is, and that it is more sui table for tasks where a major part of the clauses as non-ground and non-u.'"li t. On the other hand, points 1 and 3 enable us to guess that PCDB should be much faster in those cases where it is applicable, al thoug.'1 no cornparati ve rreas\.1l""eli\el1ts are yet available.

The NT!-! !ie·.1ris"':: ics Lal::orat:)ry orogra'!l (see ~Jorton , 1971, and Dixon, 1971). This program is sJ.r.ular in approach to QA3. In sorre experi.ne:-.<:s , che NIP. p!'Cgrarn has been guided by heuristic searc.'-1, but this does not affect the comparison ·.~it:. PD3 . 'ihe :.:rn group have compiled axioctS usi.'"lg partial evaluation, and did so a year before ~s. However, their compilation (at least as described in the paper by Dixon) seems to be :!"Ore restricted. It is perforrred so that

!"'esolve[c,c'] = (compile[c]) [c']

1-:he!"'eas the execution of one compiled rule b PCG3 r..ay be equivalent to a la_~e number of resolutions.

P:~~'"ler (see Hewitt, 1970). Li.~e PCDB and unli.~e ':he p!"'eceedbg prograr:'s, Pla-Jler is a substrate for special- purpose theore~-provers, rather than a general-purpose theorem-prover. Planner is also nore data- base- o!'ier.ted than the preceedir.g prcgra'!ls. For example, Planner uses the idea of associating procedures with relation symbols, and to exec·..Jte these for sc:orage and/or retrie­ val . The dichotomv between fo:rN'ard and backward ded"Jction is present in Pla'"lner, where one speaks about "consequent" and "antecedent" t;-,eorercs, respectively.

~e ~.ajor difference is that Planner uses a general high-level control r.echanism, which is si~i~ar in approach t o no~-jeterrninistic prcg­ rar.r..i.;·\g . This control mechanism is available to the user cf Planner; t he ~se!' of PCDB does not '"lave ic: (except trivially when he can utilize the system's search executive for backward pYDOf in some rol.ll!d-about >:ay). The control r.e::hanism is also used inside Planner . The occu..YTences of this correspond e.g. to the b!"'eadtr.-:irst search t;-.at is ;:Jerforrred by the L:nc-:ior. ':''!ssearch in PCJ~, ~o:d to the l ocps that are generated by bind and cant in compiled axioms. This differenceiS correlated with another:

Planner thinks about its user as a progranmer, and about its "theorems" as programs, albeit in a very machine-rel!Ote p~arrming language which assumes the above-mentioned control structure. PCDB thinks about its input as sta­ tic information ("declarations", "facts", "rules"), plus sorre tags which hint when and where this static information is to be used; and PCDB takes as its task to "digE;!st" its in­ put so that it can later be used in the indi­ cated situations. (This attitude of PCDB can be overcome, e.g. using the function do that was described above, but it is still significant). As a cc:nsequence of this, PCDB assumes predicate calculus notation as input, whereas Planner assumes its own input language. (It is an interesting problem to write a translator from predicate-calculus-plus-control-tags to the Planner language) . Thus PCDB is in several respects slighcl y closer to conventional theorem-proving programs than Planner is.

Present status and -elanned extensions of PCDB. Most features described in t hi s paper are presently working (May 20, 1971). The excep­ tions are: (a) pass I of compilation (infix t o prefix notation); (b) pass IV of compilation (prog-reduct i on) and the function collapsing step in pass III (partial evaluation); (c) function-to-relation conversion in canpiling rules with PC functions in the:r. . The i.rrvnediate plans are t o complete these steps ; to add a package for answering open questions (exists in outline); and to compare t he efficiency of PCDB-generated code with ma~ually produced code.

Acknowledgements

Many thanks to Lennart Drugge , Anders Haraldson , Rene Reboh and Arne Tengvald , who helped great­ ly with testing and debugging various parts of the PCDB program. Thanks also to David Luckharr:, who patiently explained some of t he intricacies of resolutionology, and to members of the SR. I A.I. group for the opportunity to discuss and to play with the QA3. 5 prograr:1 .