Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
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. Th...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2018-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4195/pdf |
| _version_ | 1827322819772416000 |
|---|---|
| author | Jörg Endrullis Helle Hvid Hansen Dimitri Hendriks Andrew Polonsky Alexandra Silva |
| author_facet | Jörg Endrullis Helle Hvid Hansen Dimitri Hendriks Andrew Polonsky Alexandra Silva |
| author_sort | Jörg Endrullis |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:00Z |
| format | Article |
| id | doaj.art-c71d6605d5d34964a525b7367f63d6ff |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:00Z |
| publishDate | 2018-01-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-c71d6605d5d34964a525b7367f63d6ff2024-03-08T09:53:24ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742018-01-01Volume 14, Issue 110.23638/LMCS-14(1:3)20184195Coinductive Foundations of Infinitary Rewriting and Infinitary Equational LogicJörg EndrullisHelle Hvid HansenDimitri HendriksAndrew PolonskyAlexandra SilvaWe 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.https://lmcs.episciences.org/4195/pdfcomputer science - logic in computer science |
| spellingShingle | Jörg Endrullis Helle Hvid Hansen Dimitri Hendriks Andrew Polonsky Alexandra Silva Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic Logical Methods in Computer Science computer science - logic in computer science |
| title | Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic |
| title_full | Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic |
| title_fullStr | Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic |
| title_full_unstemmed | Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic |
| title_short | Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic |
| title_sort | coinductive foundations of infinitary rewriting and infinitary equational logic |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/4195/pdf |
| work_keys_str_mv | AT jorgendrullis coinductivefoundationsofinfinitaryrewritingandinfinitaryequationallogic AT hellehvidhansen coinductivefoundationsofinfinitaryrewritingandinfinitaryequationallogic AT dimitrihendriks coinductivefoundationsofinfinitaryrewritingandinfinitaryequationallogic AT andrewpolonsky coinductivefoundationsofinfinitaryrewritingandinfinitaryequationallogic AT alexandrasilva coinductivefoundationsofinfinitaryrewritingandinfinitaryequationallogic |