de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt

# Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

#### $\forall\exists^\ast$-Equational Theory of Context Unification is $\Pi_1^0$-Hard

##### MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45677

Vorobyov,  Sergei
Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

##### Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
##### Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
##### Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
##### Zitation

Vorobyov, S. (1998). $\forall\exists^\ast$-Equational Theory of Context Unification is $\Pi_1^0$-Hard. In L. Brim, J. Gruska, & J. Zlatuska (Eds.), Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS-98) (pp. 597-606). Berlin, Germany: Springer.

\begin{abstract} Context unification is a particular case of second-order unification, where all second-order variables are \emph{unary} and only \emph{linear} functions are sought for as solutions. Its decidability is an open problem. We present the simplest (currently known) undecidable quantified fragment of the theory of \emph{context unification} by showing that for every signature containing a $\geq\!2$-ary symbol one can construct a \emph{context equation} ${\mathcal E}\,(p,r,\overline{F},\overline{w})$ with parameter $p$, first-order variables $r$, $\overline{w}$, and context variables $\overline{F}$ such that the set of true sentences of the form $\forall r\;\exists\;\overline{F}\;\exists\;\overline{w}\;\; {\mathcal E}(p,r,\overline{F},\overline{w})$ is $\Pi_1^0$-hard (i.e., every co-r.e. set is many-one reducible to it), as $p$ ranges over finite words of a binary alphabet. Moreover, the existential prefix above contains just 5 context and 3 first-order variables. \end{abstract}