无穷重写与无穷等式逻辑的余归纳基础
计算机科学中的逻辑
2019-03-14 v2
摘要
我们提出了一个余归纳框架，用于以统一、余归纳的方式定义和推理等式逻辑与项重写的无穷类比。该框架捕获了任意序数长度的重写序列，但既不需要序数，也不需要度量收敛。这使得该框架特别适用于定理证明器中的形式化。
引用
@article{arxiv.1706.00677,
title = {Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic},
author = {Jörg Endrullis and Helle Hvid Hansen and Dimitri Hendriks and Andrew Polonsky and Alexandra Silva},
journal= {arXiv preprint arXiv:1706.00677},
year = {2019}
}
备注
arXiv admin note: substantial text overlap with arXiv:1505.01128, arXiv:1306.6224