Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

DOI10.4230/LIPICS.CSL.2018.17MaRDI QIDQ5079741zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

completenesstransitive closureinductionsoundnessstandard semanticsinfinitary proof systemscyclic proof systemshenkin semantics

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Non-well-founded proof theory of transitive closure logic
• Sequent calculi for induction and infinite descent
• Ancestral Logic: A Proof Theoretical Study
• Automated Reasoning with Analytic Tableaux and Related Methods
• scientific article; zbMATH DE number 408795

Cites work

• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 1956528 (Why is no real title available?)
• scientific article; zbMATH DE number 2087442 (Why is no real title available?)
• scientific article; zbMATH DE number 3365218 (Why is no real title available?)
• A cut-free cyclic proof system for Kleene algebra
• Accessible Independence Results for Peano Arithmetic
• Ancestral Logic: A Proof Theoretical Study
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Completeness for ancestral logic via a computationally-meaningful semantics
• Completeness in the theory of types
• Cyclic arithmetic is equivalent to Peano arithmetic
• Cyclic proofs of program termination in separation logic
• Equivalence of inductive definitions and cyclic proofs under arithmetic
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• Fundamental properties of infinite trees
• General Models and Completeness of First-Order Modal  -calculus
• Handbook of proof theory
• Proof theory. 2nd ed
• Sequent calculi for induction and infinite descent
• The relative efficiency of propositional proof systems
• Untersuchungen über das logische Schliessen. I

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)