Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Proof Checking and Logic Programming Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

A Type-Theoretic Approach to Resolution

verfasst von : Peng Fu, Ekaterina Komendantskaya

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of program transformation that allows to transform logic programs in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

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




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

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




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel From Boolean Equalities to Constraints
Nächstes Kapitel A Typed Language for Events
Fußnoten
1
Extended version is available at both authors’ homepages.
 
Literatur
1.
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)CrossRefMATH
2.
Bertot, Y., Komendantskaya, E.: Inductive and coinductive components of corecursive functions in coq. Electron. Notes Theor. Comput. Sci. 203(5), 25–47 (2008)MathSciNetCrossRefMATH
3.
Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)MATH
4.
Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. ACM SIGPLAN Not. 46(9), 163–175 (2011)CrossRefMATH
5.
Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications, ICLP (2015)
6.
Jones, M.P.: Qualified Types: Theory and Practice. Cambridge University Press, Cambridge (2003)MATH
7.
Kleene, S.C.: Introduction to Metamathematics. North-Holland Publishing Company, New York (1952). Co-publisher: Wolters-Noordhoff; 8th revised ed.1980MATH
8.
Komendantskaya, E., Power, J., Schmidt, M.: Coalgebraic logic programming: from semantics to implementation. J. Log. Comput. (2014)
9.
Nilsson, U., Maluszynski, J.: Logic, Programming and Prolog. Wiley, Chichester (1990)MATH
10.
Terese.: Term rewriting systems. In: Bezem, M., Willem Klop, J., deVrijer, R. (eds.) Cambridge Tracts in Theoretical Computer Science, vol. 55. pp. xxii + 884. Cambridge University Press (2003)
11.
Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Symposium on Principles of Programming Languages, pp. 60–76. ACM (1989)
Metadaten
Titel
A Type-Theoretic Approach to Resolution
verfasst von
Peng Fu
Ekaterina Komendantskaya
Copyright-Jahr
2015
Buch
Logic-Based Program Synthesis and Transformation

Print ISBN: 978-3-319-27435-5

Electronic ISBN: 978-3-319-27436-2

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-27436-2_6

Premium Partner

    Bildnachweise