First sound and complete nested sequent calculi for Horn-characterizable QMLs with equality and inner/outer domains via grammar-parameterized reachability rules.
On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics.Logical Methods in Computer Science, 7(2)
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
fields
cs.LO 2verdicts
UNVERDICTED 2representative citing papers
A linear nested sequent calculus for Kt is presented that admits syntactic cut-elimination, backward proof-search, and counter-model construction while using minimal nesting for converse modalities.
citing papers explorer
-
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
First sound and complete nested sequent calculi for Horn-characterizable QMLs with equality and inner/outer domains via grammar-parameterized reachability rules.
-
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
A linear nested sequent calculus for Kt is presented that admits syntactic cut-elimination, backward proof-search, and counter-model construction while using minimal nesting for converse modalities.