Proofnets for S5: sequents and circuits for modal logic

from blog Home on consequently.org, | ↗ original
In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). The sequent derivations and proofnets...