Fragments of arithmetic and cyclic proofs
From MaRDI portal
Cites work
- -Calculus with Explicit Points and Approximations
- A cyclic proof system for HFL\(_\mathbb{N}\)
- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
- A Proof System for the Linear Time μ-Calculus
- A realization theorem for the Gödel-Löb provability logic
- A realization theorem for the modal logic of transitive closure \(\mathsf{K}^+\)
- A tableau system for the modal -calculus
- Automated Reasoning with Analytic Tableaux and Related Methods
- Circular proofs for the Gödel-Löb provability logic
- Classical system of Martin-Löf's inductive definitions is not equivalent to cyclic proofs
- Coalgebraic proof translations for non-wellfounded proofs
- Computational expressivity of (circular) proofs with fixed points
- Cut Elimination in the Presence of Axioms
- Cyclic arithmetic is equivalent to Peano arithmetic
- Cyclic proofs of program termination in separation logic
- Equivalence of inductive definitions and cyclic proofs under arithmetic
- Games for the -calculus
- Global neighbourhood completeness of the provability logic \textsf{GLP}
- Hierarchies of Primitive Recursive Functions
- scientific article; zbMATH DE number 6680140 (Why is no real title available?)
- scientific article; zbMATH DE number 2087442 (Why is no real title available?)
- scientific article; zbMATH DE number 7155168 (Why is no real title available?)
- scientific article; zbMATH DE number 227056 (Why is no real title available?)
- Induction rules in bounded arithmetic
- Induction rules, reflection principles, and provably recursive functions
- Infinitary proof theory: the multiplicative additive case
- Local validity for circular proofs in linear logic with fixed points
- Lyndon Interpolation for Modal $$\mu $$-Calculus
- Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
- On parameter free induction schemas
- On structural proof theory of the modal logic \(\mathsf{K}^+\) extended with infinitary derivations
- On the proof theory of the modal mu-calculus
- On the scheme of induction for bounded arithmetic formulas
- Programming languages and systems. 10th Asian symposium, APLAS 2012, Kyoto, Japan, December 11--13, 2012. Proceedings
- Proof-theoretic analysis by iterated reflection
- Sequent calculi for induction and infinite descent
- Structural proof theory. With an appendix by Aarne Ranta
- The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
- Uniform interpolation from cyclic proofs: the case of modal mu-calculus
- Unprovability results for clause set cycles
This page was built for publication: Fragments of arithmetic and cyclic proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6866420)