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
Secondary volumes: Selected Papers of the 26th International Conference on Rewriting Techniques and Applications and the 13th International Conference on Typed Lambda Calculus and Applications (RTA and TLCA 2015)
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
  • Probabilistic Foundations for Networks; Funder: European Commission; Code: 679127

Classifications

Mathematics Subject Classification 20201
Sources:
  • [1] zbMATH Open.

Share and export

Consultation statistics

This page has been seen 3922 times.
This article's PDF has been downloaded 888 times.