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.

PDF file

In  Proceedings of the 4th Asian Computing Science Conference on Advances in Computing Science (ASIAN 98)

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details