Integrating induction and coinduction via closure operators and proof cycles

DOI10.1007/978-3-030-51074-9_21OpenAlexW3039514567MaRDI QIDQ2096458

Reuben N. S. Rowe, Liron Cohen

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_21

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Cyclic hypersequent system for transitive closure logic ⋮ Polarized subtyping ⋮ Non-well-founded deduction for induction and coinduction ⋮ Cyclic proofs, hypersequents, and transitive closure logic

Uses Software

• CIRC
• Nuprl
• Agda
• Irdis
• CoALP
• Idris
• CoCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Coinductive big-step operational semantics
• Fundamental properties of infinite trees
• Finiteness is mu-ineffable
• Handbook of proof theory
• Cut-elimination for a logic with definitions and induction
• Universal coalgebra: A theory of systems
• Completeness for ancestral logic via a computationally-meaningful semantics
• Untersuchungen über das logische Schliessen. I
• Cut elimination for a logic with induction and co-induction
• The middle ground-ancestral logic
• A proof theory for model checking
• Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)
• Circular Coinduction: A Proof Theoretical Foundation
• Ancestral Logic: A Proof Theoretical Study
• Cyclic Arithmetic Is Equivalent to Peano Arithmetic
• Coalgebraic Semantics for Derivations in Logic Programming
• Sequent calculi for induction and infinite descent
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Cyclic proofs of program termination in separation logic
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• CIRC: A Circular Coinductive Prover
• Languages that Capture Complexity Classes
• The relative efficiency of propositional proof systems
• CoCaml: Functional Programming with Regular Coinductive Types
• Recursive subtyping revealed
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• Non-well-founded Proof Theory of Transitive Closure Logic
• Towards automated reasoning in Herbrand structures
• Practical coinduction
• Well-founded recursion with copatterns and sized types
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Coinductive Logic Programming
• A homogeneous system for formal logic
• Least and Greatest Fixed Points in Linear Logic
• Automatically verifying temporal properties of pointer programs with cyclic proof

This page was built for publication: Integrating induction and coinduction via closure operators and proof cycles