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.

PDF file

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

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details