Publication:2988374

DOI10.1007/978-3-662-54458-7_17zbMATH Open1486.03095OpenAlexW2611879577MaRDI QIDQ2988374FDOQ2988374

Alex Simpson

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_17

Mathematics Subject Classification ID

Structure of proofs (03F07) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Sequent calculi for induction and infinite descent
• On the proof theory of the modal mu-calculus
• Games for the \(\mu\)-calculus
• Cyclic proofs of program termination in separation logic
• The Logical Strength of Büchi's Decidability Theorem
• A Proof System for the Linear Time μ-Calculus
• A Proof System for Compositional Verification of Probabilistic Concurrent Processes
• Automated Reasoning with Analytic Tableaux and Related Methods
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Automated Cyclic Entailment Proofs in Separation Logic
• On global induction mechanisms in aμ-calculus with explicit approximations
• On the Proof Theory of Regular Fixed Points

Cited In (19)

• Uniform interpolation from cyclic proofs: the case of modal mu-calculus
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• From GTC to \textsc{Reset}: generating reset proof systems from cyclic proof systems
• Title not available (Why is that?)
• Coinduction in Flow: The Later Modality in Fibrations
• Cyclic hypersequent system for transitive closure logic
• NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC
• Title not available (Why is that?)
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Abstract cyclic proofs
• Non-well-founded deduction for induction and coinduction
• Integrating induction and coinduction via closure operators and proof cycles
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• Abstract cyclic proofs
• Cyclic implicit complexity
• Circular (Yet Sound) Proofs in Propositional Logic
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Proof systems for the modal \(\mu \)-calculus obtained by determinizing automata
• Title not available (Why is that?)

Uses Software

• Cyclist

This page was built for publication: Cyclic Arithmetic Is Equivalent to Peano Arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988374)