使用遗传有限集的有限自动机形式化
形式语言与自动机理论
2015-05-08 v1 计算机科学中的逻辑
摘要
遗传有限（HF）集合论提供了一个标准的集合全域，但不包含无限集。其效用通过正则语言和有限自动机理论的形式化得到展示，包括 Myhill-Nerode 定理和 Brzozowski 最小化算法。自动机的状态是 HF 集，可能通过积、和、幂集及类似运算构造。
引用
@article{arxiv.1505.01662,
title = {A Formalisation of Finite Automata using Hereditarily Finite Sets},
author = {Lawrence C. Paulson},
journal= {arXiv preprint arXiv:1505.01662},
year = {2015}
}
备注
Accepted to CADE-25 (International Conference on Automated Deduction), Berlin, August 2015