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 metadatas

Cited literature [23 references]  Display  Hide  Download
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:22:30 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 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