Coaxioms: flexible coinductive definitions by inference systems
We introduce a generalized notion of inference system to support more flexible interpretations of recursive definitions. Besides axioms and inference rules with the usual meaning, we allow also coaxioms, which are, intuitively, axioms which can only be applied "at infinite depth" in a proo...
Main Author: | Francesco Dagnino |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2020-02-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/4745/pdf |
Similar Items
-
General Recursion via Coinductive Types
by: Venanzio Capretta
Published: (2005-07-01) -
Applications of Metric Coinduction
by: Dexter Kozen, et al.
Published: (2009-09-01) -
Coinductive Proof Principles for Stochastic Processes
by: Dexter Kozen
Published: (2007-11-01) -
Stone-Type Dualities for Separation Logics
by: Simon Docherty, et al.
Published: (2019-03-01) -
Generic Trace Semantics via Coinduction
by: Ichiro Hasuo, et al.
Published: (2007-11-01)