Tableau methodology for propositional logics
T. Jarmuzek, R. Gore
TL;DR
The paper proposes a universal tableau metatheory for propositional logics by coupling general semantic structures with a label-based, nodes-on-sets tableau framework. It defines a satisfaction-based semantics and a corresponding branch-consequence notion, and proves a Tableau Metatheorem that equates semantic entailment, branch consequences, and the existence of closed tableaux under suitable conditions. A central contribution is the general methodology plus concrete metatheoretic results (closure properties, openness/completeness of branches) and a worked multimodal, three-valued example that demonstrates automation potential. The work advances universal, automatable construction of tableau systems across diverse propositional languages and semantics, with clear pathways toward extending to first-order logic and other frameworks.
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.