论文标题
迈向无量词理论片段的经过验证的图表权
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
论文作者
论文摘要
使用Isabelle/HOL，我们使用Singleton（简称MLSS）验证了多级三段式的最新决策程序，这是集合理论的无量词片段。我们将其语法和语义以及声音和完整的彩色演算形式化。我们还提供了可执行的规范，该规范详尽地应用了微积分的规则并证明其终止。此外，我们使用轻质类型的系统扩展了微积分，该系统为将过程集成到Isabelle/Hol中铺平了道路。
Using Isabelle/HOL, we verify the state-of-the-art decision procedure for multi-level syllogistic with singleton (MLSS for short), which is a quantifier-free fragment of set theory. We formalise its syntax and semantics as well as a sound and complete tableau calculus for it. We also provide an executable specification of a decision procedure that exhaustively applies the rules of the calculus and prove its termination. Furthermore, we extend the calculus with a lightweight type system that paves the way for an integration of the procedure into Isabelle/HOL.
