A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs (Q4506460): Difference between revisions

@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Q5610986
@@ Property / cites work: Q5610986 / rank @@
+Normal rank
@@ Property / cites work @@
+Contraction-free sequent calculi for intuitionistic logic
+Normal rank
@@ Property / cites work @@
+Termination of permutative conversions in intuitionistic Gentzen calculi
+Normal rank
@@ Property / cites work @@
+On proof normalization in linear logic
@@ Property / cites work: On proof normalization in linear logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264727
@@ Property / cites work: Q4264727 / rank @@
+Normal rank
@@ Property / cites work @@
+Permutability of proofs in intuitionistic sequent calculi
+Normal rank
@@ Property / cites work @@
+Q4716271
@@ Property / cites work: Q4716271 / rank @@
+Normal rank
@@ Property / cites work @@
+Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
+Normal rank
@@ Property / cites work @@
+Rippling: A heuristic for guiding inductive proofs
+Normal rank
@@ Property / cites work @@
+Q3817590
@@ Property / cites work: Q3817590 / rank @@
+Normal rank
@@ Property / cites work @@
+Residual theory in λ-calculus: a formal development
+Normal rank
@@ Property / cites work @@
+Metamathematics, Machines and Gödel's Proof
@@ Property / cites work: Metamathematics, Machines and Gödel's Proof / rank @@
+Normal rank