Rigid reachability

Harald Ganzinger, Florent Jacquemard, and Margus Veanes


We show that rigid reachability, the non-symmetric form of rigid E-unification, is undecidable already in the case of a single constraint. From this we infer the undecidability of a new rather restricted kind of second-order unification. We also show that certain decidable subclasses of the problem which are P-complete in the equational case become EXPTIME-complete when symmetry is absent. By applying automata-theoretic methods, simultaneous monadic rigid reachability with ground rules is shown to be in EXPTIME.


Publication typeInproceedings
Published inProceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN 98)
PublisherSpringer Verlag
> Publications > Rigid reachability