Non-well-founded deduction for induction and coinduction
type: Item
instance of: scholarly article
title: Non-well-founded deduction for induction and coinduction
DOI: 10.1007/978-3-030-79876-5_1
author: Liron Cohen
publication date: 2021-12-01T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437069
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 1
OpenAlex ID: W3181713287
cites work: Well-founded recursion with copatterns and sized types
cites work: Q5144634
cites work: Q5875411
cites work: Least and Greatest Fixed Points in Linear Logic
cites work: Q5278431
cites work: Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
cites work: Programming Languages and Systems
cites work: Inductive and coinductive components of corecursive functions in Coq
cites work: Friends with Benefits
cites work: Truly Modular (Co)datatypes for Isabelle/HOL
cites work: Automated Reasoning with Analytic Tableaux and Related Methods
cites work: Formalised Inductive Reasoning in the Logic of Bunched Implications
cites work: Cyclic proofs of program termination in separation logic
cites work: Automated Cyclic Entailment Proofs in Separation Logic
cites work: Sequent calculi for induction and infinite descent
cites work: Q4960258
cites work: Completeness for ancestral logic via a computationally-meaningful semantics
cites work: Ancestral Logic: A Proof Theoretical Study
cites work: The middle ground-ancestral logic
cites work: Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
cites work: Integrating induction and coinduction via closure operators and proof cycles
cites work: Non-well-founded Proof Theory of Transitive Closure Logic
cites work: Towards automated reasoning in Herbrand structures
cites work: Q5208872
cites work: A cut-free cyclic proof system for Kleene algebra
cites work: Q5079743
cites work: A Proof System for the Linear Time μ-Calculus
cites work: Q5144621
cites work: Towards Completeness via Proof Search in the Linear Time μ-calculus
cites work: Into the Infinite - Theory Exploration for Coinduction
cites work: Q4600775
cites work: Q4731182
cites work: Q2958526
cites work: Recursive subtyping revealed
cites work: Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
cites work: Untersuchungen über das logische Schliessen. I
cites work: A proof theory for model checking
cites work: The power of parameterization in coinductive proof
cites work: Languages that Capture Complexity Classes
cites work: Q4355684
cites work: Property-Directed Inference of Universal Invariants or Proving Their Absence
cites work: Q4744245
cites work: Practical coinduction
cites work: Expressive Logics for Coinductive Predicates
cites work: A formally verified compiler back-end
cites work: Coinductive big-step operational semantics
cites work: CIRC: A Circular Coinductive Prover
cites work: Q5638283
cites work: Cut-elimination for a logic with definitions and induction
cites work: Types for Proofs and Programs
cites work: PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
cites work: One-Path Reachability Logic
cites work: Circular Coinduction: A Proof Theoretical Foundation
cites work: Universal coalgebra: A theory of systems
cites work: Q3145858
cites work: Q4738237
cites work: Q4001345
cites work: Cyclic Arithmetic Is Equivalent to Peano Arithmetic
cites work: Q4417874
cites work: All-Path Reachability Logic
cites work: Automatically verifying temporal properties of pointer programs with cyclic proof
cites work: A logic for reasoning about generic judgments
cites work: Cut elimination for a logic with induction and co-induction
cites work: Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
description: scientific article; zbMATH DE number 7437069