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

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 path-hypertableaux we define analytic calculi for the intermediate logics $\Bd_k$, with $k \geq 1$, which are semantically characterized by Kripke models of depth $\leq k$. These calculi are obtained by adding one more structural rule to the path-hypertableau calculus for Intuitionistic Logic.