Abstract

The method of analytic tableaux is discussed with respect to the notion of computational complexity. The class of formulas that was first identified to be intractable for the tableau method I. examined, and an explicit proof of this intractability is presented. A minor addition that leads to fast proofs of these formulas is described. Several results demonstrating that tableau deductions can be substantially speeded up with applications of path dissolution, which is an inference medianism that generalises the method of analytic tableaux, are summarised