Subject: Rewriting383---rigid_E_unification

Simultaneous rigid E-unification is a basis for adding equality to     
extension procedures, like the tableau method, the connection (mating) 
method and model elimination. Since its formulation in 1987, there were
several faulty proofs of its decidability. In our recent technical
reports (one of them is joint with Yu.Matiyasevich) we proved the undecidability
of the general problem and established some connections of special cases
of this problem with well-known problems: diophantine equations,
word equations and semi-unification.

The reports (nn. 104 and 105) are available by WWW at
http://www.csd.uu.se/~thomasl/reports.html and by anonymous ftp at ftp.csd.uu.se
in the directory pub/papers/reports as 0104.ps.gz and 0105.ps.gz.

The abstracts are enclosed,
Anatoli Degtyarev,
Andrei Voronkov.

-----------------------------------------------

          Simultaneous Rigid $E$-Unification is not so Simple

                           Anatoli Degtyarev
                          Yuri Matiyasevich
                           Andrei Voronkov

        Simultaneous rigid $E$-unification has been introduced in the
        area of theorem proving with equality. It is used in {\em
        extension procedures,\/} like the tableau method or the
        connection method. Some articles in this area assume
        the existence of an algorithm for simultaneous rigid
        $E$-unification. There were several faulty proofs of the
        decidability of this problem.

        In this article we prove several results about the simultaneous
        rigid $E$-unification. Two results are reductions of known
        problems to simultaneous rigid $E$-unification. Both these
        problems are very hard. The word equation solving (unification
        under associativity) is reduced to the monadic case of
        simultaneous rigid $E$-unification.  The variable-bounded
        semi-unification problem is reduced to the general simultaneous
        rigid $E$-unification.  The word equation problem used in the
        first reduction is known to be decidable, but the decidability
        result is extremely non-trivial. As for the variable-bounded
        semi-unification, its decidability is not even known.

        We also prove that a special case of simultaneous rigid
        $E$-unification with one unary function symbol is decidable.
        This is shown by reducing it to the Diophantine problem for
        addition and divisibility whose decidability is known. The
        technique we use is a combination of a technique of the number
        theory and a technique of the theory of rewrite systems.

---------------------------------------------------

           Simultaneous Rigid $E$-Unification is Undecidable

                           Anatoli Degtyarev
                           Andrei Voronkov

        Simultaneous rigid $E$-unification has been introduced in the
        area of theorem proving with equality. It is used in {\em
        extension procedures,\/} like the tableau method or the
        connection method. Many articles in this area assume the
        existence of an algorithm for simultaneous rigid
        $E$-unification. There were several faulty proofs of the
        decidability of this problem. In this paper we prove that
        simultaneous rigid $E$-unification is undecidable. As a
        consequence we obtain the undecidability of the
        $\exists^{\ast}$-fragment of intuitionistic logic with
        equality.