Non-well-founded deduction for induction and coinduction
From MaRDI portal
Publication:2055840
DOI10.1007/978-3-030-79876-5_1OpenAlexW3181713287MaRDI QIDQ2055840FDOQ2055840
Authors: Liron Cohen 
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_1
Recommendations
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- CIRC: A Circular Coinductive Prover
- The power of parameterization in coinductive proof
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Untersuchungen über das logische Schliessen. I
- Universal coalgebra: A theory of systems
- Inductive and coinductive components of corecursive functions in Coq
- Programming Languages and Systems
- Cut elimination for a logic with induction and co-induction
- Languages that Capture Complexity Classes
- 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?)
- Title not available (Why is that?)
- Cut-elimination for a logic with definitions and induction
- Types for Proofs and Programs
- Title not available (Why is that?)
- A formally verified compiler back-end
- Title not available (Why is that?)
- Title not available (Why is that?)
- One-path reachability logic
- Coinductive big-step operational semantics
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
- Title not available (Why is that?)
- Truly modular (co)datatypes for Isabelle/HOL
- Cyclic proofs of program termination in separation logic
- Title not available (Why is that?)
- Into the Infinite - Theory Exploration for Coinduction
- Title not available (Why is that?)
- A Proof System for the Linear Time μ-Calculus
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- A proof theory for model checking
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Completeness for ancestral logic via a computationally-meaningful semantics
- A cut-free cyclic proof system for Kleene algebra
- Ancestral Logic: A Proof Theoretical Study
- Automated Reasoning with Analytic Tableaux and Related Methods
- Constructive completeness for the linear-time \(\mu \)-calculus
- Expressive Logics for Coinductive Predicates
- Title not available (Why is that?)
- Cyclic arithmetic is equivalent to Peano arithmetic
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- Automated cyclic entailment proofs in separation logic
- Infinitary proof theory: the multiplicative additive case
- Towards completeness via proof search in the linear time \(\mu\)-calculus: the case of Büchi inclusions
- A logic for reasoning about generic judgments
- Practical coinduction
- Well-founded recursion with copatterns and sized types
- Title not available (Why is that?)
- The middle ground-ancestral logic
- Integrating induction and coinduction via closure operators and proof cycles
- PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
- Property-directed inference of universal invariants or proving their absence
- Coinductive foundations of infinitary rewriting and infinitary equational logic
- Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
- Non-well-founded proof theory of transitive closure logic
- Title not available (Why is that?)
- Towards automated reasoning in Herbrand structures
- Title not available (Why is that?)
- Automatically verifying temporal properties of pointer programs with cyclic proof
This page was built for publication: Non-well-founded deduction for induction and coinduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055840)
