Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
From MaRDI portal
Publication:5079741
DOI10.4230/LIPICS.CSL.2018.17OpenAlexW2888803631MaRDI QIDQ5079741FDOQ5079741
Liron Cohen, Reuben N. S. Rowe
Publication date: 28 May 2022
Full work available at URL: https://dblp.uni-trier.de/db/conf/csl/csl2018.html#0001R18
completenesstransitive closureinductionsoundnessstandard semanticsinfinitary proof systemscyclic proof systemshenkin semantics
Cites Work
- Untersuchungen über das logische Schliessen. I
- Handbook of proof theory
- Proof theory. 2nd ed
- Fundamental properties of infinite trees
- The relative efficiency of propositional proof systems
- Completeness in the theory of types
- Sequent calculi for induction and infinite descent
- Title not available (Why is that?)
- Accessible Independence Results for Peano Arithmetic
- Title not available (Why is that?)
- Title not available (Why is that?)
- General Models and Completeness of First-Order Modal -calculus
- Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
- Cyclic proofs of program termination in separation logic
- Title not available (Why is that?)
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- Completeness for ancestral logic via a computationally-meaningful semantics
- A cut-free cyclic proof system for Kleene algebra
- Ancestral Logic: A Proof Theoretical Study
- Cyclic Arithmetic Is Equivalent to Peano Arithmetic
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- Title not available (Why is that?)
- Automatically verifying temporal properties of pointer programs with cyclic proof
Cited In (6)
- Lemmaless induction in trace logic
- Geometric Rules in Infinitary Logic
- Cyclic hypersequent system for transitive closure logic
- Non-well-founded deduction for induction and coinduction
- Integrating induction and coinduction via closure operators and proof cycles
- Cyclic proofs, hypersequents, and transitive closure logic
This page was built for publication: Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5079741)
