非传递关系的不动点定理
摘要：在本论文中，我们开发了一个基于Isabelle/HOL的有序定点定理的库。我们保持我们的形式化尽可能的通用：我们重新证明了关于完全序的几个众所周知的结果，通常只需要反对称性或者吸引性，这是反对称性或传递性所蕴含的一种温和的条件。特别地，我们推广了各种确保完全关系上单调映射存在准定点的定理，并且证明了（准）定点集本身是完全的。这个结果推广并加强了Knaster-Tarski、Bourbaki-Witt、Kleene、Markowsky、Pataraia、Mashburn、Bhatta-George和Stouti-Maaden的定理。
作者：J\'er\'emy Dubut and Akihisa Yamada
论文ID：2009.13065
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22