Non-well-founded deduction for induction and coinduction
From MaRDI portal
Publication:2055840
Recommendations
Cites work
- scientific article; zbMATH DE number 6680140 (Why is no real title available?)
- scientific article; zbMATH DE number 6115908 (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 4116521 (Why is no real title available?)
- scientific article; zbMATH DE number 2087442 (Why is no real title available?)
- scientific article; zbMATH DE number 3799616 (Why is no real title available?)
- scientific article; zbMATH DE number 7189131 (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 7155168 (Why is no real title available?)
- scientific article; zbMATH DE number 3365218 (Why is no real title available?)
- scientific article; zbMATH DE number 7649955 (Why is no real title available?)
- A Proof System for the Linear Time μ-Calculus
- A cut-free cyclic proof system for Kleene algebra
- A formally verified compiler back-end
- A logic for reasoning about generic judgments
- A proof theory for model checking
- Ancestral Logic: A Proof Theoretical Study
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automated cyclic entailment proofs in separation logic
- Automatically verifying temporal properties of pointer programs with cyclic proof
- CIRC: A Circular Coinductive Prover
- Circular coinduction: a proof theoretical foundation
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- Coinductive big-step operational semantics
- Coinductive foundations of infinitary rewriting and infinitary equational logic
- 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
- Expressive Logics for Coinductive Predicates
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Inductive and coinductive components of corecursive functions in Coq
- Infinitary proof theory: the multiplicative additive case
- Integrating induction and coinduction via closure operators and proof cycles
- Into the Infinite - Theory Exploration for Coinduction
- Languages that Capture Complexity Classes
- Non-well-founded proof theory of transitive closure logic
- One-path reachability logic
- PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
- Practical coinduction
- Programming Languages and Systems
- Property-directed inference of universal invariants or proving their absence
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
- Recursive subtyping revealed
- Sequent calculi for induction and infinite descent
- The middle ground-ancestral logic
- The power of parameterization in coinductive proof
- Towards automated reasoning in Herbrand structures
- Towards completeness via proof search in the linear time \(\mu\)-calculus: the case of Büchi inclusions
- Truly modular (co)datatypes for Isabelle/HOL
- Types for Proofs and Programs
- 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
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)
