LEO-I und LEO-II haben internationale Anerkennung erfahren als sehr erfolgreiche automatische Beweiser für klassische Logik höherer Stufe. In LEO-I wurde erstmals eine  primitive Behandlung (im Gegensatz zur axiomatischen Behandlung) der Extensionalitätsprinzipien erreicht. Neu war auch die Kooperation mit externen Beweisern (wie z.B. dem erststufigen Beweiser E) in einer flexiblen, agentenbasierten Architektur. Die Implementirung von LEO-II hatte signifikanten Einfluss auf die parallele Entwicklung der neuen TPTP THF Infrastruktur  für typisierte Logiken höherer Stufe.  Diese Infrastruktur führte zu enormen Verbesserungen in höherstufigen Beweisern (z.B. in den automatischen Beweisern ISABELLE/HOL und TPS) und zu Neuentwicklungen im Gebiet (wie z.B. dem Beweiser Satallax). LEO-II gewann den internationalen CASC Beweiserwettbewerb in 2010 und wird zur Zeit in den interaktiven Beweisassistenten ISABELLE/HOL integriert.

In diesem Punkt möchten wir LEO-II überführen in einen Beweiser, der auf geordneter Paramodulation/Superposition basiert.

Diese Änderungen an LEO-II sind signifikant in Theorie und Praxis. Das resultierende System, - bezeichnet als LEO-III - wird der Integrierbarkeit mit anderen Systemen eine besondere Bedeutung beimessen.