No label defined (Q4524786)

This chapter introduces special techniques for enhancing proof systems in terms both of their efficiency and of their range of applicability. Gains in efficiency are achieved through the general principle of compression, and applications other than theorem proving in first-order logic are made possible by extensions of the underlying methods. The work presented develops an advanced proof system for a compressed version of tableaux, the connection method. Two specialized techniques are presented in detail: the first one introduces the concepts of DB-reductions and DB-unification, and applies to the class of problems which involve many facts and are similar to databases. The technique may be considered as a lazy evaluation strategy, for the search for a particular solution is not commited until it is forced to. This results in a compression of the search space of possible tableaux. The second technique is a non-clausal decision procedure for propositional logic in the form of a generalization of the standard Davis-Putnam procedure. Although theoretically the generalization is straightforward, compression of the formula as well as of the corresponding search space is obtained. A section is devoted to three different topics such as equivalences, subsumption, and default reasoning. The three topics are surveyed, not entering into details, showing how the first two items are instances of compression, while the last one illustrates how classical proof techniques can be exported to extended logics. The techniques introduced in this chapter have been developed in the context of the implementation of the KoMeT theorem proving system, to which several references are made in the text. For the entire collection see [Zbl 0948.00015].