Designing Examples for Semantically Guided Hierarchical Deduction

DESIGNING EXAMPLES FOR SEMANTICALLY GUIDED HIERARCHICAL DEDUCTION

Tie Cheng Wa.ng Department of Computer Seiences The University of Texas at Austin Austin, Texas 78712

resolving ·B agairrst the first clause of S. Note that, for a semantically guided refutation proof, only the clauses that are false in the given model are treated as semanti­ cally provable, so ca.n be used as goals during deduction. Because ·A is false in M, but A V ·C is not, only the first bra.nch can be developed next. Then, from ·A, only a resolvent ·C V B is produced by resolving ·A agairrst the first clause of S. Now, because ·C VB is true in M and there is no other deduction path left, the deduction has to terminate with failure. Some previous approaches tried to avoid this source of incompleteness by changing the model during deduction [5,6]. For example, according to Example 1 of [5], a secondary model M' = { ·A, B, C} s,hould be used later to finally prove S (The set S of the above example is just a simplified version of the problern given in Example 1 of [5]). But, generally speaking, this strategy is not feasible to implement. One reason for this is that to design a "suitable" example for helping prove a hard theorem is not a easy matter. This is another problern encountered in using this method.

In fact, the design or selection of a suitable exam­ ple for a theorem to prove is a.n essential problern with using this method. Of course, this task is difficult for a computer to do automatically because domain depen­ dent knowledge is usually needed and also because it is hard to give a precise description of what is a suitable example. As for the human design, the difficulty lies in dealing with the interpretation of skolem functions (here, we are concerned with first-order logic only), because a casually-chosen interpretation of a skolem function may cause proof failure.

This paper tries to give a solution of the above prob­ lems. We will use examples to guide a resolution-based theorem prover, semantically guided hierarchical deduc­ tion prover (SHD-PROVER). Different from the usual goal-oriented deduction procedure, this procedure has a particular mecha.nism in producing and retaining all "le­ gal" resolvents producible from a goal clause in each de­ duction step. In light of this feature, many failure cases caused by using models in a traditional goal-oriented prover can be avoided. For example, this procedure will retain both resolvents ·A and A V ·C producible from the goal ·B at the first step of deduction of the above example. But the resolvent A V ·C which is true in M

ABSTRACT

Sema.ntically guided hierarchical deduction prover is a resolution-based theorem-proving procedure which is ca­ pable of using the domain dependent knowledge presented in weil designed examples. This paper gives a.n overview of the basic deduction components of the prover, inves­ tigates some rules for human design of examples, and demonstrates their usage in proving several non-trivial theorems.

I. INTRODUCTION

A method for using domain dependent knowledge in mecha.nical theorem proving is to present the hypothe­ ses of a theorem-i.e. the axiomatic system involved as a model (or say, an example*)-which is then used in guiding a mecha.nical prover to search a proof along with semantically provable paths. This method has been inves­ tigated by several researchers[2,3,5,6], where it was used mainly in some natural deduction proving procedures.

Though the basic idea of this method is simple and plausible, its potential usage has been limited by some problems or difficulties exposed in earlier implementa­ tions.

One problern is that this method often produces in­ completeness for the traditional goal-oriented theorem provers, such as a linear resolution procedure or some natural deduction procedures. For example, consider a unsatisfiable set S of ground clauses, S = { A V ·C V B, ·A VB, C, ·B}. Suppose the first three clauses of S are hypotheses. We use M = { A, B, C} as a model of these hypotheses to guide a linear resolution proof (refu­ tation) of S. Let the last clause ·B of S be the the first goal. The first step of deduction has two different branches: one produces a resolvent ·A by resolving ·B agairrst ·A VB, another produces aresolvent A V ·C by will be allowed to be used only as rule clause. Then a re­ solvent ·C can be produced in the next step by resolving ·A against this new rule. Because ·C is false in M, it can be used as next goal to finally deduce a refutation of s.

This work was supported in part by NSF gra.nt MCS8313499.

* In this paper, the word "example" means a model that contains real semantics.

The SHD-PROVER is based on a complete deductive component, hierarchical deduction procedure. The effi­ ciency of this procedure is enhanced by several complete­ ness-preserving refinements. The procedure can prove au­ tomatically a series of non-trivial theorems without the help of examples (see [8]). So, our approach emphasizes also the importance of a compact deductive component.

This paper mainly describes our method of design­ ing and using examples for SHD-PROVER. we will inves­ tigate some rules for the human design of examples, es­ pecially, for the interpretation of skolem functions. More considerations about completeness and effectiveness prob­ lems will be included in these rules. As an application, this method will be used in designing examples to help our prover prove several non-trivial theorems, AM8, IMV, GCD, LCM and Schubert's statement. In order to in­ clude type information and other useful knowledge into examples, a three valued modeling and the corresponding interpretation method will be proposed.

The paper concludes with a summary of the results of computer runs in proving the example theorems.

II. OUTLINE OF THE HIERARCHICAL DEDUCTION

(See [8] for details. Those familiar with [8] should proceed to next section.)

The hierarchical deduction procedure proves a theo­ rem by traversing a tree of nodes. Each node contains a different set of clauses and other information. All candi­ date goal clauses are contained in a goal-list. Each Iitera! of each goal clause is indexed by a node name, through which a set of nodes can be located to obtain rule clauses for the resolution upon that Iitera!.

At the beginning of a deduction, there is only one node (node 1) which contains all input clauses, while the goal-list contains only the input goal clauses. The literals of the input goal clauses are all indexed by 1, which cor­ responds to the name of the first node. The general proof process is as follows:

1. The first goal clause G of the goal-list is taken. Along with the index of the left-most Iitera! of G, a set of rule clauses is obtained by retrieving the node indi­ cated by this index and all parent nodes of this node. This index will be the parent name of the new node being produced in this round of deduction.
2. All "legal" resolvents are produced by resolving the goal clause against each clause of the set of rules upon the left-most Iitera! of the goal clause. For each of the resolvents produced, the indices and the order of

the literals inherited from the goal clause are re­ tained, but the indices of the literals inherited from the rule clause are replaced by a !arger integer which is just the name of a node being produced; these lit­ erals are placed to the left in the resolvent.

1. If D (the empty clause) is obtained, then the pro­ cedure returns "proved". Otherwise, the resolvents will be stored into the new node and also be inserted into the goal-list according to their priorities. Then the above process is repeated.

The "legal" resolvents produced by the prover are called H-resolvents (hierarchical resolvents). They are produced under a number of constraints which will be briefly described next.

Local Subsumption Test: The literals previously re­ solved upon are retained by the resolvent as "framed" literals. A resolvent is said to be locally subsumed if it has more than one Iitera! including its framed literals, aharing a common atom. The locally subsumed resolvent will be discarded.

Constraints on Common Tails: We call any index of a Iitera! in a clause C which is less than the index of the left-most Iitera! of C, a tai/ index of C. An index that is a tail index of two different clauses is called a common tail index of these clauses. We require that a legal resolvent of a goal clause must not be produced by resolving the goal upon the Iitera! of a rule clause whose index is a common tail index of these clauses. We require also that the common tails ( consisting of the literals with common tail indices) of the clauses being resolved be mergeable (unifiable).

Proper Reduction: An H-resolvent H is called a proper reduction of an ancestral goal clause G, iff H is a variant (including indices) of a proper part of G. Once a proper reduction is obtained, all other descendant re­ solvents produced from G (including G itself) will be dis­ carded.

Global Subsumption Test: The hierarchical deduc­ tion has a feature that the resolvents grouped in the same node are similar to each other in the sense that the tails of these resolvents all are instances of the same part of a goal clause. Based on this property, the procedure can use an effective subsumption test method, so that only a few relevant resolvents need to be compared to determine whether a new resolvent is redundant.

Resolvent Evaluation and Reordering: The prover uses a best-first search strategy by which the candidate goal clause with largest priority is to be resolved first. The priority of each resolvent is assigned by an evaluation rou­ tine based on certain ideas, such as "twin symbol". These ideas are also used by a Ievel subgoal reordering subrou­ tine, which is responsible for selecting an "important Iit­ era!" from a goal clause to be the left-most Iitera! of that clause.

A Partial Set of Support Strategy and Others: This strategy is another use method of the model methodol­ ogy (or say, set of support strategy) to reduce the search space. With this strategy, some literals of input clauses will be disallowed to resolve upon according to a model or "setting" . The prover includes a finite forward chain­ ing subroutine to produce some useful information for the evaluation routine. A special factoring algorithm, hierar­ chical factoring, is used by the procedure, which allows production of fewer factoring resolvents without causing incompleteness.

III. SEMANTICALLY GUIDED HIERARCHICAL DEDUCTION

Now, suppose M is a model of the input set of rule clauses. We require that only the resolvents that are false in M (that is, semantically refutable) can be used as goals by the hierarchical deduction procedure. Then this proce­ dure becomes a so-called semantically guided hierarchical deduction (SHD-PROVER). Note, the newly produced re­ solvents that are true in M will still be retained in some node, so they may be used later as rules.

In order to incorporate type information and other useful knowledge into a model, the interpretation method to be discussed in this paper will be slightly different from the traditional one. In particular, we will allow the do­ main D of an interpretation to include a special element, "unknown". Thus D = Do U {unknown}, where Do is an ordinary nonempty domain not containing the el­ ement "unknown". This element will be used for indi­ cating the interpreted value of semantically meaningless terms, atoms, or formulas. We restriet the use of our interpretation method to a subset of the first-order for­ mulas, namely, the simplified first order formulas.

Definition. A simplified first-order formula is a quan­ tifier free first-order formula containing no logical symbol other than ·, 1\, V; and each negation symbol· occurring in this formula must be applied to an atomic subformula (ie. atom).

All atomic formulas, clauses, and sets of clauses (treated as conjunctions of disjuncts) are simplified first­ order formulas. The formulas in the interpretation normal form, which· is to be introduced next, are also simplified first-order formulas.

Interpretation. An interpretation I for a simplified first-order formula W consists of a domain D and a defi­ nition for each non-variable symbol occurring in W, such that

• o Each n place predicate symbol P is interpreted in I as a function, P: D"-+ {true,false,unknown};
• o Each n place function symbol F is interpreted in I as a function, F : D" -+ D;
• o The logical symbols are interpreted in I traditionally, except ·unknown = unknown, unknown 1\ X= X,
• and unknown V X = unknown, where X E { true, f alse, unknown };
• o For any term or simplified first-order formula W, the term or formula W', obtained from W by substituting all variables occurring in W with some elements of D, is called an interpretation instance of W over D. Let [W']1 denote the interpreted value obtained by evaluating W' according to the interpretations of all non-variable symbols occurring in W';
• o Let C be any simplified first-order formula, then [C]r = unknown iff, for each interpretation instance C' of Cover D0 , [C']r = unknown; [C]r = false iffthere is an interpretation instance C' of Cover Do, [C']r = false; otherwise, [C]r = true.

Domain. SHD-PROVER requires that the domain D(Do) of an interpretation be finite. This finite domain is obtained by the following method. For a theorem W to be proved, we first interpret it by using a natural do­ main (it may be infinite). Then the domain D(Do) used by the prover is produced mechanically by the following procedure:

• PRDCEDURE DDMAIN_GENERATDR (domainJimit); count := 1;

D := { e : e is the interpreted value of a constant (0 place function symbol) of W };

WHILE count ~ domainJimit DD

count := count + 1;

D := D U { e : e is the interpreted value of an interpretation instance of a term in W over D };

The domainJimit can be given by the user. In prac­ tice, we prefer to use a small domainJimit first, such as 1, to generate a small size domain. H the prover fails, then repeatedly increase dominJimit and call the prover until a proof is obtained. We will give several examples of this procedure being used.

For SHD-PROVER, the resolvent that is interpreted as "unknown" will be discarded. It is noticed that the expense of obtaining the interpreted value of a literal or a term increases exponentially along with the increase of the number of different variables it contained. Wehave used a more efficient method (not given here) to implement this semantic test for avoiding the expensive evaluation.

IV. EXAMPLE DESIGN METROD

Semantically guided hierarchical deduction, by re­ taining the resolvents which are true in the modelas rules, has acquired a valuable property: if the prover is guided by a particular model, such that at most one semantically refutable and useful resolvent is produced in each step of a deduction, then the procedure will not lose a proof of a theorem. Our task in designing examples and interpreting skolem functions is to obtain this kind of model" .

According to this property and others, a model M with the following characteristics is preferable:

1. The model M should not represent a trivial case of the theorem.
2. Each rule clause should be interpreted to true in M, and the goal clause should be false in M.
3. Among a group of resolvents produced in each step of deduction, at most one ~ resolvent is false in M (A useful resolvent is one which can be used by the hierarchical deduction procedure in continuing the current path to CJ).
4. A literal or a term should be interpreted to "un­ known" for arguments that Iead to semantically meaningless situations.

The above characteristic 3 is important to reduce the possibility that a semantic guide causes proof failure (it is also important to efliciency). Let us consider a set of clauses, 81 = { Q V R, P V -,Q, P V -,R, -,p}, with ...,p as goal. Suppose we use {P, Q, -,R} as a model of the hy­ pothesis clauses, then there is a successful deduction path in which only one useful resolvent false in the model can be produced in each step of deduction. Now, suppose we use {P, Q, R} as a model, then the proofwill fail, because the two useful resolvents ...,q, ...,R produced in the first round of deduction are both false in this model.

Certainly, it is usually not easy to construct a model that ha.s such a cha.racteristic. In the following, we will investigate a way towa.rd a partial solution of this prob­ lern. Notice that the clause P V -,Q and P V ...,R in the above example can be put together to form a formula, P V [-,Q 1\ -,R]. We will call this form of a formula inter­ pretation normal form.

Definition. An interpretation normform (IPN form) is a simplified first-order formula in the following form:

where L1 ... L1c are literals and C1 ... Ch are clauses.

For consistency, a formula with a form L1 V ··. V L1c (a clause) is treated as a degenerate case of IPN form, where h = 1 and C1 = CJ (so is deleted); a formula with a form C1 1\ ... 1\ Ch is treated as another degenerate case of IPN form, where k = 1 and L1 = CJ (so is deleted).

Note that, corresponding to each IPN form, there is a set of clauses, each of which contains a subclause C; for some j, 1 $ j $ h.

Interpretation rules for a formula in IPN form: For each interpretation instance of an IPN form,

1. if [L~ V . .. V L~]r = false, then for each j, 1 $ j $ h, [Cj]r should not be false, except when C; is iden­ tical to a part of the goal clause.

* Not all theorems have such models, but most of the practical theorems seem to have, at least the only counter­ example we found is very unnatural and complicated.

1. if [L~ V ··· V L~]r = true, then there should be at most one j, 1 $ j $ h, suchthat [Cj]r = false.

As a simple application of these rules, Iet us consider again to design a model for proving the set S1 by the SHD­ PROVER. First, we combine the clauses in 81 into 3 IPN forms, {Q V R, P V [-,Q 1\ -,R], -,P}. Because ...,p will be the goal clause, P must be interpreted to true. Applying the above rule 2 to the interpretation of the IPN form P V [-,Q 1\ -,R], we notice that at most one of ...,q and -,R can be interpreted to false. Thus the model {P, ...,q, R} {P, Q, -,R} is acceptable, but the model {P, Q, R} is not.

In this paper, we will mainly consider the problern of designing examples.for theorems that have real seman­ tics. In this case, as it will be shown in what follows, the interpretation rules of IPN form will be mainly applied to interpret some skolem functions.

An examole desjgn method. Let T be a theorem of first-order theory, and S be the set of clauses obtained by skolemizing the negation ofT. We design an example of T for SHD-PROVER by follows:

1. Design a real example E for T;
2. Interpret naturally each predicate of S according to its meaning in E;
3. Interpret naturally each function symbol (including constant) that has a corresponding instance in E (this kind of symbol is called interpreted symbol);
4. Foreach of the remaining function symbols occurring inS (the uninterpreted symbols), combine all clauses of S containing an occurrence of this symbol into an IPN form, then interpret this symbol, according to its meaning and following the interpretation rules for IPN form.

V.APPLICAIION OF THE EXAMPLE DESIGN METROD

1. AM8: The attaining minimum (or ma.ximum) value theorem in analysis: a continuous function f in a closed real interval [a,b] attains its minimum (or ma.xi­ mum) in this interval.

To prove this theorem, we use a continuity a.xiom, and the least upper bound a.xiom instantiated by this par­ ticular problem. The theorem is formalized as follows (We did not present the needed inequality a.xioms):

We first transform the negation of this theorem into a simplified first-order formula (the predicate p stands for symbol :S) F1:

In the formula F1, we have forced all occurrences of every uninterpreted function symbol, such as q, h, k, to be contained in an IPN form. So the interpretation rules for IPN form can be used in interpreting these skolem functions.

According to the meaning of the theorem, we de­ signed an example, shown in Figure 1. The interpretation for the interpreted functions or predicates of the theorem are natural:

Notice that, by the above interpretation, an atom, such as p(f ( a), a), will be interpreted to "unknown" , be­ cause it would be "semantically meaningless" to write [f(a)]I :S [a]I according to the example shown as Fig­ ure 1, since the two arguments of :S belong to different types: the point [f(a)]I = 104 is on the Y-axis and the point [a]I = -4 is on the X-axis. Notice also that, we de­ fined the function f only in the interval [ -4, 8] of X-axis. This restriction allows the procedure to prevent some re­ dundant resolvents. For example, a resolvent containing a term f(f(a)) or J(f(l)) must be discarded, because f is undefined in [f(a)]I or [f(l)]I·

Now we interpret the skolem function q, which is con­ tained in the fourth conjunct of F1:

For the meaningful interpretation, we need only to consider two cases:

1. x E [-4,0]. Then [p(x,l)]I = true. By interpretation rule 2 for IPN form, at most one among the literals p(a, q(x)),p(q(x), x) and ·p(f(x), f(q(x))) (each cor­ responds a C; in the definition of IPN form) can be interpreted to false. So we can interpret q to be a function, which maps the point x,x E [-4,0], to a point x',x' E [-4,-2 x x) (see Figure 1). In con­ trast, if q were interpreted to map the point x to a point point x",x" E [-2 x x,8], then there would be two literals P(q(x)), x) and ·P(f(x), f(q(x))) inter­ preted to false. We tested some different interpreta­ tions, such as q(x) = -4, q(x) = x (AM8a of Table 1), q(x) = -2xx (AM8b oftable 1) and q(x) = 8, for q(x),x E [-4,0], by running the prover with identical other conditions. The prover succeeded with the use of the first two interpretations, which satisfy the in­ terpretation rules, and failed with the use of the last two interpretations, which did not satisfy the inter­ pretation rules.
2. x E (0,8]. Then [p(x,l)]I,[·p(a,x)] 1 and [·p(x,b)J 1 are all false. By interpretation rule 1 for IPN form, we should interpret all of p( a, q( x)), p( q ( x), x) and ·p(f(x), f(q(x))) to true. Thus the following rela­ tions should be satisfied:

Consulting Figure 1, we define q(x) = 0.5 x x for x E (0, 8]. The final interpretation for q can be

By a similar process, we interpret the skolem function h, contained in the fifth conjunct of F1, as follows:

The skolem function k occurs in the last IPN form of the above formula F1:

Because the last conjunct, ·p(f(u), f(k(u))), to­ gether with the first two disjuncts will form the goal clause of the input set, which should be interpreted to false. Ac­ cording to the meaning of the theorem, the function k(u) is meaningful only for u=O in this example, so we interpret k as follows:

The domain Do is obtained by the subroutine DO­ MAIN_GENERATOR, where we set domainJimit = 3,

By the help of this example, the prover obtained a quite efficient proof (see Table 1): only 68 resolvents ac­ cepted, among which 30 were useful. 4 useful resolvents were produced by resolving goals against some resolvents that were true in the model. So the hierarchical deduc­ tion structure, which retained these resolvents as rules, was important for this proof.

2. IMV: The mean value theorem in analysis: If function f is continuous in a real closed interval [a, b], where f(a) ~ 0 and 0 ~ f(b), then 3xf(x) = 0.

Several interesting interpretations of uninterpreted skolem functions, similar to the interpretation of skolem function q in AM8, were encountered in designing exam­ ples for this theorem. One can find the set of clauses for this theorem in [8]. This problern has been considered in [2]. A different example was designed by us according to our interpretation rules.

3. GCD: If gcd(a, b) is the greatest common divisor of two positive integers a and b, then for any positive integer e, gcd(a x e,b x e) = gcd(a,b) Xe.

Let g(x, y, u) denote u = gcd(x,y), and d(x, y) denote x properly divides y. Then the theorem is represented as the follows:

The second conjunct of the above formula is the def­ inition of positive integers gcd. The third conjunct is the assertion of the existence of the gcd. Number the­ ory is a typical example for this theorem. We interpreted a, b, c, d, e, g naturally:

Skolemizing the definitions of gcd and the third con­ junct introduced skolem functions i and k, each of which was forced to be contained in an IPN form:

The following interpretations for i and k satisfy in­ terpretation rules for IPN forms, which were used by the prover:

A subset of axioms about the product operator X, and the proper division operator I was used in proving this theorem. These operators were interpreted accord­ ing to their natural meanings. The domain is produced by DOMAIN_GENERATOR with domainJimit = 1. An commu­ tative unification algorithm and a sorting ground commu­ tative terms subroutine were used by the prover to avoid explicitly including commutative laws into input set of clauses.

1. LCM: If lcm(a, b) is the least common multiple of two positive integers, a and b, then

The above theorem GCD, was used as a Iemma in proving this theorem. Let l(x,y,u) mean u = lcm(x,y), and Iet the predicates g and d be the same as that of GCD, then the theorem is represented as follows:

The same subset of axioms for the operators x and I, and a similar strategy in dealing with commutative laws as that for proving GCD were used in proving this theorem. The example designed for this theorem is similar to GCD, but is augmented by interpretations for predicate l and a skolem function i obtained by skolemizing the definition of LCM. We do not go into much detail.

5. SST: In AAAI 1984, C. Walther reported his suc­ cess of using many-sorted resolution to prove Schubert's statement (SST). It was said that this problern was so hard, that no automatic prover could ever obtain a proof, except the many sorted resolution prover. After the meet­ ing, we submitted this problem, together with an exam­ ple designed according to the meaning of the statement, to our SHD-PROVER. Without any difficulty, the prover succeeded.

To understand our design of the example for this problem, the reader can refer to [7] for finding the original statement of the problern and the resulted set of clauses.

Several skolem constants occur in the set of clauses, each of which corresponds to a type of entities, where

w0 : a wolf bo: a bird so: a snail / 0 : a fox co: a caterpillars go: grain.

To facilitate implementation, we interpret each entity as a integer:

With the above interpretations of entities and accord­ ing to the meaning of each sentence of the statement, we interpret the predicates occurring in the set of clauses as follows:

Three skolem functions occurred in the set of clauses, each of which could be forced to be contained in an IPN form:

Then they were interpreted as follows:

The domain Do consists of a finite set of integers: D0 = {2,3,5,7,11,13}.

We should emphasize that, different from the many­ sorted resolution, our use of this example includes both type information and the knowledge for guiding the prover to select semantically provable paths.

Table 1 is a summary of the computer runs by SHD­ PROVER in proving (without interaction) these theorems with the help of the above examples. The prover was run on the Symbolics 3600. The code has not been weil optimized. The heuristic search strategy (it was described in [8]) based on syntactic featureswas important to these proofs, but no particular heuristics were added to help prove different theorem, except some control parameters, such as the Iimit of search depth, the Iimit of function nesting depth, etc. may be different.

ACKNOWLEDGMENTS

The author is grateful to W. W. Bledsoe who con­ tributed valuable suggestions and helped with phrasing for this manuscript, also to L. Wos, L. J. Henschen and A. M. Ballantyne for their help related to this topic.