Unification of stratified second-order terms

We consider the problem of unifying a set of equations between second-order terms. Terms are constructed from function symbols, constant symbols and variables, and furthermore using monadic second-order variables that may stand for a term with one hole, and parametric terms. We consider stratified systems, where for every first-order and second-order variable, the string of second-order variables on the path from the root of a term to every occurrence of this variable is always the same. It is shown that unification of stratified second-order terms is decidable by describing a nondeterministic decision algorithm that eventually uses Makanin's algorithm for deciding the unifiability of word equations. As a generalization, we show that the method can be used as a unification procedure for non-stratified second-order systems, and describe conditions for termination in the general case.

Metadaten
Verfasserangaben:	Manfred Schmidt-Schauß ORCiD GND
URN:	urn:nbn:de:hebis:30-8884
URL:	http://www.ki.informatik.uni-frankfurt.de/papers/schauss/D-uni-SO-9-95.ps
Titel des übergeordneten Werkes (Englisch):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 1
Titel des übergeordneten Werkes (Deutsch):	Universität Frankfurt am Main. Fachbereich Informatik: Interner Bericht ; 94,12
Schriftenreihe (Bandnummer):	Interner Bericht / Fachbereich Informatik, Johann Wolfgang Goethe-Universität Frankfurt a.M. (94,12)
	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (1)
Verlag:	Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Verlagsort:	Frankfurt [am Main]
Dokumentart:	Arbeitspapier
Sprache:	Englisch
Jahr der Fertigstellung:	1994
Jahr der Erstveröffentlichung:	1994
Veröffentlichende Institution:	Universitätsbibliothek Johann Christian Senckenberg
Datum der Freischaltung:	12.05.2005
Seitenzahl:	39
Erste Seite:	1
Letzte Seite:	39
Quelle:	Internal report 12/94
HeBIS-PPN:	190002204
Institute:	Informatik und Mathematik / Informatik
DDC-Klassifikation:	0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):	Deutsches Urheberrecht

Open Access