Tableaux with Accelerated Search

Automated deduction in non-classical logics is an important field of research in areas of computer science such as software verification and security analysis. The project is in the heart of this field and addresses systems of tableaux. Among the virtues of this family of deduction systems are (1) readability of proofs, (2) ability to construct counterexamples and (3) applicability to a large class of non-classical logics - three crucially important points for a number of practical applications. For class ical logics, proof-search in tableau systems has proved less efficient than for resolution systems, mainly due to two computationally significant shortcomings recently overcome by independent work within the PMA group in Oslo (the method of uniform variab le splitting) and the Formal Methods group in Göteborg (the incremental closure technique). This project aims at integrating the two contributions in a new tableau system for classical logic and extending the methods to a wide range of non-classical logic s.