Reference : Going Polymorphic - TH1 Reasoning for Leo-III
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/33702
Going Polymorphic - TH1 Reasoning for Leo-III
English
Steen, Alexander [> >]
Wisniewski, Max [> >]
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
4-Jun-2017
IWIL Workshop and LPAR Short Presentations
EasyChair
Kalpa Publications in Computing, Volume 1
13
Yes
International
Maun, Botswana
IWIL Workshop and LPAR Short Presentations
7 May 2017
Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov
Maun
Botswana
[en] Polymorphism Automated Reasoning ; LEO Prover ; Higher Order Logic
[en] While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and therefore do not allow such flexibility. In this paper, we present modifications to the higher-order automated theorem prover Leo-III for turning it into a reasoning system for rank-1 polymorphic HOL.
To that end, a polymorphic version of HOL and a suitable paramodulation-based calculus are sketched. The implementation is evaluated using a set of polymorphic TPTP THF problems.
Researchers ; Professionals ; Students
http://hdl.handle.net/10993/33702
http://www.easychair.org/publications/paper/346851
1

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Going_Polymorphic_-_TH1_Reasoning_for_Leo-III.pdfPublisher postprint533.31 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.