Prolog Extensions Based on Tableau Calculus

I. Introduction

Problem description. Expert systems are able to draw con­ clusions from data they contain. This deductive process can adopt different forms. There is the tradition of automated theorem proving, there are the many expert systems working with a production rule formalism, and there is PROLOG, a programming language which, at the same time, is a logical language.

PROLOG has proven very successful though it has some limitations. One of them is that it only accepts Horn clauses as rules and atomic formulas as goals. This restriction makes proof search simple and effective. But some properties cannot be expressed by Horn clauses, e.g. the linearity of an order relation. There are application domains where this handicap is not severe. In the LEX (linguistics and logic based Legal EXpert system) project at Heidelberg Science Center where the paper in band was worked out, we consider the expres­ siveness of PROLOG to be too low. Only about 80 % of the knowledge in legal applications can be formulated. For the rest, we need negation, disjunction etc.

Existing solutions. Resolution calculus ([Robinson65]) is able to accept arbitrary frrst order formulas, even in non­ clausal form if the extensions described in [Murray82] are used. Some of its defects when applied in its pure form to proving mathematical theorems are discussed in [Bledsoe77]. Bledsoe points out that heuristics should play an important role. Another defect is ([Clocksin81], p.221): 'Resolution tells us how to derive a consequence from two clauses, it does not tel! us either how to decide which clauses to Iook at next or which literals to match.'

As compared with resolution based systems, Gentzen type systems did not yet attract much attention. An important theoretical article is [Beth59] where the notion of a tableau is introduced to present a Gentzen type system in a more y is satisfiable if and only if there is a non-contradictory path through its diagram, i.e. a path containing no complementary pair of literals.

This method to represent formulas is used in [Bibel83]. lt should be compared with the usual and-or-graphs. Bibel describes a procedure which directly checks for the existence of non-contradictory paths. A better way to get an overview of all paths is to arrange them into a tree.

More precisely, we call the smallest tree containing the same paths as the diagram of y the tree of y. A tableau for y is a tree for y where any contradictory branch is cut off as soon as a complementary pair occurs. (In [Beth59], a tableau does not only contain literals but also the initial formula as well as all intermediate steps. Since these steps are 'straight­ forward', it suffices to represent only the fmal result.) A proof for the unsatisfiability of y is a tableau for it in which all branches are contradictory, y is satisfiable if and only if its tree is no proof. Hence, any procedure which, given a formula, generates a tableau and checks whether it is a proof is correct and complete.

3. Tableaux for sets of propositional forumlas

Let r be a set of formulas which is to be checked for satisfiability. One way to do that is to proceed as above as if r were given by the conjunction of its elements in a fixed, but arbitrarily chosen order. For example, suppose that r ... {y;li- 1, 2, 3} where Yl .. (...., R & ...., S)IS, Yl"" (R & ...., S)l(...., R & S), Y3- ..., R. Then Figure 2 may be called a tableau for r . If r is infmite, its tableau may be infmite. Again, r is not satisfiable if and only if the tableau is a proof, i.e. all its branches are closed by contradiction. Note that a proof is necessarily fmite.

If the order ofr is not fixed, in which way can a tableau for r be composed by the tableaux of its elements so that completeness still holds ? Suppose that a tree T is composed of the tableaux of the elements of r. A branch ofT is said to cross (a tableau of) a formula y f: r if it contains as subpath a branch of the tableau for y. T is called a tableau for r if each non-contradictory branch crosses each y f: r at least once. If T is no proof, then it contains at least one non-contradictory branch. The interpretation determined by such a branch satisfies each y f: r (since it crosses it). If T is a proof, then no interpretation can satisfY r . Hence, r is unsatisfiable if and only if there is a tableau for r which is a proof.

Choosing the next formula. To make search effective, it is necessary to keep the tableau as small as possible. First, no path should cross a formula twice. Second, branches should be cut off by a complementary pair as soon as pos­ sible. For example, a better tableau than Figure 2 on page 3 is

Two literals are linked if they form a complementary pair. Furthermore, a Iitera! is linked to a formula y if it is comple­ mentary to some Iitera! in y. Suppose that a set r offormulas contains an element a singled out for some reason. a is called the goal. Furthermore, suppose that a tableau for r is being generated, starting with a, and suppose that this process is now in a state where the tableau of another y f: r has to be appended to a certain non-contradictory branch B.

The idea is to choose a y f: r so that at least one of the resulting branches contains a complementary pair. To this end, Iet 8 be the last formula crossed by B, and Iet 818 be the restriction of B to 6, i.e. that subpath of B which is part of the tableau for 8. Furthermore, Iet C (for 'choices') be the set of all y f: r with the following properties.

1. y is linked to some Iitera! on 818.
2. y is not crossed by B.

C is erdered in a certain way, e.g. by respecting a given order of r. This is used to organize backtracking. If backtracking occurs, the subtableau starting with the actually chosen y f: C is removed, and a new subtableau is generated starting with the next y f: C. We say that the choice at 8 is altered. Back­ tracking means that we go upwards on B up to the next 8 where such an altering of a choice is possible.

The following gives the whole algorithm, called SEARCH.

1. Start with the tableau for a .
2. Mark Contradietory paths.
3. If all paths are contradictory, stop with 'succeed'.
4. Otherwise, Iet B be the leftmost non-contradictory path.
5. Let C be as above.
6. If C is empty, then check whether any choice can be altered along B.
7. If yes, then backtrack.
8. Otherwise, choose a y f: r which is not yet crossed by B and go to 8. lf there is none, then stop with 'fail'.
9. Otherwise, choose a y f: C.

1. Append its tableau to B.
2. Goto 2.

This strategy is again correct and complete. Correctness follows from the fact that any tableau (found by a strategy whatsoever) with all branches closed by contradictions is a correct proof. To see completeness, note that 6.b. guarantees that all forrnulas in f are crossed exactly once by each non-contradictory branch. If it is applied to the above f with Y3 as a goal, then Figure 3 on page 4 results. .

Comparison with PROLOG. It is claimed that algonthi? SEARCH, when applied to propositional Horn clauses, ~s very close to PROLOG's search strategy. Some remarks will help to understand the claim.

The li as considered above corresponds to the current predicate. C is the set of rul~s with whi~h this predicate matches (with the above ment10ned exceptlon that matches leading to loops are avoided). Step 4 means that the frrst predicate on the right band side of a rule is chosen.

One important difference is that SEARCH does never get into a loop. This comes from the fact that C as defmed above does not contain any forrnula crossed previously by branch B. Such loop checking is essential when defmitions o~ the form P(x) = a(x) are evaluated. Note what PROLOG mter­ preters do when given the data base a - b,b - a.

The main difference comes in with 6.b. PROLOG stops at this point with 'fail'. SEARCH will in general go on and eventually generate a satisfying interpretat~on. This is ~e~es­ sary since it may e.g. happen that r contams a contradictlon which cannot be reached from the goal by chaining through linked forrnulas. Note that no PROLOG knowledge base can be inconsistent. Furtherrnore, note that resolution calculus captures this situation by working breadth-frrst.

Predicate logic Suppose f consists of arbitrary predicate logic forrnulas. A naive implementation ofthe tableau c~culus would be to substitute all Herbrand terrns for all uruversal variables in a ftxed order and then to generate a tableau from the resulting set of variable-free forrnulas (Ievel saturation). It is one of the key Observations in [Bowen82) and in [Wrightson84) that only those substituti~ns need to ~e ~er­ forrned which produce complementary parrs. The ~o~bmatlon oftheir idea (they do not worry about the proposttlonal case, e.g. backtracking) with those of this paper is not difficult and yields a strategy for full frrst order logic extending PROLOG.

4. Extensions

Our strategy may be refmed in many ways. E.g. we could extend the defmition of the choice set C in such a way that more than one link is taken into account. This would Iead far beyond PROLOG. .

Another point to be mentioned is the followmg. SEA~CH composes tableaux starting with the root. But we rrught equally weil try to compose them starting from th~ leave.s. This is nothing eise than resolution calculus. U s~g this unified view of different proof procedures, the followmg can be said.

• Resolution calculus generates a theory, i.e. a deductively closed set of forrnulas, and stops when it derives the empty clause.
• Tableau calculus generates models and stops when all cases Iead to contradiction.
• In the PROLOG case, both calculi coincide since the theory to be generated consists of atomic forrnulas only, describing the 'minimal' model.
• Resolution may make multiple use of the same inference, of Iemmas, and so reduce proof length.
• Tableau calculus may be extended to recognize loops in the generation of models and so reduce proof search length [Schönfeld83]. .

Both proof search approaches forrnalize different reasoning principles, and it seems useful to combine them. Mathema­ ticians work this way: When given an open problem, they start by deriving some relevant facts from known theorems (resolution!). But then, they disbelieve their hypothesis and try to construct counterexamples (tableau!). They may switch back to the theorems and so on. I do not claim that their reasoning principles are the ultima ratio. But this shows th~t a combination of different principles can be useful. (In addi­ tion we should not forget Bledsoe's claim for heuristics.)

To draw a fmal conclusion from all these considerations - I believe that tableau calculus is not a substitute for other calculi, but a useful complement.