Pholi

座谈焦点

计算机科学座谈会基金会 - 2月24日至16日，数据室 - 陈列室（DHEG136E） - Sandgasse 36 Eg de Neville Hans：“与接口的部分高阶逻辑” 2024年2月12日| 09:30 h摘要此演示文稿是关于我要开发的数学证据的正式验证的计算。我使用了现有的验证系统（Coq，Holight，Isabelle和Mizar），但我认为还有改进的余地。pholi的意思是“具有接口的部分高阶逻辑”。它基于我在2014年开发的部分功能的3值逻辑。我想将此逻辑演变为用户友好的演算，以进行数学证明检查。为了做到这一点，必须添加高阶，用于类型定义的方法以及证明结构的方法。我花了一半的时间实施了第一个版本，并对结果感到失望。演算的缺陷使其有效无法使用。在2018年期间，我试图实施改进的版本，并得出结论，在我知道的每种编程语言中，实施逻辑都需要太多时间，包括功能语言。在2020-23期间，我从事实施逻辑的技术。去年，我取得了很大进步。i开发了一个编译器，该编译器会在C ++中自动生成递归数据结构。我相信实施问题现在已经完全解决。现在我想再次实施Pholi，但我不想重复以前的错误。我相信这种方法正在起作用。因此，我将在文本中编写证据，直到我对演算完全满意为止。在演讲中，我将展示如何在Pholi中发展标准自动机理论。尽管这些是使用众所周知的构造的简单证明，但是使用pholi看着它们的构造给出了基本问题的新观点：在字母表上定义单词的最佳方法是什么？一个人如何在单词上定义函数？一个人如何证明单词的存在？为了使非确定性的有限自动机确定性，需要一个子集结构，需要该子集构造。但是，对于计算机科学家来说，正确的集合理论是什么？计算机科学家需要多少集理论？