Going Polymorphic - TH1 Reasoning for Leo-III

Alexander Steen, Max Wisniewski, Christoph Benzmüller – 2017

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.

Titel
Going Polymorphic - TH1 Reasoning for Leo-III
Verfasser
Alexander Steen, Max Wisniewski, Christoph Benzmüller
Verlag
EasyChair
Datum
2017-06
Erschienen in
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Kalpa Publications in Computing, Vol. 1, 2017
Größe oder Länge
13 pages