Polymorphism Automated Reasoning; LEO Prover; Higher Order Logic
Résumé :
[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.
BENZMÜLLER, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Going Polymorphic - TH1 Reasoning for Leo-III
Date de publication/diffusion :
04 juin 2017
Nom de la manifestation :
IWIL Workshop and LPAR Short Presentations
Organisateur de la manifestation :
Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov
