Integrating induction and coinduction via closure operators and proof cycles

DOI10.1007/978-3-030-51074-9_21MaRDI QIDQ2096458zbMATH OpenOpenAlexFDO

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

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

Cited in

(6)

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

Describes a project that uses

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)