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.
Type de document :
Article dans une revue
International Journal of Foundations of Computer Science, World Scientific Publishing, 2000, 11 (1), pp.3-27
Liste complète des métadonnées

https://hal.inria.fr/inria-00099097
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:50:56
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

120