A formally verified cut-elimination procedure for linear nested sequents for tense logic (Q2142082): Difference between revisions

@@ Property / describes a project that uses @@
+Haskell
@@ Property / describes a project that uses: Haskell / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-030-86059-2_17
+Normal rank
@@ Property / OpenAlex ID @@
+W3198628855
@@ Property / OpenAlex ID: W3198628855 / rank @@
+Normal rank
@@ Property / cites work @@
+Display logic
@@ Property / cites work: Display logic / rank @@
+Normal rank
@@ Property / cites work @@
+Formalized meta-theory of sequent calculi for linear logics
+Normal rank
@@ Property / cites work @@
+Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi
+Normal rank
@@ Property / cites work @@
+From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
+Normal rank
@@ Property / cites work @@
+Q4484337
@@ Property / cites work: Q4484337 / rank @@
+Normal rank
@@ Property / cites work @@
+Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
+Normal rank
@@ Property / cites work @@
+Q2753601
@@ Property / cites work: Q2753601 / rank @@
+Normal rank
@@ Property / cites work @@
+Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents
+Normal rank
@@ Property / cites work @@
+Cut-free sequent calculi for some tense logics
@@ Property / cites work: Cut-free sequent calculi for some tense logics / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive decision via redundancy-free proof-search
+Normal rank
@@ Property / cites work @@
+A formal framework for specifying sequent calculus proof systems
+Normal rank
@@ Property / cites work @@
+Proof analysis in modal logic
@@ Property / cites work: Proof analysis in modal logic / rank @@
+Normal rank
@@ Property / cites work @@
+A fresh view of linear logic as a logical framework
+Normal rank
@@ Property / cites work @@
+Structural Focalization
@@ Property / cites work: Structural Focalization / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Cut Elimination of Coalgebraic Logics in Coq
+Normal rank
@@ Property / cites work @@
+Q4716271
@@ Property / cites work: Q4716271 / rank @@
+Normal rank
@@ Property / cites work @@
+Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
+Normal rank
@@ Property / cites work @@
+Mechanizing focused linear logic in Coq
@@ Property / cites work: Mechanizing focused linear logic in Coq / rank @@
+Normal rank