Hypertableau and path-hypertableau calculi for some families of intermediate logics

Abstract

In this paper we investigate the tableau systems corresponding to hypersequent calculi. We call these systems hypertableau calculi. We define hypertableau calculi for some propositional intermediate logics. We then introduce path-hypertableau calculi which are simply defined by imposing additional structure on hypertableaux. Using pathhypertableaux we define analytic calculi for the intermediate logics Bdκ, with κ ≥ 1, which are semantically characterized by Kripke models of depth ≤ κ. These calculi are obtained by adding one more structural rule to the path-hypertableau calculus for Intuitionistic Logic. © Springer-Verlag Berlin Heidelberg 2000.