Lash 1.0 (system description)

DOI10.1007/978-3-031-10769-6_21MaRDI QIDQ2104521zbMATH OpenOpenAlexFDO

Authors Cezary Kaliszyk, Chad E. Brown

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2205.06640

zbMATH Keywords

automated reasoninghigher-order logicTPTP

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The system LD
• System description: E 1.8
• scientific article; zbMATH DE number 1890626
• System Description: Spass Version 3.0
• scientific article; zbMATH DE number 1614703
• scientific article; zbMATH DE number 2090306
• scientific article; zbMATH DE number 1765682
• System description: GAPT 2.0

Cites work

• A combinator-based superposition calculus for higher-order logic
• Analytic tableaux for higher-order logic with choice
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• Extended First-Order Logic
• Extensional higher-order paramodulation in Leo-III
• Internal guidance for Satallax
• Making higher-order superposition work
• Satallax: An Automatic Higher-Order Prover
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• TPS: A theorem-proving system for classical type theory

Cited in

(9)

• Lash
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Translating SUMO-K to Higher-Order Set Theory
• Extending a high-performance prover to higher-order logic
• Solving hard Mizar problems with instantiation and strategy invention
• The dependently typed higher-order form for the TPTP world
• Hammering higher order set theory
• Experiments with choice in dependently-typed higher-order logic
• Tableaux for automated reasoning in dependently-typed higher-order logic

Describes a project that uses

Uses Software

• TPTP
• Satallax
• TPS
• Leo-III

This page was built for publication: Lash 1.0 (system description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104521)