The undecidability of simultaneous rigid E-unification with two variables

Margus Veanes

Abstract

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.

Details

Publication typeInproceedings
Published in5th Kurt Gödel Colloquium (KGC'97)
Pages305-318
Volume1289
SeriesLNCS
PublisherSpringer Verlag
> Publications > The undecidability of simultaneous rigid E-unification with two variables