论文标题
睫毛1.0（系统描述）
Lash 1.0 (System Description)
论文作者
论文摘要
LASH是一种高阶自动定理供体式，作为定理供体satallax的叉子创建的。 Satallax的基本基础演算是一个地面彩票演算，其规则仅使用有关参与规则的术语和公式的浅信息。 Lash使用重要的结构和操作的新的，有效的C表示。最重要的是，LASH使用（正常）术语的C表示，完美共享以及C实施归一化替换。我们描述了睫毛与satallax不同的方式以及与类似标志设置一起使用时睫毛在satallax上的性能改善。有10秒的超时睫毛在TPTP中的收集问题上优于Satallax。我们以继续开发睫毛的想法结论。
Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules only use shallow information about the terms and formulas taking part in the rule. Lash uses new, efficient C representations of vital structures and operations. Most importantly, Lash uses a C representation of (normal) terms with perfect sharing along with a C implementation of normalizing substitutions. We describe the ways in which Lash differs from Satallax and the performance improvement of Lash over Satallax when used with analogous flag settings. With a 10s timeout Lash outperforms Satallax on a collection TH0 problems from the TPTP. We conclude with ideas for continuing the development of Lash.
