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 ma
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.
show moreshow less

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
Author:Manfred Schmidt-Schauß
URN:urn:nbn:de:hebis:30-8884
Series (Serial Number):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (01)
Publisher:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Place of publication:Frankfurt [am Main]
Document Type:Working Paper
Language:English
Date of Publication (online):2005/05/12
Year of first Publication:1994
Publishing Institution:Univ.-Bibliothek Frankfurt am Main
Release Date:2005/05/12
Source:Internal report 12/94
HeBIS PPN:190002204
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License Logo Veröffentlichungsvertrag für Publikationen

$Rev: 11761 $