Abstract
LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate with the first-order automated theorem provers E, SPASS, and Vampire. The improved performance of LEO-II, especially in comparison to its predecessor LEO, is due to several novel features including the exploitation of term sharing and term indexing techniques, support for primitive equality reasoning, and improved heuristics at the calculus level. LEO-II is implemented in Objective Caml and its problem representation language is the new TPTP THF language. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Benzmüller, C., Paulson, L. C., Theiss, F., & Fietzke, A. (2008). LEO-II - A cooperative automatic theorem prover for classical higher-order logic (system description). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 162–170). https://doi.org/10.1007/978-3-540-71070-7_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
