Skip to Main content Skip to Navigation
New interface
Journal articles

Rigid reachability, the non-symmetric form of rigid E-unification

Harald Ganzinger Florent Jacquemard 1 Margus Veanes 
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We show that rigid reachability, the non-symmetric form of rigid E-unification, is already undecidable in the case of a single constraint. From this we infer the undecidability of a new and rather restricted kind of second-order unification. We also show that certain decidable subclasses of the problem which are PTIME-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 PSPACE-complete. Moreover, we identify two decidable non-monadic fragments that are complete for EXPTIME.
Document type :
Journal articles
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:50:56 AM
Last modification on : Friday, February 4, 2022 - 3:32:00 AM


  • HAL Id : inria-00099097, version 1



Harald Ganzinger, Florent Jacquemard, Margus Veanes. Rigid reachability, the non-symmetric form of rigid E-unification. International Journal of Foundations of Computer Science, 2000, 11 (1), pp.3-27. ⟨inria-00099097⟩



Record views