Accelerating tableaux proofs using compact representations (Q1334905)

A modified form of tableau calculus, called tableau graph calculus, is introduced. The aim is to overcome the well-known inefficiencies of the traditional tableau calculus. The new calculus is based on a compact representation of analytic tableaux by using tableau graphs. Such graphs can be generated from the input formula in linear time. As a result, the tableau graph calculus has only a single rule that is repeatedly applied to obtain a proof. Many optimization heuristics are presented as well.