| Reference : Leo-III 1.5 |
| Computer developments : Software | |||
| Engineering, computing & technology : Computer science | |||
| http://hdl.handle.net/10993/45464 | |||
| Leo-III 1.5 | |
| English | |
Steen, Alexander  [University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) >] | |
| Jul-2020 | |
| 2016 | |
| [en] Automated Theorem Proving ; Higher-Order Logic ; Automated Reasoning | |
| [en] Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external (mostly first-order) theorem provers for increased performance. Nevertheless, Leo-III can also be used as a stand-alone prover without employing any external cooperation.
In addition for its HOL reasoning capabilities, Leo-III supports reasoning in many higher-order quantified modal logics. | |
| Deutsche Forschungsgemeinschaft (DFG) | |
| Researchers ; Students | |
| http://hdl.handle.net/10993/45464 | |
| 10.5281/zenodo.4435995 | |
| https://github.com/leoprover/Leo-III | |
| Leo-III is developed at Freie Universität Berlin and the University of Luxembourg. From 2014 - 2018, it was supported by the German National Research Foundation (DFG) under project BE 2501/11-1 (Leo-III). | |
| Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with additional ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external (mostly first-order) theorem provers for increased performance. Nevertheless, Leo-III can also be used as a stand-alone prover without employing any external cooperation. | |
| 1.5 |
There is no file associated with this reference.
All documents in ORBilu are protected by a user license.
