Lash swMATH ID: 43905 Software Authors: Brown, Chad E.; Kaliszyk, Cezary Description: Lash 1.0 (system description). 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 10 s timeout Lash outperforms Satallax on a collection TH0 problems from the TPTP. We conclude with ideas for continuing the development of Lash. Homepage: https://arxiv.org/abs/2205.06640 Keywords: higher-order logic; automated reasoning; TPTP; arXiv_cs.LO Related Software: TPS; Satallax; TPTP Cited in: 1 Document Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Lash 1.0 (system description). Zbl 07628197Brown, Chad E.; Kaliszyk, Cezary 2022 Cited by 2 Authors 1 Brown, Chad Edward 1 Kaliszyk, Cezary Cited in 0 Serials Cited in 1 Field 1 Computer science (68-XX) Citations by Year