Cargando…

Integrating Induction and Coinduction via Closure Operators and Proof Cycles

Coinductive reasoning about infinitary data structures has many applications in computer science. Nonetheless developing natural proof systems (especially ones amenable to automation) for reasoning about coinductive data remains a challenge. This paper presents a minimal, generic formal framework th...

Descripción completa

Detalles Bibliográficos
Autores principales: Cohen, Liron, Rowe, Reuben N. S.
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324239/
http://dx.doi.org/10.1007/978-3-030-51074-9_21