Non-well-founded deduction for induction and coinduction
From MaRDI portal
Publication:2055840
DOI10.1007/978-3-030-79876-5_1OpenAlexW3181713287MaRDI QIDQ2055840
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_1
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
- Coinductive big-step operational semantics
- Cut-elimination for a logic with definitions and induction
- Universal coalgebra: A theory of systems
- Completeness for ancestral logic via a computationally-meaningful semantics
- A cut-free cyclic proof system for Kleene algebra
- Untersuchungen über das logische Schliessen. I
- Cut elimination for a logic with induction and co-induction
- 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
- A proof theory for model checking
- A formally verified compiler back-end
- Inductive and Coinductive Components of Corecursive Functions in Coq
- Truly Modular (Co)datatypes for Isabelle/HOL
- Circular Coinduction: A Proof Theoretical Foundation
- The power of parameterization in coinductive proof
- Ancestral Logic: A Proof Theoretical Study
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Cyclic Arithmetic Is Equivalent to Peano Arithmetic
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- Friends with Benefits
- Sequent calculi for induction and infinite descent
- Property-Directed Inference of Universal Invariants or Proving Their Absence
- 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
- Towards Completeness via Proof Search in the Linear Time μ-calculus
- Recursive subtyping revealed
- Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
- Non-well-founded Proof Theory of Transitive Closure Logic
- All-Path Reachability Logic
- Automated Cyclic Entailment Proofs in Separation Logic
- Towards automated reasoning in Herbrand structures
- One-Path Reachability Logic
- Practical coinduction
- Well-founded recursion with copatterns and sized types
- A Proof System for the Linear Time μ-Calculus
- Automated Reasoning with Analytic Tableaux and Related Methods
- Programming Languages and Systems
- Types for Proofs and Programs
- Expressive Logics for Coinductive Predicates
- Least and Greatest Fixed Points in Linear Logic
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Into the Infinite - Theory Exploration for Coinduction
