HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Rigid Reachability

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 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 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 in EXPTIME.
Document type :
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:22:30 AM
Last modification on : Friday, February 4, 2022 - 3:31:12 AM
Long-term archiving on: : Friday, November 25, 2016 - 11:53:51 AM


  • HAL Id : inria-00098741, version 1



Harald Ganzinger, Florent Jacquemard, Margus Veanes. Rigid Reachability. [Intern report] 98-R-388 || ganzinger98a, 1998, 24 p. ⟨inria-00098741⟩



Record views


Files downloads