Programming Research Group Technical Monograph PRG-88

Marcello D'Agostino

November 1990, 131 pages, ISBN 0-902928-67-8

Cut-free Gentzen systems and their semantic-oriented variant, the tableau method , constitute an established paradigm in proof-theory and are of considerable interest for automated deduction and its applications. In this latter context, their main advantage over resolution-based methods is that they do not require reduction in clausal form; on the other hand, resolution is generally recognised to be considerably more efficient within the domain of formulae in clausal form.

In this monograph we analyse and develop a recently proposed alternative to the tableau method, the system KE. We show that KE, though being "close" to the tableau method and sharing all its desirable features, is essentially more efficient. We trace this phenomenon to the fact that KE establishes a closer connection with the intended (classical, bivalent) semantics. In particular we point out, in Chapter 2, a basic "redundancy" in tableau refutations (or cut-free Gentzen proofs) which depends on the form of the propositional inference rules and therefore, affects any procedure based on them. In Chapter 3 we present the system KE and show that it is not affected by this kind of redundancy. An important property of KE is the analytic cut property: cuts cannot be eliminated but can be restricted to subformulae of the theorem, so that the subformula principle is still obeyed. We point out the close relationship between KE and the resolution method within the domain of formulae in clausal form. In Chapter 4 we undertake an analysis of the complexity of the propositional fragment of KE relative to the propostional fragments of other proof systems, including the tableau method and natural deduction, and prove some simulation and separation results. We show, among other things, that KE and the tableau method are separated with respect to the p-simulation relationship (KE can linearly simulate the tableau method, but the tableau method cannot p-simulate KE). In Chapter 5 we consider Belnap's four-valued logic, which has been proposed as an alternative to classical logic for reasoning in the presence of inconsistencies, and develop a tableau-based as well as a KE-based refutation system. Finally, in Chapter 6, we generalise on the the ideas contained in the previous chapters and prove some more simulation and separation results.