面向一个集合的量词自由片段的可验证表格证明器
摘要：使用Isabelle/HOL，我们验证了多层级带有单例的（简称为MLSS）最先进的决策过程，该过程是一个无全称量词的集合论片段。我们形式化它的语法和语义，以及一个对它完备而完全的表格推理。我们还提供了一个决策过程的可执行规范，该规范详尽地应用了表格推理的规则，并证明了其终止性。此外，我们还扩展了该推理表达式，增加了一个轻量级的类型系统，为将该过程整合到Isabelle/HOL中铺平道路。
作者：Lukas Stevens
论文ID：2209.14133
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-04