基于常复合关系半群与恶魔格运算的恶魔格与半格形式化
计算机科学中的逻辑
2021-05-17 v1 逻辑
摘要
关系代数及其归约系统为我们提供了推理非确定性程序及其部分正确性的有力工具。为建模由恶魔控制非确定性的机器行为而引入的恶魔演算,也将此类推理扩展到了总正确性。我们使用具有常复合和恶魔格运算的半群,形式化了关于非确定性程序总正确性的关系推理框架。我们证明了可表示恶魔连接半群类不是有限可公理化的,且恶魔交半群的代表类对其有限成员不具有有限表示性质。对于格半群(具有复合、恶魔并和恶魔交),我们证明了有限代数的表示问题是不可判定的,此外有限表示问题也是不可判定的。由此可知表示类不是有限可公理化的,且有限表示性质不成立。
引用
@article{arxiv.2105.06787,
title = {Demonic Lattices and Semilattices in Relational Semigroups with Ordinary Composition},
author = {Robin Hirsch and Jaš Šemrl},
journal= {arXiv preprint arXiv:2105.06787},
year = {2021}
}