Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System

DOI10.1007/978-3-662-54458-7_18zbMath1486.03094OpenAlexW2611853323MaRDI QIDQ2988375

Makoto Tatsuta, Stefano Berardi

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54458-7_18

Mathematics Subject Classification ID

Structure of proofs (03F07) Inductive definability (03D70)

Related Items

Unnamed Item, Unnamed Item, Cyclic hypersequent system for transitive closure logic, Cyclic Arithmetic Is Equivalent to Peano Arithmetic, Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System, Unnamed Item, Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs, Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent, Non-well-founded deduction for induction and coinduction, Induction and Skolemization in saturation theorem proving, Cyclic proofs, hypersequents, and transitive closure logic

Uses Software

• Cyclist

Cites Work

• Unnamed Item
• Cyclic Arithmetic Is Equivalent to Peano Arithmetic
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Sequent calculi for induction and infinite descent
• Cyclic proofs of program termination in separation logic
• Accessible Independence Results for Peano Arithmetic
• Automated Cyclic Entailment Proofs in Separation Logic
• Automated Reasoning with Analytic Tableaux and Related Methods