Chad E. Brown, Cezary Kaliszyk
Automated Reasoning – 11th International Joint Conference, IJCAR 2022, pp. 250-358, 2022.
pdf 
doi:10.1007/978-3-031-10769-6_21
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 10 s timeout Lash outperforms Satallax on a collection TH0 problems from the TPTP. We conclude with ideas for continuing the development of Lash.
BibTex
@inproceedings{cbck-ijcar22, author = {Chad E. Brown and Cezary Kaliszyk}, booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022}, doi = {10.1007/978-3-031-10769-6\_21}, editor = {Jasmin Blanchette and Laura Kov{\'{a}}cs and Dirk Pattinson}, pages = {350--358}, publisher = {Springer}, series = {LNCS}, title = {Lash 1.0 (System Description)}, url = {https://doi.org/10.1007/978-3-031-10769-6\_21}, volume = {13385}, year = {2022}}