Tableau methodology for propositional logics

TL;DR

This paper introduces a general tableau methodology for propositional logics, enabling systematic construction and analysis of tableau systems across different semantics and logic variants.

Contribution

It develops a universal tableau metatheory that simplifies the creation of complete tableau systems and generalizes consistency properties across propositional logics.

Findings

Provides a formal framework for tableau systems

Simplifies the construction of complete tableau systems

Generalizes consistency properties for propositional logics

Abstract

We set out a general methodology for producing tableau systems for propositional logics via a tableau metatheory that provides general and formal notions for different tableau systems that vary by semantics or formulae. Moreover, by dint of these general notions, some facts, independent of their applications to a particular propositional logic, can be proved. One of the examples is the tableau metatheorem that simplifies the process of constructing a complete tableau system for a given logic, just reducing it to checking specific properties of the tableau rules within the analyzed, particular system. In our paper we generalize an abstract consistency property proposed by R. Smullyan and M. Fitting from the modal case to the others. Such a methodology is essential for a deeper and universal treatment of tableau methods for various propositional languages and semantics.