|
Abstract : |
There is a close relationship between word unification and second-order unification. This similarity has been exploited for instance for proving decidability of monadic secondorder unification. Word unification can be easily decided by transformation rules (similar to the ones applied in higher-order unification procedures) when variables are restricted to occur at most twice. Hence a well-known open question was the decidability of secondorder unification under this same restriction. Here we answer this question negatively by reducing (a variant of) simultaneous rigid E-unification to it. This reduction is in some sense reversible, providing decidability results for cases when rigid E-unification is decidable. This happens, for example, for one-variable problems where the variable occurs at most twice (because rigid E-unification is decidable for just one equation). We also prove decidability when no variable occurs more than once, hence significantly narrowing the gap between decidable and undecidable second-order unification problems with variable occurrence restrictions., |
