The undecidability of simultaneous rigid E-unification with two variables

Recently it was proved that the problem of simultaneous rigid E-unification, or SREU, is undecidable. Here we show that 4 rigid equations with ground left-hand sides and 2 variables already imply undecidability. As a corollary we improve the undecidability result of the ∃*-fragInent of intuitionistic logic with equality. Our proof shows undecidability of a very restricted subset of the ∃∃-fragment. Together with other results, it contributes to a complete characterization of decidability of the prenex fragment of intuitionistic logic with equality, in terms of the quantifier prefix.

kgc97.pdf
PDF file

In  5th Kurt Gödel Colloquium (KGC'97)

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

TypeInproceedings
Pages305-318
Volume1289
SeriesLNCS
> Publications > The undecidability of simultaneous rigid E-unification with two variables