Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Rigid reachability

Harald Ganzinger, Florent Jacquemard, and Margus Veanes

Abstract

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.

Details

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