Controlled use of clausal lemmas in connection tableau calculi (Q5927985): Difference between revisions

The use of clausal lemmas is investigated in order to develop a method to reduce proof lengths and depths and to provide an appropriate reordering of the search space in connection tableau calculus. Specifically, an integration of bottom-up elements, the clausal lemmas, into the top-down oriented connection tableau calculus is provided. This paper is based on results of \textit{J. Schumann} [Lect. Notes Comput. Sci. 814, 774-777 (1994)] and the author [ibid. 1421, 33-37 (1998)], where, in order to refute a set of clauses with the connection tableau calculus, a set of unit lemmas is created in a preprocessing phase to be joined to the input clauses. One contribution of this paper is a method to develop an appropriate set of clausal lemmas which can provide proof length reductions in a number of refinements and extensions of the basic connection tableau calculus. A second contribution is the intelligent control of the application of these generated lemmas. In order to control the use of lemmas, in contrast to previous approaches in which the lemmas are selected without considering the given proof task and the search scheme to be used, techniques are developed for selecting relevant lemmas based on partial evaluation techniques which consider both the given clauses to be refuted as well as the search method to be employed. To evaluate the proposed method, a number of experiments with the theorem prover Setheo have been conducted using the TPTP library.