Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

 
 
DownloadE-Mail
  Encoding Monomorphic and Polymorphic Types

Blanchette, J. C., Böhme, S., Popescu, A., & Smallbone, N. (2016). Encoding Monomorphic and Polymorphic Types. doi:10.2168/LMCS-2014-1018.

Item is

Dateien

einblenden: Dateien
ausblenden: Dateien
:
arXiv:1609.08916.pdf (Preprint), 790KB
Name:
arXiv:1609.08916.pdf
Beschreibung:
File downloaded from arXiv at 2016-10-26 11:09
OA-Status:
Sichtbarkeit:
Öffentlich
MIME-Typ / Prüfsumme:
application/pdf / [MD5]
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Blanchette, Jasmin Christian1, Autor           
Böhme, Sascha2, Autor
Popescu, Andrei2, Autor
Smallbone, Nicholas2, Autor
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2External Organizations, ou_persistent22              

Inhalt

einblenden:
ausblenden:
Schlagwörter: Computer Science, Logic in Computer Science, cs.LO
 Zusammenfassung: Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2016-09-282016
 Publikationsstatus: Online veröffentlicht
 Seiten: LMCS-2014-1018
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: arXiv: 1609.08916
DOI: 10.2168/LMCS-2014-1018
URI: http://arxiv.org/abs/1609.08916
BibTex Citekey: Blanchette1609.08916
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: