Abstract

In this paper I propose a more general framework for tableaux-like first order classical deductions in which bottom-up inferences find a natural place. The result is a new system of proof for classical first order logic with many interesting normal form properties. Restricting myself to classical propositional logic, I show how these properties can be exploited to obtain an analytical system of proof which is not cut-free but generates shorter proofs than the usual cut-free systems