Non-well-founded deduction for induction and coinduction

DOI10.1007/978-3-030-79876-5_1OpenAlexW3181713287MaRDI QIDQ2055840

Liron Cohen

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_1

Mathematics Subject Classification ID

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