A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic.

Caitlin D'Abrera Jeremy E. Dawson Rajeev Goré

Published in: TABLEAUX (2021)

Keyphrases

sequent calculus
cut elimination
linear logic
inference rules
sequent calculi

natural deduction
modal logic
proof theoretic
proof search
linear time temporal logic

intuitionistic logic
fixed point
logic programming
logical framework
theorem proving

theorem prover
desirable properties
classical logic
search procedure
temporal logic