Integrating induction and coinduction via closure operators and proof cycles

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

Authors: Liron Cohen, Reuben N. S. Rowe 

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)

Cites Work

• CIRC: A Circular Coinductive Prover
• Idris, a general-purpose dependently typed programming language: Design and implementation
• CoCaml: functional programming with regular coinductive types
• Untersuchungen über das logische Schliessen. I
• Handbook of proof theory
• Universal coalgebra: A theory of systems
• Coalgebraic semantics for derivations in logic programming
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Fundamental properties of infinite trees
• Cut elimination for a logic with induction and co-induction
• Languages that Capture Complexity Classes
• The relative efficiency of propositional proof systems
• Circular coinduction: a proof theoretical foundation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Recursive subtyping revealed
• Sequent calculi for induction and infinite descent
• Title not available (Why is that?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Cut-elimination for a logic with definitions and induction
• Title not available (Why is that?)
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Title not available (Why is that?)
• Coinductive big-step operational semantics
• Least and Greatest Fixed Points in Linear Logic
• Finiteness is mu-ineffable
• Cyclic proofs of program termination in separation logic
• Title not available (Why is that?)
• Coinductive Logic Programming
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• A proof theory for model checking
• Completeness for ancestral logic via a computationally-meaningful semantics
• Ancestral Logic: A Proof Theoretical Study
• A coinductive framework for infinitary rewriting and equational reasoning
• Constructive completeness for the linear-time \(\mu \)-calculus
• Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
• Title not available (Why is that?)
• Cyclic arithmetic is equivalent to Peano arithmetic
• Infinitary proof theory: the multiplicative additive case
• Practical coinduction
• Well-founded recursion with copatterns and sized types
• Title not available (Why is that?)
• The middle ground-ancestral logic
• 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
• A homogeneous system for formal logic
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Stream differential equations: specification formats and solution methods

Cited In (6)

• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• Polarized subtyping
• Cyclic hypersequent system for transitive closure logic
• Non-well-founded deduction for induction and coinduction
• Induction, coinduction, and adjoints
• Cyclic proofs, hypersequents, and transitive closure logic

Uses Software

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

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

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