Lash 1.0 (System Description)

TL;DR

Lash 1.0 is an improved higher-order theorem prover based on Satallax, utilizing efficient C representations and sharing techniques to enhance performance on TH0 problems within a 10-second timeout.

Contribution

Lash introduces new C-based data structures and sharing methods that significantly improve performance over Satallax in higher-order theorem proving.

Findings

Lash outperforms Satallax on TPTP TH0 problems within 10 seconds.

Use of C representations and sharing techniques enhances proof search efficiency.

Performance gains demonstrate the effectiveness of Lash's design improvements.

Abstract

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.