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 metadatas

https://hal.inria.fr/inria-00099097
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:50:56 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM

Identifiers

  • HAL Id : inria-00099097, version 1

Collections

Citation

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

Share

Metrics

Record views

138