SETHEO V3.2: Recent Developments – System Abstract –

Chr. Goller, R. Letz, K. Mayr, J. Schumann

Institut für Informatik, Technische Universität München D-80290 München email: setheo@informatik.tu-muenchen.de

1 Introduction

SETHEO is a theorem prover for first-order predicate logic. The original system, which has been developed within the ESPRIT project 415, is described in [LSBB92]. SETHEO is a top-down prover based on the calculus of so-called connection tableaux [LMG93] which generalizes weak model elimination [Lov78]. Proofs are found by a consecutively bounded depth-first iterative deepening search with backtracking. The search procedure is implemented as an abstract machine which extends the Warren Abstract Machine [War83]. The system is being continuously extended and enhanced with additional inference mechanisms and reduction techniques. The current version of SETHEO is V3.2. In this paper we describe the major improvements of the new system with respect to the system described in [LSBB92].

2 Additional Inference Rules

Since, due to its cut-freeness, the basic calculus is among the weakest proof systems concerning proof compactness, many proofs cannot be found, simply because no sufficiently short proofs exist in the calculus. Therefore, in [LMG93] controlled ways of integrating the backward cut rule are investigated. The techniques developed there are the folding up and the folding down operation. Folding up, which generalizes C-reduction [Sho76], represents an efficient way of supporting the basic top-down calculus with lemmata derived in a bottom-up manner. Folding down is equivalent to factorization (of subgoals) in model elimination and the connection calculus. Both mechanisms have been implemented in a very efficient manner and are now available in the system. Experiments with a number of representative examples from the field of automated deduction demonstrate that for difficult problems the system with folding up performs significantly better than the cut-free variant of connection tableaux and the one with folding down. Thus, using folding up one can easily solve problems which are out of scope or at least extremely difficult for pure top-down oriented cut-free tableau procedures, like the intermediate value theorem (ivt) or the algebraic problems wos31 and wos33, as shown below in the table of measurements.

3 Tableau Subsumption and Anti-Lemmata

In contrast to the most successful style of resolution theorem proving which is based on a formula enumeration or saturation procedure, such an approach is not possible in the connection tableau framework, because, unlike resolution and unlike the original tableau calculus, the connection tableau calculus is not proof confluent, that is, not every refutation attempt of an unsatisfiable formula can be completed successfully. This possibility of making irreversible decisions in the calculus demands a different organization of the proof process, namely, as a tableau enumeration instead of a formula enumeration procedure. The structure implicitly explored by the backtracking-driven tableau search procedure of SE-THEO is a tree of tableaux. There are two different methodologies for reducing the search effort of tableau enumeration procedures. On the one hand, one can attempt to refine the tableau calculus, that is, disallow certain inference steps if they produce tableaux of a certain structure—the regularity condition described in [LSBB92] is of this type. The effect on the tableau search tree is that the respective nodes together with the dominated subtrees can be ignored, so that the branching rate of the tableau search tree decreases, whereas minimal proof length cannot be preserved (see [LMG93]). These structural methods of redundancy elimination are local pruning techniques in the sense that they can be performed by looking at single tableaux only.

The other approach is to improve the proof search procedure so that information coming from the proof search itself can be used to even eliminate proof attempts not excluded by the calculus. More specifically, these global methods compare competitive tableaux in the search tree, i.e., tableaux on different branches, and attempt to show that one tableau (together with its successors) is redundant in the presence of the other. A natural approach here is to exploit subsumption between tableaux, in a similar manner subsumption between clauses is used in formula saturation procedures like resolution. To this end, in [LMG93] the notion of subsumption has been generalized from clauses to literal trees, and it is shown under which conditions subsumed tableaux can be deleted. Unfortunately, a direct application of subsumption deletion is only possible in explicit tableau enumeration procedures. The technique is not compatible with the Prolog-like search procedure of SETHEO, since at any time only one tableau is in memory and the information about the existence of alternative (possibly subsuming) tableaux is not available. A restricted concept of subsumption deletion, however, can be achieved with the mechanism of so-called anti-lemmata, which avoids that the same (or more special) solutions of subgoals are computed several times.

Generation and application of anti-lemmata Whenever a subgoal N in a tableau has been solved, the computed solution substitution σ of N is stored at the node N. If the solution of subsequent subgoals fails and the proof procedure backtracks over the node N, then σ is turned into an anti-lemma. In any alternative solution process of the subgoal N, if a substitution τ = τ_{1} ⋯ τ_{m} is computed such that one of the anti-lemmata stored at the node N is more general than τ, then the proof procedure immediately backtracks. When the search state at which N was selected for solution is backtracked, then all anti-lemmata at N are deleted.

It can be shown, that whenever an anti-lemma σ for a tableau node N in a tableau T is more general than a substitution τ computed during an alternative solution attempt T′ of N, then T subsumes the alternative tableau T′. Consequently, the described anti-lemma mechanism achieves a restricted form of subsumption deletion. All cases of tableau subsumption, however, cannot be captured with this technique, since when a completely failed subgoal N is deleted, then all anti-lemmata at N disappear, too. More permanent anti-lemmata require caching techniques as used in [Ast92]. However these techniques are very expensive and normally only applied in the Horn-case, whereas anti-lemmata can be used efficiently in the non-Horn-case too.

4 Constraint Technology

In [LSBB92] it has been demonstrated that the tableau refinements which forbid cases of irregularity, tautological tableau clauses, and tableau clauses which are subsumed by other input clauses can be reformulated as syntactic disequation constraints between term lists. Fortunately, the same holds for the implementation of the anti-lemma mechanism. As a consequence, in the new version a constraint handling mechanism has been integrated similar to the ones available in advanced Prolog systems like SEPIA or SIXTUS Prolog. The constraints are carried along with the current tableau in order to control the instantiations of the variables in the tableau. Whenever a constraint is violated the proof procedure backtracks.

The constraint management is carried out by using disunification. Here maximal efficiency is obtained by keeping the constraints in a solved form where the left sides of the contraints are lists of variables. This permits that whenever variables are instantiated in the unification routine, then the constraints to be checked can be accessed very quickly.

The used constraint mechanism provides a uniform and highly efficient method for implementing the mentioned search pruning reductions. The integration of this technique is a natural extension of the abstract machine and it permits to detect suboptimal or unsolvable tableaux as early as possible.

5 Bounds for Completeness

As tableau enumerating strategy, SETHEO uses consecutively bounded depth-first iterative deepening search with backtracking. In this approach iteratively larger finite initial parts of the search tree are explored by imposing bounds on the sizes and structures of the permitted tableaux. The two bounds used traditionally in SETHEO are the depth and the number of inferences of the current tableau (compare [Sti89] and [Ast92]). In order to provide more flexibility for focussing the search process SETHEO V3.2 offers several additional bounds, like the number of distinct free variables, the term complexity of the open subgoals and the number of tried/open alternatives of all existing choice points in the current tableau.

6 Table of Results

In order to demonstrate the effect of the new techniques, particularly the new inference rules, we wish to present the results for running 12 well-known examples from the field of automated deduction. All three systems are using antilemmata. The first one is the cut-free system, the others apply factorization and C-reduction steps, respectively. As bound we have used a complex bound limiting both the depth and the inferences in tableaux. The values in the ‘proof’-column are the numbers of proof inferences, in brackets the numbers of factorization steps and C-reduction steps are given, respectively. The problems were run on a SUN SPARC 10, the time is given in seconds. For a more detailed description of the experiments see [LMG93].

Problem  Cut-free  Model  Model
Model  Elimination Elimination
Elimination + factorization + C-reduction
Name Horn Size time proof time proof time proof
wos1 yes 17 1.8 10 .2 11(2) .1 11(1)
wos10 yes 20 25.6 15 68.3 15(0) 48.5 15(0)
wos11 yes 22 4.5 9 9.1 9(0) 6.5 8(0)
wos22 yes 34  3.8 14 11.8 14(0) 11.5 14(0)
wos31 no 23 ≫ 10^{4}  1214.8 55(16) 12.5 55(10)
wos33 no 26 ≫ 10^{4} ≫ 10^{4} 37.5 59(18)
apabhp no 18 130.7 14 149.7 14(0) 253.9 14(1)
ex5  no 15  4.8 18  6.7 15(1) 6.6 14(1)
ls108 no 16 17.8 40  8.4 23(3)  .2 21(3)
ls112 no 23 28.8 56  2.7 60(8) 1.7 60(9)
ls121 no 21 5.7 27 32.4 29(0) .3 20(3)
ivt  no 17 6787.6 99 9849.4 99(0) 14.3 41(13)

The experiments clearly demonstrate that the proof procedure with folding up (C-reduction) perform significantly better than the other two. While the relative loss in efficiency is limited to a factor of 3, the relative gain in efficiency with respect to the other systems is often by magnitudes. Let us describe the benefit of shortening proofs for the proof search with the intermediate value theorem (ivt). The cut-free proof we have found needs 99 inference steps and has depth 8. With the folding up mechanism the proof length can be reduced to 41 steps and, which seems even more crucial, the depth of the proof to 6. Consequently, the proof is found two levels earlier. This explains the achieved speed-up of about 500. The same holds for the problems wos31, wos33, ls108, and ls121. Interestingly, even in cases where the proof is on the same level, a speed-up can be achieved, namely, for the problems wos1 and ls112.

Additional experiments have shown that indeed techniques like anti-lemmata are needed in order to successfully compensate the redundancies caused by the new inference rules folding up and folding down. Just to give one example, the solution process of the problem wos31 needs 40 times more time if no antilemmata are used.

7 The SETHEO System

The SETHEO system includes an X-based graphical user interface to facilitate its usage, especially for the novice. Both the search process and the proof tree (a tableau with applied substitutions) can be displayed graphically. Features for scrolling and hiding parts of the tableau allow to represent even extremely large tableaux in a readable manner.

Since SETHEO is based on Prolog abstract machine technology, it can also be used for logic-programming purposes. A set of Prolog-style built-ins and additional features (like backtrackable global variables) are provided and can be combined with the basic theorem proving techniques of SETHEO (e.g., sound unification, access of the current path in the tableau, iterative deepening).

The entire system is implemented in C as a set of independent programs. Additionally, several stand-alone preprocessing modules, like a bottom-up deltaiterator [?] are available.

Binaries and documentation are available via ftp from:

flop.informatik.tu-muenchen.de in directory /fki/setheo.

For free sources and further information, please send e-mail to

setheo@informatik.tu-muenchen.de.

References

[Ast92] O. W. Astrachan and M. E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. Proceedings of the 11th Conference on Automated Deduction (CADE-11), LNAI 607, Saratoga Springs, pages 224–238, Springer, 1992.

[Lov78] D. W. Loveland. Automated Theorem Proving: a Logical Basis. North– Holland, 1978.

[LSBB92] R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8(2):183– 212, 1992.

[LMG93] R. Letz, K. Mayr, and C. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Technical Report, Techn. Univ. Munich, 1993.

[Sho76] R. E. Shostak. Refutation Graphs. Artificial Intelligence, 7:51–64, 1976.

[Sti89] M. E. Stickel. A Prolog Technology Theorem Prover: a new Exposition and Implementation in Prolog. Stanford, 1989.

[War83] D.H.D. Warren. An Abstract PROLOG Instruction Set. Technical report, SRI, Menlo Park, Ca, USA, 1983.