Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-39492
Titel: A Many-Sorted Calculus with Polymorphic Functions Based On Resolution And Paramodulation
VerfasserIn: Schmidt-Schauß, Manfred
Sprache: Englisch
Erscheinungsjahr: 1985
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 000 Allgemeines, Wissenschaft
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: A many-sorted first order calculus, called ΣRP, whose well formed formulas are sorted (typed) clauses and whose inference rules are factorization, resolution, paramodulation and weakening is extended to a many sorted calculus ΣRP* with polymorphic functions (overloading). It is assumed that the sort structure is a finite partially ordered set with a greatest element. It is shown, that this extended calculus is sound and complete, provided the functional reflexivity axioms are present. It is also shown, that unification of terms containing polymorphic functions is in general finitary, i.e. the set of most general unifiers may contain more than one element, but at most finitely many. We give a natural condition for the signature (the sort structure), such that the set of most general unifiers is always at most a singleton provided this condition holds.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-394925
hdl:20.500.11880/35658
http://dx.doi.org/10.22028/D291-39492
Schriftenreihe: Memo SEKI : SEKI-Projekt / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI
Band: 85,2 KL
Datum des Eintrags: 17-Apr-2023
Bemerkung/Hinweis: In der GND existiert kein Normdatensatz für die Person, die sie eindeutig als solche identifiziert. Alternative oder damit in Verbindung stehende Schreibweise(n): Schmidt-Schauss, Manfred.
Fakultät: SE - Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professur: SE - Sonstige
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.