The cut-free single-succedent Gentzen sequent calculus ${\mathsf{GK}}_t$ for the minimal tense logic ${\mathsf{K}}_t$ is introduced. This sequent calculus satisfies the displaying property. The proof proceeds in terms of a Kolmogorov translation and three intermediate sequent systems. Finally, we show that tense logics axiomatized by strictly positive implication have cut-free Gentzen sequent calculi uniformly.

Layered algebras are introduced and used to express layered graphs. Layered graphs are considered to be a highly effective abstract tool to manage the difficulty in conceptualizing and reasoning regarding complex systems related to coding in email exchange and access control in security. In the present paper, we study the varieties of several classes of lattice-based layer algebras and show that all these varieties have decidable equational theory via a finite model property.

We investigate involutive commutative residuated lattices without unit, which are commutative residuated lattice-ordered semigroups enriched with a unary involutive negation operator. The logic of this structure is discussed and the Genzten-style sequent calculus of it is presented. Moreover, we prove the decidability of this logic.