Going Polymorphic - TH1 Reasoning for Leo-III

Steen, Alexander; Wisniewski, Max; Benzmüller, Christoph

Reference : Going Polymorphic - TH1 Reasoning for Leo-III


	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/10993/33702

Title :	Going Polymorphic - TH1 Reasoning for Leo-III
Language :	English
Author, co-author :	Steen, Alexander [> >]
	Wisniewski, Max [> >]
	Benzmüller, Christoph [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
Publication date :	4-Jun-2017
Main document title :	IWIL Workshop and LPAR Short Presentations
Publisher :	EasyChair
Collection and collection volume :	Kalpa Publications in Computing, Volume 1
Pages :	13
Peer reviewed :	Yes
Audience :	International
City :	Maun, Botswana
Event name :	IWIL Workshop and LPAR Short Presentations
Event date :	7 May 2017
Event organizer :	Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov
Event place (city) :	Maun
Event country :	Botswana
Keywords :	[en] Polymorphism Automated Reasoning ; LEO Prover ; Higher Order Logic
Abstract :	[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.
Target :	Researchers ; Professionals ; Students
Permalink :	http://hdl.handle.net/10993/33702
Other URL :	http://www.easychair.org/publications/paper/346851
Commentary :	1

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	Going_Polymorphic_-_TH1_Reasoning_for_Leo-III.pdf		Publisher postprint	533.31 kB	View/Open

All documents in ORBi^lu are protected by a user license.

University of Luxembourg Library | Feedback | Legal notices