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

lmcs:4195 - Logical Methods in Computer Science, January 10, 2018, Volume 14, Issue 1
Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

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

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.


Source : oai:arXiv.org:1706.00677
DOI : 10.23638/LMCS-14(1:3)2018
Volume: Volume 14, Issue 1
Published on: January 10, 2018
Submitted on: January 10, 2018
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 265 times.
This article's PDF has been downloaded 113 times.