Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

04.06.2018

From Types to Sets by Local Type Definition in Higher-Order Logic

Zeitschrift:
Journal of Automated Reasoning
Autoren:
Ondřej Kunčar, Andrei Popescu
Wichtige Hinweise
This is the extended, journal version of the conference paper [1], submitted to the JAR special issue dedicated to ITP 2016.

Abstract

Types in higher-order logic (HOL) are naturally interpreted as nonempty sets. This intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We propose a more expressive type definition rule that addresses the limitation and we prove its consistency. This higher expressive power opens the opportunity for a HOL tool that relativizes type-based statements to more flexible set-based variants in a principled way. We also address particularities of Isabelle/HOL and show how to perform the relativization in the presence of type classes.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit dem Kombi-Abo erhalten Sie vollen Zugriff auf über 1,8 Mio. Dokumente aus mehr als 61.000 Fachbüchern und rund 500 Fachzeitschriften aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit dem Wirtschafts-Abo erhalten Sie Zugriff auf über 1 Mio. Dokumente aus mehr als 45.000 Fachbüchern und 300 Fachzeitschriften aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit dem Technik-Abo erhalten Sie Zugriff auf über 1 Mio. Dokumente aus mehr als 40.000 Fachbüchern und 300 Fachzeitschriften aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Premium Partner

Neuer Inhalt

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Product Lifecycle Management im Konzernumfeld – Herausforderungen, Lösungsansätze und Handlungsempfehlungen

Für produzierende Unternehmen hat sich Product Lifecycle Management in den letzten Jahrzehnten in wachsendem Maße zu einem strategisch wichtigen Ansatz entwickelt. Forciert durch steigende Effektivitäts- und Effizienzanforderungen stellen viele Unternehmen ihre Product Lifecycle Management-Prozesse und -Informationssysteme auf den Prüfstand. Der vorliegende Beitrag beschreibt entlang eines etablierten Analyseframeworks Herausforderungen und Lösungsansätze im Product Lifecycle Management im Konzernumfeld.
Jetzt gratis downloaden!

Bildnachweise