scientific article; zbMATH DE number 7089071

MaRDI QIDQ5227521

Stefano Berardi, Makoto Tatsuta

Publication date: 6 August 2019

Full work available at URL: https://arxiv.org/abs/1712.09603

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

proof theoryHenkin modelsinductive definitionscyclic proofBrotherston-Simpson conjectureMartin-Löf's system of inductive definitions

Mathematics Subject Classification ID

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

Related Items (3)

Uniform interpolation from cyclic proofs: the case of modal mu-calculus ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Induction and Skolemization in saturation theorem proving

Uses Software

• Cyclist

Cites Work

• Unnamed Item
• 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
• A general framework to build contextual cover set induction provers

This page was built for publication: