Cut elimination for a logic with induction and co-induction

DOI10.1016/J.JAL.2012.07.007zbMath1278.03086arXiv1009.6171OpenAlexW2141039045MaRDI QIDQ1948276

Alberto Momigliano, Alwen Tiu

Publication date: 2 May 2013

Published in: Journal of Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

cut eliminationsequent calculusproof theoryinductionco-inductionintuitionistic theory of types

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05)

Related Items (10)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Extracting Proofs from Tabled Proof Search ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Syntactic cut-elimination for a fragment of the modal mu-calculus ⋮ Non-well-founded deduction for induction and coinduction ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ A proof theory for model checking ⋮ Integrating induction and coinduction via closure operators and proof cycles

Uses Software

• HYBRID
• Tac
• Bedwyr

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Nominal abstraction
• Strong normalization property for second order linear logic
• Partial inductive definitions
• Encoding transition systems in sequent calculus
• Cut-elimination for a logic with definitions and induction
• A two-level logic approach to reasoning about computations
• Proof search specifications of bisimulation and modal logics for the π-calculus
• On the Proof Theory of Regular Fixed Points
• A framework for defining logics
• Mechanizing coinduction and corecursion in higher-order logic
• A logic programming language with lambda-abstraction, function variables, and simple unification
• A proof theory for generic judgments
• Foundations of Software Science and Computational Structures
• Types for Proofs and Programs
• Reasoning with higher-order abstract syntax in a logical framework
• Focused Inductive Theorem Proving
• Inductively defined types in the Calculus of Constructions
• Least and Greatest Fixed Points in Linear Logic
• Solution to a problem of Ono and Komori

This page was built for publication: Cut elimination for a logic with induction and co-induction