Conceptual
Browse Instruct Curate

Nested-Sequent Calculus for the Quantum Modal Logic MB

The modal logic MB is the modal counterpart (via a McKinsey-Tarski-style translation) of extended quantum logic, designed to reason about the absolute value of the inner product between quantum states. This work builds a nested-sequent calculus for MB, using it to prove the completeness theorem and the decidability of MB's validity problem, and introduces an extended logic MB+ with additional modal symbols.