Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

Jörg Endrullis; Helle Hvid Hansen; Dimitri Hendriks; Andrew Polonsky; Alexandra Silva

doi:10.23638/LMCS-14(1:3)2018

Jörg Endrullis ; Helle Hvid Hansen ; Dimitri Hendriks ; Andrew Polonsky ; Alexandra Silva - Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

lmcs:4195 - Logical Methods in Computer Science, January 10, 2018, Volume 14, Issue 1 - https://doi.org/10.23638/LMCS-14(1:3)2018

Coinductive Foundations of Infinitary Rewriting and Infinitary Equational LogicArticle

Authors: Jörg Endrullis ; Helle Hvid Hansen ; Dimitri Hendriks ; Andrew Polonsky ; Alexandra Silva

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence.
This makes the framework especially suitable for formalizations in theorem provers.

Comment: arXiv admin note: substantial text overlap with arXiv:1505.01128, arXiv:1306.6224

https://doi.org/10.23638/LMCS-14(1:3)2018

Source: arXiv.org:1706.00677

Volume: Volume 14, Issue 1

Published on: January 10, 2018

Imported on: January 10, 2018

Keywords: Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph