Coalgebraic proof translations for non-wellfounded proofs

Borja Sierra Miranda; Lukas Zenger; Thomas Studer

REVIEW 3 major objections 4 minor 21 references

Coalgebraic proof translations for non-wellfounded proofs

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper proves that a local proof-translation step between two local-progress calculi can be lifted by coalgebraic corecursion to a translation of all non-wellfounded proofs, and applies this to cut-elimination for non-wellfounded Grz.

desk verdict A genuinely new corecursive framework for proof translations, but the Grz application has a real gap in Lemma 4.3 that needs a full proof before the paper is publishable. read the letter →

arxiv 2506.01711 v1 pith:2G2NWZAF submitted 2025-06-02 math.LO

Borja Sierra Miranda , Thomas Studer , Lukas Zenger This is my paper

classification math.LO MSC 03B4503F05

keywords non-wellfoundedprooftheorycoalgebracorecursionlocalprogressconditioncut-eliminationGrzegorczykmodallogicfinite-fragmentedtreestranslation

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Non-wellfounded proofs are infinite proof trees whose soundness is protected by a local progress condition: every infinite branch must pass through a progressing premise infinitely often. The paper's aim is to show that translating between two such systems needs no global handling of infinite branches, because it is enough to rewrite one finite fragment at a time. It defines a proof translation step as a map that sends the finite main fragment of a $C_0$-proof to a $C_1$-proof fragment while keeping the attached subtrees as $C_0$-proofs, and proves that corecursion then extends it to a full map from non-wellfounded $C_0$-proofs to non-wellfounded $C_1$-proofs. As an instance, the paper establishes cut-elimination for the non-wellfounded Grzegorczyk modal logic Grz by first pushing cuts out of the finite main fragment and then applying the corecursive theorem.

What carries the argument

The central object is the finite-fragmented tree: an infinite tree whose nodes are partitioned into finite convex classes, each with a unique root, so that the whole tree reads as a finite tree at the root with finite trees attached to its *-labelled leaves, and so on. The collection of finite-fragmented trees carries a coalgebra structure for the endofunctor $T$ that sends a set $X$ to pairs of a finite tree with non-wellfounded leaves and a function from those leaves to $X$; the destruct and construct maps make this collection a final coalgebra. Any proof translation step $\alpha$ satisfying the two proof-fragment conditions is then lifted to the unique coalgebra morphism into the final coalgebra, and the corecursion equation computes the global translation one finite fragment at a time.

What would settle it

Exhibit a local-progress pre-proof in which the equivalence class of some node under the relation generated by non-progressing parent-child edges is infinite; that would refute Lemma 3.6(i) and break the finite-fragmentation encoding. For the Grz instance, a concrete check is whether every inversion and contraction case in Lemma 4.3 can be carried out with local height and main-fragment cut-freeness preserved; a counterexample to any one case would collapse cuts-up and the resulting translation.

Watch

Extended reading notes

Core claim

The central claim is Theorem 3.8: if $\alpha$ is a proof translation step from a local-progress calculus $C_0$ to a local-progress calculus $C_1$, then the unique morphism from the coalgebra of finite-fragmented proofs into the final coalgebra of finite-fragmented trees restricts to a finite-fragmented proof translation, and the underlying tree map translates $\mathrm{P}^\infty(C_0)$ into $\mathrm{P}^\infty(C_1)$. The proof shows that every fragment in the corecursively constructed image is a proof fragment of $C_1$, because the subtrees reached along root-paths remain $C_0$-proofs by the second condition on $\alpha$. Applied to the non-wellfounded Grz calculus, the paper defines $\alpha$ through a function that removes all cuts from the finite main fragment by standard permutation and inversion rules, so the theorem yields that every sequent provable with cuts in the non-wellfounded system is provable without cuts.

Load-bearing premise

The load-bearing premise is that in any local-progress pre-proof the equivalence classes of nodes connected by chains of non-progressing steps are always finite (Lemma 3.6(i)), a fact the paper only sketches via Konig's lemma, and, for the Grz application, that the weakening, contraction, and inversion maps of Lemma 4.3 exist while preserving local height and main-fragment cut-freeness, because Lemma 4.4 and Lemma 4.5 use them without a written proof.

Editorial extensions

If this is right

For any pair of local-progress calculi, checking a proof translation reduces to two finite local checks: the main fragment maps to a $C_1$-proof fragment, and attached subtrees stay $C_0$-proofs.
Theorem 4.6 gives cut-elimination for non-wellfounded Grz: any sequent derivable in the system with cut has a cut-free derivation in the same infinite calculus.
Because the main fragment is finite, cut-elimination for these systems is as local as in finitary proof theory; all infinitary work is absorbed by corecursion.
The same scheme should yield cut-elimination for other local-progress logics, such as weak Grz, by adapting the function that pushes cuts out of the main fragment.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

An implicit consequence is that the method's scope is wider than Grz: any logic with a local progress condition, including modal fixed-point logics on conversely well-founded frames, should admit this style of translation once finite-fragmentation is established.
The theorem suggests a practical design rule for proof assistants: a formalized finite rewriting procedure on the main fragment, together with a proof that subtrees remain valid, automatically yields a formalized infinite-proof translation.
Viewed coalgebraically, translations between local-progress calculi may compose, since coalgebra morphisms into a final coalgebra compose; the paper does not develop this categorical reading.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's my take. The genuinely new thing is the coalgebraic packaging: finite-fragmented trees with the destruct/construct structure, used as a final coalgebra to define proof translations by corecursion. Theorem 3.8 is a clean and useful criterion: a local translation step between local-progress calculi lifts to a global proof translation. The proof of finality in Theorem 2.19 is thorough, and the identification of finite-fragmented proofs with non-wellfounded proofs (Lemma 3.6) is correct—though the finiteness argument is condensed, it's standard König's lemma and works. The cut-elimination example for Grz re-derives a known result, but does so with substantially different machinery, and the paper is straight about that.

The soft spot is real. Lemma 4.3 is load-bearing and its proof is one sentence. The functions wk, contraction, and inversions have to be defined on the whole infinite proof, not just the main fragment. An induction on local height only controls the finite main fragment; it gives no definition for the subproofs attached at progressing edges and, more importantly, no proof that the transformations preserve the local progress condition along infinite branches. If a function like inv changes which rule instances progress, Lemma 4.4's construction could produce a pre-proof that fails the progress condition, and Theorem 4.6 falls apart. This is not a cosmetic omission. The good news is that the paper's own framework is the natural fix: define these functions corecursively along the fragmentation and verify the proof-translation-step conditions. I expect it can be done, but it has to be written out.

The garbled rule in Definition 4.1 is a typesetting issue, not a math issue, but should be corrected. The reader's separate worry about Lemma 3.6(i) doesn't survive contact with the paper: an infinite equivalence class would give an infinite finitely branching branch with no progressing node, contradicting the local progress condition. So that concern is off.

Who should read this? Proof theorists who care about cyclic/non-wellfounded proofs, and anyone using corecursion to manage infinite structures. The framework is a genuine contribution. As it stands the Grz application is conditional on filling the gap in Lemma 4.3. I'd send it to a serious referee and ask for that proof; it's not a desk reject, but it's not a minor revision either.

Referee Report

3 major / 4 minor

Summary. This manuscript presents a method for constructing proof translations between non-wellfounded sequent calculi whose global correctness condition is a local progress condition. The method is coalgebraic: proofs are represented as finite-fragmented trees; Section 2 proves that the set of finite-fragmented trees with the destructor map forms the final coalgebra of the endofunctor T; Section 3 defines a proof translation step and shows, in Theorem 3.8, that every such step extends by corecursion to a translation on finite-fragmented proofs and hence on non-wellfounded proofs. Section 4 applies the framework to Grzegorczyk modal logic, aiming to prove that every proof in (Grz+cut)∞ can be translated to a cut-free proof in Grz∞ (Theorem 4.6).

Significance. The paper's central idea is useful and the final-coalgebra construction is a genuine contribution: it gives a uniform, category-theoretic account of translations for local-progress systems and avoids the ultrametric-space technology of earlier work. The proof of Theorem 2.19 is detailed, and the conditions in Definition 3.7 are cleanly isolated. If the missing pieces in Section 4 are supplied, the framework would be a solid tool for cut-elimination and other proof transformations in non-wellfounded proof theory. The attribution of the Grz∞ calculus to Savateev and Shamkanov is appropriate, and the proof does not appear to presuppose their cut-elimination theorem.

major comments (3)

[§4, Lemma 4.3] The proof of Lemma 4.3 is omitted, and the sentence 'All the items (i) to (vii) are provable by induction in the local height of π' does not by itself account for the infinite structure of the input. Local height is defined as the height of the main fragment (Definition 4.2), while the functions are claimed for arbitrary proofs in P∞(Grz+cut)∞. A transformation such as weakening changes sequents at the root and therefore along the main fragment; when a non-wellfounded leaf's sequent changes, the subtree attached at that leaf must be transformed as well, and that subtree may have arbitrarily large local height. An induction on the local height of the main fragment does not define the action on these attached fragments. Since Lemma 4.4 and Lemma 4.5 invoke condition (viii) repeatedly and Theorem 4.6 depends on it, this is a load-bearing gap. Please provide full constructions and proofs, for example by corecursion on the fragmentation, and verify preservation of the local progress condition on all infinite branches.
[§3, final paragraph; §4, Theorem 4.6] Theorem 4.6 is not a direct instance of Theorem 3.8 as stated. Theorem 3.8 concerns a proof translation step α : Tff -> T(Tff), whereas the function α defined in Theorem 4.6 has domain Pff(Grz+cut)∞. The last paragraph of Section 3 sketches a generalization to an arbitrary set X but does not state or prove it. Because the cut-elimination result depends on this generalized version, please promote it to a formal lemma with proof, or define α on all of Tff and verify that the proof translation step conditions hold on all finite-fragmented trees.
[§4, Lemma 4.4, Case 3, first subcase] The proof of the first subcase of Case 3 in Lemma 4.4 is not coherent as printed. The proof π concludes S0,Π•,ψ◦,ϕ◦, but the text asserts that ι0 = invψ◦(π) concludes S0,Π•,ψ◦,ϕ•, and Lemma 4.3(vii) does not justify such an inversion. The natural argument is to cut π directly against τ0 and then apply the modal rule with τ1; please rewrite this case, correct the displayed conclusion of ι0, and check that the induction hypotheses apply.

minor comments (4)

[§3, Lemma 3.6(i)] The finiteness of each ∼τ-class is only sketched. Please spell out the König's lemma argument, in particular why an infinite equivalence class would contain an infinite branch all of whose edges are non-progressing.
[§4, Definition 4.1] The modal rule is typeset in a way that makes the premise/conclusion structure ambiguous; please reformat it explicitly.
[§3, final paragraph] The notation Tnil(α)(x) and Tw(α)(x) in the final paragraph of Section 3 is not defined for an arbitrary coalgebra; please use the standard projections from the coalgebra structure or define these abbreviations.
[§4, Lemma 4.3(vii)] As printed, item (vii) states that invϕ◦ maps a proof of S,ϕ◦ to a proof of the same sequent; if this is not intended as the identity map, the statement should be corrected.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the corecursive translation theorem and the Grz cut-elimination proof are derived from stated definitions and lemmas, not from the target result or from load-bearing self-citations.

full rationale

The derivation chain is self-contained. Theorem 3.8 is a compositionality theorem: Definition 3.7 packages local conditions, namely that one step of the translation sends each proof fragment of C0 to a proof fragment of C1 and sends each subproof at a non-wellfounded leaf to a proof of C0, and the proof shows by induction along root-paths that the unique coalgebra morphism !α preserves these conditions. The final-coalgebra theorem (Theorem 2.19) is proved in the paper, not imported, so the global translation is not assumed. No step reduces the conclusion to Definition 3.7 by construction beyond the usual sense in which a compositional theorem unpacks a well-chosen local condition; the paper still proves that the infinite gluing is correct. The Grz application (Theorem 4.6) defines α from cuts-up (Lemma 4.5), and Lemma 4.5 is proved from Lemma 4.4 by induction on the number of cuts in the main fragment; Lemma 4.4 is an induction on cut-rank and local heights using Lemma 4.3. Lemma 4.3 is asserted with only a sketch, so it is a genuine load-bearing gap and a correctness risk, but it is not circular: the item functions are not defined in terms of the desired cut-elimination theorem, and the lemma is not justified by citing the earlier Savateev–Shamkanov result. The citations of [14] merely attribute the Grz∞ calculus and acknowledge an earlier proof; they do not carry the new argument. Self-citations in the introduction appear only in survey or background contexts and are not load-bearing for Theorems 3.8 or 4.6. I therefore find no exhibited reduction of a claimed result to its own input, and no self-citation chain that forces the conclusion; the appropriate finding is no significant circularity.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

No fitted parameters: the work is fully synthetic. The axioms are standard set theory (including König's lemma), definitional assumptions about local-progress calculi, and the domain assumption, inherited from the cited literature, that the presented Grz∞ rules are the non-wellfounded system for Grz.

assumptions (4)

standard math König's lemma: every finitely branching infinite tree has an infinite path.
Used in Lemma 3.6 to show each fragmentation class is finite in a proof satisfying the local progress condition.
standard math Set-theoretic foundations for trees as sets of finite words, with the category Set as the ambient category.
Assumed throughout; standard for coalgebraic arguments.
domain assumption The Grz∞ calculus defined in Definition 4.1 is a non-wellfounded proof system for the Grzegorczyk modal logic Grz.
Soundness and completeness of the calculus for Grz are not reproved; the paper cites Savateev and Shamkanov [14] and notes they established cut-elimination for the same system.
domain assumption The local progress condition (Definition 3.2) is the appropriate soundness condition for these calculi.
Assumed from the cited literature on non-wellfounded proof systems for GL and Grz [14,16].

invented entities (1)

Finite-fragmented trees and the endofunctor T
purpose: To encode non-wellfounded proofs as elements of the final coalgebra of T, enabling proof translations by corecursion.
These are new mathematical constructions justified internally by Theorems 2.19 and 3.8; there is no empirical or external falsifiable handle attached.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Coalgebraic proof translations for non-wellfounded proofs." pith.science (2026). https://pith.science/paper/2G2NWZAF

@misc{pith2026250601711,
  author       = {Pith},
  title        = {Pith review of: Coalgebraic proof translations for non-wellfounded proofs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2G2NWZAF}},
  note         = {Machine review of arXiv:2506.01711}
}

read the original abstract

Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL or Grz. In this paper, we provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instance of our method, we establish cut-elimination for a non-wellfounded system of the logic Grz. Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

21 extracted references · 15 canonical work pages

[1]

Grotenhuis, G

Afshari, B., L. Grotenhuis, G. E. Leigh and L. Zenger, Ill-founded proof systems for intuitionistic linear-time temporal logic , in: R. Ramanayake and J. Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods (2023), pp. 223–241

work page 2023
[2]

Afshari, B. and J. Kloibhofer, Cut elimination for cyclic proofs: A case study in temporal logic, in: Proceedings Twelfth International Workshop on Fixed Points in Computer Science (to appear)

work page
[3]

Afshari, B., G. E. Leigh and G. Men´ endez Turata, A cyclic proof system for full computation tree logic, in: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) , Schloss Dagstuhl-Leibniz-Zentrum f¨ ur Informatik, 2023

work page 2023
[4]

Doumane and A

Baelde, D., A. Doumane and A. Saurin, Infinitary Proof Theory: the Multiplicative Additive Case , in: J.-M. Talbot and L. Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) , Leibniz International Proceedings in Informatics (LIPIcs) 62 (2016), pp. 42:1–42:17. URL https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPI...

doi:10.4230/lipics.csl.2016.42 2016
[5]

Brotherston, J. and A. Simpson, Complete sequent calculi for induction and infinite descent, in: Proceedings of LICS-22 (2007), pp. 51–60

work page 2007
[6]

Kuznets and T

Bucheli, S., R. Kuznets and T. Studer, Two ways to common knowledge , Electronic Notes in Theoretical Computer Science 262 (2010), pp. 83–98, proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009). URL https://www.sciencedirect.com/science/article/pii/S1571066110000290

work page 2010
[7]

Das, A. and D. Pous, Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+ Lattices), in: D. R. Ghica and A. Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) , Leibniz International Proceedings in Informatics (LIPIcs) 119 (2018), pp. 19:1–19:18. URL https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.19

doi:10.4230/lipics.csl.2018.19 2018
[8]

Docherty, S. and R. N. S. Rowe, A non-wellfounded, labelled proof system for propositional dynamic logic , in: Automated Reasoning with Analytic Tableaux and Related Methods: 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings (2019), p. 335–352. URL https://doi.org/10.1007/978-3-030-29026-9_19

work page doi:10.1007/978-3-030-29026-9_19 2019

Show all 21 references

[9]

Kokkinis, I. and T. Studer, Cyclic proofs for linear temporal logic , in: D. Probst and P. Schuster, editors, Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter, Berlin, Boston, 2016 pp. 171–192. URL https://doi.org/10.1515/9781501502620-011

2016 doi
[10]

Marti, J. and Y. Venema, A focus system for the alternation-free µ-calculus, in: Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings (2021), p. 371–388. URL https://doi.o...

2021 doi
[11]

Niwi´ nski, D. and I. Walukiewicz, Games for the µ-calculus, Theoretical Computer Science 163 (1996), pp. 99–116. URL https://www.sciencedirect.com/science/article/pii/0304397595001360

1996
[12]

Rooduijn, J. M. W. and L. Zenger, An analytic proof system for common knowledge logic over s5, in: David Fern´ andez-Duque, Alessandra Palmigiano and Sophie Pinchinat (eds.) Advances in Modal Logic , 2022, pp. 659–680

2022
[13]

Ramanayake and J

Saurin, A., A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points, in: R. Ramanayake and J. Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods (2023), pp. 203–222

2023
[14]

Savateev, Y. and D. Shamkanov, Non-well-founded proofs for the Grzegorczyk modal logic, The Review of Symbolic Logic 14 (2018). 22 Coalgebraic proof translations for non-wellfounded proofs

2018
[15]

Savateev, Y. and D. Shamkanov, Cut elimination for the weak modal grzegorczyk logic via non-well-founded proofs , in: R. Iemhoff, M. Moortgat and R. de Queiroz, editors, Logic, Language, Information, and Computation (2019), pp. 569–583

2019
[16]

S., Circular proofs for the G¨ odel-L¨ ob provability logic, Mathematical Notes 96 (2014), pp

Shamkanov, D. S., Circular proofs for the G¨ odel-L¨ ob provability logic, Mathematical Notes 96 (2014), pp. 575–585. URL http://dx.doi.org/10.1134/S0001434614090326

2014 doi
[17]

Esparza and A

Simpson, A., Cyclic arithmetic is equivalent to peano arithmetic , in: J. Esparza and A. S. Murawski, editors, Foundations of Software Science and Computation Structures (2017), pp. 283–300

2017
[18]

Stirling, C., A proof system with names for modal mu-calculus , Electronic Proceedings in Theoretical Computer Science 129 (2013)

2013
[19]

Studer, T., On the proof theory of the modal mu-calculus , Studia Logica 89 (2008), pp. 343–363. URL http://www.jstor.org/stable/40268983

2008
[20]

M., Cyclic proof systems for modal fixpoint logics , ILLC Dissertation series (2024)

Turata, G. M., Cyclic proof systems for modal fixpoint logics , ILLC Dissertation series (2024)

2024
[21]

Blackburn, J

Venema, Y., Algebras and coalgebras, in: P. Blackburn, J. Van Benthem and F. Wolter, editors, Handbook of Modal Logic, Studies in Logic and Practical Reasoning 3, Elsevier, 2007 pp. 331–426. URL https://www.sciencedirect.com/science/article/pii/S1570246407800097

2007

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

Grotenhuis, G

Afshari, B., L. Grotenhuis, G. E. Leigh and L. Zenger, Ill-founded proof systems for intuitionistic linear-time temporal logic , in: R. Ramanayake and J. Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods (2023), pp. 223–241

work page 2023

[2] [2]

Afshari, B. and J. Kloibhofer, Cut elimination for cyclic proofs: A case study in temporal logic, in: Proceedings Twelfth International Workshop on Fixed Points in Computer Science (to appear)

work page

[3] [3]

Afshari, B., G. E. Leigh and G. Men´ endez Turata, A cyclic proof system for full computation tree logic, in: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) , Schloss Dagstuhl-Leibniz-Zentrum f¨ ur Informatik, 2023

work page 2023

[4] [4]

Doumane and A

Baelde, D., A. Doumane and A. Saurin, Infinitary Proof Theory: the Multiplicative Additive Case , in: J.-M. Talbot and L. Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) , Leibniz International Proceedings in Informatics (LIPIcs) 62 (2016), pp. 42:1–42:17. URL https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPI...

doi:10.4230/lipics.csl.2016.42 2016

[5] [5]

Brotherston, J. and A. Simpson, Complete sequent calculi for induction and infinite descent, in: Proceedings of LICS-22 (2007), pp. 51–60

work page 2007

[6] [6]

Kuznets and T

Bucheli, S., R. Kuznets and T. Studer, Two ways to common knowledge , Electronic Notes in Theoretical Computer Science 262 (2010), pp. 83–98, proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009). URL https://www.sciencedirect.com/science/article/pii/S1571066110000290

work page 2010

[7] [7]

Das, A. and D. Pous, Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+ Lattices), in: D. R. Ghica and A. Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) , Leibniz International Proceedings in Informatics (LIPIcs) 119 (2018), pp. 19:1–19:18. URL https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.19

doi:10.4230/lipics.csl.2018.19 2018

[8] [8]

Docherty, S. and R. N. S. Rowe, A non-wellfounded, labelled proof system for propositional dynamic logic , in: Automated Reasoning with Analytic Tableaux and Related Methods: 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings (2019), p. 335–352. URL https://doi.org/10.1007/978-3-030-29026-9_19

work page doi:10.1007/978-3-030-29026-9_19 2019