Minimal structures for modal tableaux: Some examples

Abstract

In this paper we present some examples of decision procedures based on tableau calculus for some mono- and multimodal logics having a semantics involving properties that are not easily representable in tree-like structures (like e.g. density, confluence and persistence). We show how to handle them in our framework by generalizing usual tableaux (which are trees) to richer structures: rooted directed acyclic graphs.