A Logic Programming and Verification System for Recursive Quantificational Logic

A Logic Programming and Verification System for Recursive Quantificational Logic

Frank M. Brown

Dept. of Computer Science The University of Kansas Lawrence, Kansas 66045

ABSTRACT

In this paper, we describe a logic programming and program verification system which is based on quantifier elimination techniques and axiomatization rather than on more common method of doing logic programming using the Herbrand-Prawitz-Robinson unification algorithm without occur-check.

This system is shown to have interesting properties for logic programming and includes a number of advanced fea­ tures. Among these features are user-defined data objects, user-defined recursive relations and functions, either of which may involve quantifiers in the body of their definitions, and automatic termination and consistency checking for recursively defined concept. In addition, it has a correct implementation of negation in cantrast to PROLOG implementation of nega­ tion as failure, a smooth interaction between LISP-like func­ tions and PROLOG-like relations, and a smooth interaction between specifications and programs. Finally, it provides a method of mathematical induction applicable to recursive definitions involving quantifiers.

I. INTRODUCTION

Quantified Computational Logic(QCL) is a programming and program verification language for programs written in recursive quantificational logic. The language can be used both for logic programming and program specification.

A QCL program consists of sequences of recursively defined data objects declarations and recursive quantificational logic function definitions. Programs written in QCL are both ex­ ecuted and verified by a single automatic deduction system called the symbolic evaluator using a system of axioms and rules called the symmetric logic. The essence of the symmetric logic technique is to push quantifiers to the lowest scope pos­ sible in the hope of finding a way to eliminate them. The symbolic evaluator and the symmetric logic are described in detail[Brown 83] .

A prototype system for QCL has been implemented in ln­ terlisp.

II. QCL PROGRAMMING

A. Recursively Defined Data Objects

Although many logic programming languages provide system-defined data objects, they provide only a poor capability for user-defined data objects. QCL adopts the shell principle[Boyer&Moore 79] as a method to recursively define some useful user-defined data objects. Since the shell principle was invented, not much attention has been paid to it in logic programming. However, it is very valuable in modelling logic programs and verifying logic programs. Although many of the axioms produced by the shell principle of QCL are similar to those described in[Boyer&Moore 79], some are quite different in order to satisfy the fundamental deduction principle described in[Brown 83]. This principle requires that almost all steps in the automatic deduction should take place by a

Peiya Liu

Dept. of Computer Seiences The University of Texas Austin, Tx 78713

method of replacing expressions by an equivalent but simpler expressions.

The syntax of user-defined data object is: (SHELLCREATE constructor bottom recogniser selec­ tors types defaults). The constructor is a name of new function which constructs objects of the new types. The bot­ tarn is the bottom object or T if there is no bottom object. The recognizer is a name of new function which recognizes ob­ jects of the new type. The selectors are a Iist of functions which are accessors of the data structure. The types are a Iist of type restrictions on each shell. Each restriction is an ar­ bitrary formula in QCL consisting of symbols defined at that time. The defaults are a Iist of the default values for each shell. Data objects are easily declared. For examples, Lists are produced by the declaration (SHELLCREATE 'CONS 'T 'LISTP '(CAR CDR) '(T T) '(NIL NIL)) and Trees are produced by the declaration (SHELLCREATE 'TREE 'BTM 'TREEP '(LEFT ROOT RIGHT) '(T T T) '(0 0 0)).

B. A Safe Definition Principle

Most existing logic programming languages have syntax checking but few perform logic cheeking for properties such as termination and eonsiatency. Suppose P is a logic program and R is a goal we wish to solve. Then, executing P to solve R is the same as deducing R from P in logic program execution. Therefore, any answer will be correct if the logic program P consists of inconsistent logic statements. But the user might get one of the answers because of deduction strategy. Thus user forces his program to produce some answer. QCL on the other hand has logic protection capability to detect inconsistent or non-terminating statements in logic programs. In addition, it stores vital verification in­ formation during the checking.

S is a term if it is a variable, a sequence of a function symbol of n arguments followed by n terms, or a sequence of a universal quantifier ALL or existential quantifier EX of m+l arguments followed by a variable and m terms. A variable is free in the term if at least an occurrence of it is not within the scope of a quantifier employing the variable. Note that our definition of term is not standard in classical first order logic. QCL intends to blur the distinction between the predicates and functions. And a term t governs an occurrence of term s if either there is a subterm (IF t p q) and the occurrence of s is in p, or (IF t' p q) and the occurrence of s in q, where t is (NOT t'). (ALL __ LIST (x 1 .. . x 0 ) p) is an abbreviation for (ALL x 1 (ALL x 2 ( ... (ALL x 0 p)))), (EX __ LIST(x 1 ... x 0 ) p) for (EX x 1 (EX xi ... (EX x 0 p)))) and (ALL __ ID\ (x 1 ... x 0 ) p) for a specific n mixed quantifiers over p, its negated form (EX __ ALL;(x 1 .. . x 0 )(NOT p)).

Formally speaking, a safe definition principle is: (DEFLQ (EQUAL(f x 1 ··· xn) body)), where

• (A) f is a new function symbol of n arguments.

• (B) x 1 , ··· , X 0 are distinct variables.
• (C) body is a term and only mentions free variable symbols in x 1 ... x 0 ·
• (D) There is a well-founded relation r and a measure function m of n arguments.
• (E) For each occurrence of a subterm of the form (f y 1 .. . y 0 ) in the body, the governing terms t 1 . . . tk and the governing variables which are the free variables z 1 ... zi in the governing terms and (f y 1 ... y 0 ) but not in x 1 ··· X 0 , it is a theorem that

The definition principle is shown by proving that the axiom constitutes a recursive definition of some concept. An axiom of the form:(f x 1 ... x 0 )=body can be shown to be recursive if according to some measure M the complexity of the ar­ guments of any occurrence of f in the body, assuming the hypotheses governing f in the body, is less than the complexity of x 1 ... x 0 ·

Some examples: (DEFLQ (EQUAL(AND X Y) (IF X y NIL))) (DEFLQ (EQUAL(NOT X) (IF X NIL T))

NIL is considered as false and T denotes true. The function IF is a primitive operator. Informally speaking, if X is NIL, then (IF X Y Z) is equal to Z. and if X is not NIL, then (IF X Y Z) is equal to Y.

(DEFLQ (EQUAL(ADJ X Y) (IF(LISTP X) (IF(ADJW(CAR X)) (EQUAL Y(CDR X)) NIL) NIL))) (DEFLQ (EQUAL(ADJDL X Z) (IF(EQUAL X Z) T (EX Y(IF(ADJ X Y) (ADJDL Y Z) NIL)))))

The (ADJDL X Z) says that two things X and Y make an ad­ jective difference Iist if two things are identical or there is an adjective (ADJ X Y) followed by an adjective difference Iist (ADJDL Y Z). The defining equation for ADJDL is added to our theory by the following instantiation of definition prin­ ciple: f is the function symbol ADJDL; n is 2; x 1 is X and x 2 is Z; body is the term (IF(EQUAL X Z) T(EX Y(IF(ADJ X Y)(ADJDL Y Z) NIL))); r is PLESSP; m is the function symbol LENGTHl, where (LENGTHl X Y) is defined to be (LENGTH X); governing terms are (NOT(EQUAL X Z)) and (ADJ X Y); a governing variable is Y. One theorem required by (E) is: (ALL X(ALL Z(ALL Y(IMPLIES(AND(NOT(EQUAL X Z))(ADJ X Y)) (PLESSP(LENGTHl Y Z)(LENGTHl X Z))))))). The above theorem can be proved from definitions ADJ and LENGTHl.

(DEFLQ (EQUAL(DIFFL X Z A) (IF(EQUAL X Z) (EQUAL A NIL)

(IF(LISTP X) (EX B(IF (EQUAL A(CONS(CAR X) B)) (DIFFL (CDR X) Z B) NIL)) NIL)))

(DIFFL X Z A) follows the recursive definition principle be­ cause (ALL X(ALL Z(ALL A(ALL B(IMPLIES (AND(NOT(EQUAL X Z))(LISTP X)) (PLESSP(LENGTH2 (CDR X) Z B)(LENGTH2 X Z A))))))) is .a theorem. (LENGTH2 X Y Z) is defined to be (LENGTH X).

(DEFLQ (DEFLQ (EQUAL(ADJL A) (EQUAL(ADJDIFFL X Z) (IF(LISTP A) . (EX A(IF(DIFFL X Z A) (IF(ADJW(CAR A)) (ADJL A) (ADJL(CDR A)) NIL)))) NIL) (EQUAL A NIL))))

(ADJL A) is recursive because (ALL A(IMPLIES(LISTP A)(PLESSP(LENGTH (CDR A))(LENGTH A)) is a theorem.

The principle of definition for this advanced programming language extends previous research[Boyer&Moore 79] in the following ways: The first way is that existential and universal quantifiers are allowed in the body of the defining equation. The second way is that the measured arguments of the recur­ sive calls of a function are not necessarily some function of the formal parameters, but may simply be related to them by an arbitrary relation. For example, ADJDL is recursive because the ADJ relation makes Y smaller than X. In this case there is no obvious selector function car or cdr which, when applied to (ADJDL X Z), results in (ADJDL Y Z).

Theorem D There is a unique total function satisfying the recursive defining equation (f x 1 ... x 0 )=body.

Proot: The details are shown in [Brown&Liu 84].

Thus, system guarantees consistency and termination for each new defined function.

C. Relationship to Horn Clauses

In Prolog and some other logic programming languages, Horn clauses are the main type of logic statements. Based on the closed world assumption[Reiter 78], QCL can easily trans­ late these clauses into the quantified IF -form formulas. Thus Horn clauses are essentially a subset of QCL. For example, the following Horn clause style definition of ADJL is automati­ cally translated to the above definition of ADJL.

(ADJL NIL) <- (ADJL (CONS Al A)) <- (ADJW Al)(ADJL A) .

II. FEATURES OF QCL PROGRAMMING SYSTEM

A. Combining Programming with Veriflcation System

QCL mixes programming and verification system in the natural manner. The output form of the command (PV r), which might eompute or prove relations and functions, should be equivalent to the original expression. The meaning of (PV r)=output__form is (ALL_LIST (x 1 ... x 0 ) r=output__form) if r has n free variables. Otherwise, r= output_form.

The command (PV r) asks the system to generate any n­ tuples satisfying the relationship r , where r contains n free variables. The command (PV r) may also be used to ask system to make deduction from the relation in the case that r has no free variables. The command simply tries to prove r. Usually, the output form is true, false, its equivalent but simplified form or a conjunctive form of some equalities and inequalities about remaining arguments and their binding values.

The deduction techniques of PV are based on the fun­ damental deduction principle, which makes it possible that QCL logic programming interpreter is the same as its verifica­ tion system interpreter.

B. Explanation Gapability

lt is worthwhile embedding an explanation capability inside an automated reasoning system. Currently, the system can produce all tracing information whenever a rule, axiom, or definition is applied. This information consists of three parts: an input expression I which is being evaluated, an intermediate expression M and a name of rule which produces M from I, an output expression 0 obtained by recursively evaluating the M expressions. Thus a trace will generally be of the form:

ll:exp by use of: a name of rule, axiom or definition. M1:exp 12:exp by use of: ... M2:exp 02:exp 01:exp

where the nurober immediately following I, M, or 0 is the Ievel at which the application of an rule, axiom, or definition takes place. At a given Ievel nurober i, Oi and Mi are always associated with the preceding Ii.

The debugging principle is this: if Ii does not equal to Mi, then the definition, axiom or rule used in that application is incorrect. if Mi does not equal Oi then one must recursively examine the i+1 level(ie. Ii+l' Mi+l' Oi+l) to find the error.

C. Negation Is Not A Failure

The negation-as-failure rule is an operational connection between negative and positive terms. The soundness and com­ pleteness of a restricted form has been shown in [Clark 78][ Jaffar 83]. There are still some fundamental limitations on that rule if there is no logieal eonneetion between them.

The following program uses negation-as-failure to define a term (NDIFFL X Y Z), which is supposed to be equivalent to (NOT(DIFFL X Y Z)). The cut symbol · /" makes a commit­ ment for all subgoals since the parent goal . Hence any attempt to resatisfy any previous subgoal will fail. NIL is a predicate defined in such a way that as a goal it always fails and causes backtracking to take place. But when NIL is encountered after cut, the normal backtrackins behavior will be altered by the cut and will cause the effect that whenever (DIFFL X Y Z) is successful, (NDIFFL X Y Z) is failed.

(DIFFL X X NIL)<- (DIFFL(CONS X1 X)Z(CONS X1 A))<-(DIFFL X Z A) (NDIFFL X Y Z) <-(DIFFL X Y Z)/NIL (NDIFFL X Y Z)<-

A correct answer can be deduced by failing with NIL or rather false on the query (NDIFFL '(LARGE MANY) '(MANY) '(LARGE))). But it also returns a failure on the following question which is true for any Z not equal to MANY: (NDIFFL

'(LARGE MANY) Z '(LARGE)). This relation involves a vari­ able Z in the NDIFFL. In general, the rule is not complete and has to restriet its queries and either deduction strategy or program Statements in order to work[Clark 78] . The negative query is often restricted to the ground term. Thus, much nega­ tive information simply can't be queried.

Even worse, it should be noted that the above set of clauses are inconsistent if (NDIFFL X Y Z) really is (NOT(DIFFL X Y Z)). QCL takes a logically correct approach towards handling negative information. Any negative term (NOT tm) is defined as the term (IF tm NIL T) by system. If DIFFL is defined as before, (PV (NOT(DIFFL'(LARGE MANY) Z '(LARGE))) will result (IF (EQUAL Z '(MANY)) NIL T). This means that answer is any Z which is not equal to '(MANY). The details of computing this relation are given as follows:

Example A:

(PV (NOT(DIFFL '{LARGE MANY) Z '(LARGE)))) The expression to be recursively simplified is: (NOT (DIFFL (QUOTE (LARGE MANY)) z (QUOTE (LARGE)))) ll:(DIFFL (QUOTE (LARGE MANY)) z (QUOTE (LARGE))) by use of: DIFFL M1:(IF (EQUAL (QUOTE (LARGE MANY)) Z) (EQUAL (QUOTE (LARGE)) NIL) (IF (LISTP (QUOTE (LARGE MANY))) (EX *1 (IF (EQUAL (QUOTE (LARGE)) NIL)) (CONS (CAR (QUOTE (LARGE MANY))) *1)) (DIFFL (CDR (QUOTE (LARGE MANY))) z *1) NIL)) 12:(DIFFL (QUOTE (MANY)) Z NIL) by use of: DIFFL M2:(IF (EQUAL (QUOTE (MANY)) Z) (EQUAL NIL NIL) (IF (LISTP (QUOTE (MANY))) (EX *2 (IF (EQUAL NIL NIL)) (CONS (CAR (QUOTE (MANY))) *2)) (DIFFL (CDR (QUOTE (MANY))) z *2) NIL)) 02:(EQUAL (QUOTE (MANY)) Z) 01:(EQUAL (QUOTE (MANY)) Z) The result of recursive simplification is: (IF (EQUAL (QUOTE (MANY)) Z) NIL T) end of deduction Input 12 is due to variable *1 in M1 being replaced by NIL under the if-condition (EQUAL '(LARGE)(CONS(CAR '(LARGE MANY)) *1)).

Example B: (PV (DIFFL '(LARGE MANY} Z '(LARGE))} The expression to be recursively simplified is: (DIFFL (QUOTE (LARGE MANY)) z (QUOTE (LARGE))) 11 :(DIFFL (QUOTE (LARGE MANY)) z (QUOTE (LARGE))) by use of: DIFFL M1 :(IF (EQUAL (QUOTE (LARGE MANY)) Z) (EQUAL (QUOTE (LARGE)) Nll..) (IF (LISTP (QUOTE (LARGE MANY))) (EX *1 (IF (EQUAL (QUOTE (LARGE)) Nll..)) (CONS (CAR (QUOTE (LARGE MANY))) *1)) (DIFFL (CDR (QUOTE (LARGE MANY))) z *1) Nll..)) 12:(DIFFL (QUOTE (MANY)) Z NIL) by use of: DIFFL M2:(IF (EQUAL (QUOTE (MANY)) Z) (EQUAL Nll.. Nll..) (IF (LISTP (QUOTE (MANY))) (EX *2 (IF (EQUAL Nll.. Nll..)) (CONS (CAR (QUOTE (MANY))) *2)) (DIFFL (CDR (QUOTE (MANY))) z *2) Nll..)) 02:(EQUAL (QUOTE (MANY)) Z) 01 :(EQUAL (QUOTE (MANY)) Z)

The result of recursive simplification is: (EQUAL (QUOTE (MANY)) . Z) end of deduction

D. Relational vs. Funetional

There are currently two really good ways of programming based on formal logic, namely: (1) programs based on recur­ sive functions, such as the LISP. (2) programs based on NON­ NEGATIVE recursive relations, such as HCPRVR and PROLOG.

QCL takes a different approach from LOGLISP[Robinson 82], QUTE[Sato 83] and TABLOG[Malachi 84]towards com­ bining the5e two formalisms . Our concern focuses on the unique formalism and a smooth interaction between relations and functions.

Each type of programming system, of course, has many ad­ ditional features (eg. assignment statements, goto's etc.), but it is the logical features : reeursive funetions or reeursive relations which make it so easy to express, understand, and debug programs written in these systems. Some programs are rnore easily expressed, understood, and debugged as functions than relations and vice-versa. In particular cornbinations of deterministie . prograrns returning unique outputs should be written as functions. For example, to APPEND the REVERSE of a Iist A onto the result of APPENDing the REVERSE of a Iist B onto the REVERSE of a Iist C is written as functions as: (APPEND (REVERSE A) (APPEND (REVERSE B) (REVERSE C))) whereas it is rewritten as rela­ tions with many extra symbols as:

(EX Xl(EX X2(EX X3(EX X4(AND(REVERSE A X1) (REVERSE B X2) (REVERSE C X3) (APPEND X2 X3 X4) (APPEND X1 X4 ANSW))))))

X1,X2,and X3 are respectively the results of reversing A, B, and C, X4 is the result of appending X2 to X3, and the answer: ANSW is the result of appending X1 to X4. In such a case the Iack of nesting in relational notation rnakes it resemble assernhier notation (where the variables are registers and the assernhier operations are REVERSE and APPEND) rather than a high leveJ. language.

On the other hand, cornbinations of non-deterministic programs are more naturally expressed as relations. For ex­ ample, a program which parses English(and translates it into another language) is naturally made up of a number of non­ deterrninistic prograrns. The definition of a declarative tran­ sitive sentence is easily written in relational notation as:

(EX X1(EX X2(EX X3(AND(NP 11 12 X1) (VG 1213 X2) (NP 13 14 X3) (COMBINE X1 X2 X3 ANSW)))))

where 11 is the input text, 12 is the rest of the text after a noun phrase is parsed, 13 is the rest of the text of 12 after a verb group is parsed, 14 is any remaining unparsed text, Xl is the translation of the first noun phrase, X2 is the translation of the verb group, X3 is the translation of the second noun phrase, and ANSW is the translation of the entire sentence.

Such a program can not be rewritten in functional notation as: (COMBINE(NP 11 12)(VG 12 I3)(NP 13 14)) because the NP and VG relations are not deterministic on their third ar­ gurnents. For exarnple, there rnay be many different parses of the the first noun phrase each giving a different answer. Fur­ thermore, 12 is another non-deterministic output of (NP 11 12) which must be passed an input to (VG 12 13). Likewise, if in­ sisting on functional notation, an assernbly-like program can not be avoided.

These considerations also apply to advanced database tech­ nology. Data can be represented relationally as in relational databases [Codd 72] or functionally. For exarnple, a request for the salary of the president of the university of the largest state in the united states could be written as:

(EX X1(EX X2(EX X3 (AND(LARGEST_5TATE_OF(UNITED_8TATES) X1) (UNIVERSITY_OF X1 X2) (PRESIDENT_OF X2 X3) (SALARY_OF X3 ANSW)))))

However, it can be written in the simpler functional notation as: (SALARY_OF (PRESIDENT_OF (UNIVERSITY_OF (LARGEST_8TATE_OF (UNITED_8TATES))))) because each of these predicates is deterministic on its last argument. On the other hand, in an example with non-deterrninistic outputs, the relational representation is better.

Two distinct programrning systems have been developed based on fo~mal logical notation(recursive functions, recursive relations) and each is especially useful for representing a particular type of programs( deterministic and non-deterministic ). Furthermore, the more facilities of formal logic that are provided in a programming system, the less one needs to use constructs such as GOTO and assignment which are harder to use, understand and debug. Therefore, it follows that a sig­ nificantly better programming system could be achieved by amalgamating these formal notations into a single formal sys­ tem provided that effici .... interpreted and/or compiled in­ ference systems could be designed.

E. Specifieation vs. Program

In QCL, specifications and programs are considered as dif­ ferent styles to express logic expressions for their own purposes within the same framework. Specifications are deseriptively useful logic forms and their eomputationally useful forms are programs.

We believe that automatic derivation, verification and syn­ thesis of logic programs are made easier, provided that specifications and programs have a sm.toth interaction. Two important relationships between logic programs and their specifications are correctness and completeness. Correetness is a property that for any n-tuple x, if x is computed as a solu­ tion satisfying a relation R, then x belongs to the relation specified by S. It can be formalized as Vx(Sf-R(x)*=Pf-R(x)). CompleteneBS is a property that for all members of the specified relation R are computable from program P . It can be represented as Vx(Sf-R(x)=tPf-R(x)). One way to show these relationships is to use meta-level deduction to prove those formulas[Brown 78] . Another way is that, if finding a good specification S such that Sf-P or Pf-S, we get same correct­ ness proof or completeness proof by exploiting the transitivity of logical implication f-.

The second approach is the cornerstone of logic program derivation, verification and synthesis investigated in[Clark 77][Hogger 81]. One advantage in tbis approach towards verification is that the object-level deduction from S to P or from P to S is sufficient to show their relationships without meta-level deduction and concerning goal relation R(x) . Another advantage is that for proving any property of P, it may be much easier to show that S has that property and P is complete with respect to S. In the Hogger study, specifications expressed in "if-and-only-if· and ·first-order recursive· styles are crucial in this approach. Since QCL intend to bring specifications and programs together, it provides a good op­ portunity to investigate good specifications and program styles in order to automate the derivation, synthesis, and verification of logic programs. For example,

(DEFLQ (EQUAL(PICK.S U V Z) (IF(MEMBER.S U Z) (IF(MEMBER.S V Z) (PLESSP UV) NIL) NIL)) Informally stated, (PICKS U V Z)=(MEMBER.S U Z)/\ (MEMBER.S V Z)A(PLESSP U V). (DEFLQ (EQUAL(MEMBER.S U L) (EX X(EX Y(IF(EQUAL L (CONS X Y))) (IF(EQUAL U X) T (MEMBER.S U Y)) NIL))))

lnformally, (MEMBER.S U L)=3x3y(L=(CONS x y)/\ (U=xV(MEMBER.S U y))).

The specification S:{PICK.S MEMBER.S} is for the follow­ ing program P :{PICK.P MEMBER.P}. It said to pick any two numbers U and V from a Iist Z of numbers, not necessarily distinct, such that U is less than V. The relationships can be shown by object-level deduction, that is, Sf-P and Pf-S.

(DEFLQ (EQUAL(PICK.P U V Z) ) (IF(LISTP Z)) (IF(EQUAL U(CAR Z)) (IF(MEMBER.P V (CDR Z)) (PLESSP U V) NIL) (IF(EQUAL V(CAR Z)) (IF(MEMBER.P U (CDR Z)) (PLESSP UV) NIL) (PICK U V(CDDR Z)))) NIL) (DEFLQ (EQUAL(MEMBER.P XL) (IF(LISTP L) (IF(EQUAL X (CAR L)) T (MEMBER.P X (CDR L))) NIL))

IV. QCL VERIFICATION

A. A Generaliaed Noetherlan lnduetion Principle

In logic programming verification, we often need induction to rearrange the conjecture into a systematic way to prove. The induction principle we use is a generalized version of Noe­ therian induction[Burstall 69][Boyer&Moore 79]. Existential and universal quantifiers are allowed both in the base case and in the induction steps.

Formally stated, the induction principle is:

Suppose:

(A) p is a term with t's distinct free variables x 1 , ... ,xn,xn+l' ... ,xt; (B) r is a well-founded relation; (C) m is a measure function of n arguments; (D) b 1 , . .. , bk are non-negative integers; (E) For each i l:Si:Sk, \I· ... ,zi b are distinct bound · i variables; (F) ql' ... ,qk are terms; (G) h 1 , . .. ,hk are positive integers; and (H) For l:Si:Sk and l:Sj:Shi' si,j is a substitution and it is a theorem that (ALL_LIST (x 1 ... xt)(ALL_LIST(zi,l ... zi,b) I (IMPLIES ~ (r(m x 1 . . . x 0 )/si,j(m x 1 . . . x 0 ))))).

Then

is a theorem and

(II). (EX_LIST (x 1 ... xt) p) is a theorem if

for the base case, (EX __ LIST(x 1 .. . xt)

(AND(AND(NOT(ALL _ EX 1 (z 1 , 1 ... z1,b 1 )q1))

p)) is a theorem or

for some 1 < i < k induction step,

is a theorem.

We adopted a Boyer&Moore's definition here before prov­ ing soundness of this induction principle. <X1 ... Xn> is RM-smaller than <Y1 .. . Yn> if there is a measure function M and a well-founded relation R such that (R (M X1 ... Xn)(M Yl ... Yn)) .

Theorem I. Soundness for Universal Quantifiers Case Proof:

Supposed there is a t-tuples < Xl , ... ,Xt> suchthat (P X1 .. . Xt)=NIL where (P Xl .. . Xt) stands for pjs, s is substitu­ tion { < xl, Xl > ... < xt, Xt> }. Let it be a RM-minimal such t-tuples.

... ,

where (Qi X1 ... Xt) is abbreviated for <I;/s, and s is a substitution { < xl , X1> .. . < xt, Xt> }.

Then by base case, (P X1 ... Xt)'f'NIL contradicting the as­ sumption that (P Xl ... Xt)=NIL.

Case ll. Suppose

where (Qi X1 .. . Xt) abbreviated for qJs, s is a substitution { < x1, X1> ... < xt, Xt> }.

I Since < X1, ... ,Xt> is an RM-minimal t-tuples such that (P X1 ... Xt)=NIL and condition (H), we have (ALL __ E)\(z; 1 .. . z. b) (AND(Qi Xl .. . Xt) (P d. 1 1 .... d. 1 t) ... (P d. h 1 .' .. 1, i 111 11 1 11 i ' di,b.,t)))'f'NIL, where for each 1 ~ v ~ t, the substitution si,h. 1 I replaces Xv with some d. h . But we know the ith induction 1, i'v step is a theorem. Hence, we get (P X1 ... Xt)'f'NIL, con­ tradicting the assumption that (P X1 .. . Xt)=NIL.

Q.E.D.

Theorem II. Soundness for Existential Quantifiers Case

Proof: Theorem II is only a symmetric case of Theorem I. Its validity is obvious after proving Theorem I.

Q.E.D.

An application of this induction principle is illustrated below. In the proof (PV (ALL X(ALL Z(EQUAL(ADJDL X Z)(EX A(AND(DIFFL X Z A) (ADJ A))))))), an induction is obtained by instantiation of the principle as follows: p is (EQUAL(ADJDL X Z) (EX A(AND(DIFFL X Z A){ADJL A)))); r is PLESSP; m is LENGTH; n is 2; k is 1; b 1 is 1; z 1 1 is Y; h 1 is 1; q 1 is the term (AND (NOT(EQUAL X Z))(ADJ X Y)); the theorem required by (H) is: (ALL X(ALL Z(ALL Y(IMPLIES(AND (NOT(EQUAL X Z))(ADJ X Y))(PLESSP(LENGTH1 Y Z)(LENGTH1 X Z)))))). The induc­ tion is:

Base ease: (ALL X(ALL Z(IMPLIES{OR(EQUAL X Z) (NOT (EX Y(ADJ X Y)))) (p X Z)))) lnduetion step: (ALL X(ALL Z(IMPLIES(AND(NOT(EQUAL X Z)) (EX Y{AND(ADJ X Y) (p y Z)))) (p X Z))))

B. Induction Schemes and A Proof Example

The recursive first-order function definition suggests plausible induction schemes. Thus, the induction schemes for each of these recursive functions can now be produced. Sup­ pose we try to prove two notions of adjective different Iist are equivalent, {PV {ALL X{ALL Z{EQUAL(ADJDL X Z){ADJDIFFL X Z)))).

The mechanical proof of this conjecture begins by unravel­ ing the non-recursive function ADJDIFFL and then examining the induction schemes for each recursive function.

(ALL X( ALL Z(EQUAL(ADJDL X Z) (EX A(AND(DIFFL X Z A)(ADJL A)))))) (by opening up the function ADJDIFFL)

The system examines the induction scheme for each recur­ sive function.

The scheme for (DIFFL X Z A) is: (EQUAL(ALL X(ALL Z(ALL A(p X Z A)))) (AND(ALL X(ALL Z(ALL A(IMPLIES(OR(NOT(LISTP X)) (NOT(EX B(EQUAL A(CONS(CAR X) B)))))

(p X Z A)))))

(ALL X(ALL Z(ALL A(IMPLIES(AND(LISTP X)

(EX B(AND(EQUAL A(CONS(CAR X) B)) (p (CDR X) Z B))))

(p X Z A)))))))

The scheme for (ADJDL X Z) is: (EQUAL(ALL X(ALL Z(p X Z)))

(AND(ALL X(ALL Z(IMPLIES(OR(EQUAL X Z)

(NOT(EX Y(ADJ X Y))))

(p X Z))))

(ALL X(ALL Z(IMPLIES(AND(NOT(EQUAL X Z)) (EX Y(AND(ADJ X Y)(p Y Z))) (p X Z)))))))

The induction scheme for (ADJL A) is ignored since it has a measured argument which is a bound variable. The induc­ tion scheme for (DIFFL X Z A) is subsumed by the induction scheme for (ADJDL X Z); so the ADJDL induction scheme is used. The system uses heuristics and follows the induction principle to split the original conjecture into two cases as above. The details of the mechanical proof are generated in [Brown&Liu 84] .

V. CONCLUSIONS

A new logic programming language has been developed which is based on quantifier elimination techniques and axiomatization. Unlike other logic program systems, it does not involve any unification algorithm. This system bandies a number of problems better than unification-based logic pro­ gramming system. For example, this system allows the proper axiomatization of negation, a smooth interaction between functions and relations, and an ability to write specifications and to verify the correctness of programs using a generalized Noetherian induction rule. Also, it extends previous work in program verification to the problern verifying recursively defined relations whose definition bodies contain quantifiers.

ACKNO~ED�EMENTS

The work described here has been supported in part by the Army Research Office under Grant DAAG 29-83-K-0103 and in part by the National Science Foundation under Grant DCR-8320340.

The authors would like to thank Prof. Norman Martin and Ruey-Juin Chang for their helpful comments to earlier drafts of this paper. Our thanks also go to the referees for their use­ ful suggestions. Finally, we thank Ching-Hua Chow and Chin­ Laung Lei for their tips on using text editor.