Lash 1.0（系统描述）
计算机科学中的逻辑
2022-05-16 v1
摘要
Lash 是一个高阶自动定理证明器，作为定理证明器 Satallax 的一个分支而创建。Satallax 的基本底层演算是一个基元表演算，其规则仅使用参与规则的项和公式的浅层信息。Lash 使用了重要的结构和运算的高效 C 语言新表示。最重要的是，Lash 使用了具有完美共享的（正规）项的 C 表示，以及正规化替换的 C 语言实现。我们描述了 Lash 与 Satallax 的不同之处，以及在使用类似标志设置时 Lash 相对于 Satallax 的性能提升。在 10 秒超时下，Lash 在来自 TPTP 的一组 TH0 问题上优于 Satallax。最后我们提出了继续开发 Lash 的思路。
引用
@article{arxiv.2205.06640,
title = {Lash 1.0 (System Description)},
author = {Chad E. Brown and Cezary Kaliszyk},
journal= {arXiv preprint arXiv:2205.06640},
year = {2022}
}