Reference : Leo-III Version 1.1 (System description)
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Computational Sciences
http://hdl.handle.net/10993/33703
Leo-III Version 1.1 (System description)
English
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
Steen, Alexander [> >]
Wisniewski, Max [> >]
4-Jun-2017
IWIL Workshop and LPAR Short Presentations
EasyChair
Kalpa Publications in Computing, Volume 1
16
Yes
International
Manchester
UK
IWIL Workshop and LPAR Short Presentations
7 May 2017
Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov
Maun
Botswana
[en] Higher Order Logic ; LEO Prover ; Automated Theorem Proving
[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 first-order theorem provers.
Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use.
Researchers ; Professionals ; Students
http://hdl.handle.net/10993/33703
http://www.easychair.org/publications/paper/342979
1

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Leo-III_Version_1.1_-System_description.pdfPublisher postprint768.63 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.