# Lash 1.0 (System Description)

arXiv: https://arxiv.org/abs/2205.06640 · HTML: https://mlsanity.com/paper/2205.06640/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 May 2022.

## Built on by (most cited first, 4 of 4)

- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)
- [Translating SUMO-K to Higher-Order Set Theory](https://mlsanity.com/paper/2305.07903/) (2023)
- [Experiments with Choice in Dependently-Typed Higher-Order Logic](https://mlsanity.com/paper/2410.08874/) (2024)
- [Automated Strategy Invention for Confluence of Term Rewrite Systems](https://mlsanity.com/paper/2411.06409/) (2024)

## Abstract (arXiv)

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.