Lash 1.0 (System Description)
Chad E. Brown, Cezary Kaliszyk

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Testing and Debugging Techniques · AI-based Problem Solving and Planning
