ACM Transactions on Computational Logic

We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in ...

This article studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely, those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from ...

The article proposes a trimodal logical system that can express the strategic ability of coalitions to learn from their experience. The main technical result is the completeness of the proposed system.

We prove an algebraic canonicity theorem for normal LE-logics of arbitrary signature, in a generalized setting in which the non-lattice connectives are interpreted as operations mapping tuples of elements of the given lattice to closed or open elements of ...

We extend to natural deduction the approach of Linear Nested Sequents and of 2-Sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction: only one introduction and ...

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be ...