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.
Type de document :
Rapport
[Intern report] 98-R-388 || ganzinger98a, 1998, 24 p
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00098741
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:22:30
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 11:53:51

Fichiers

Identifiants

  • HAL Id : inria-00098741, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

95

Téléchargements de fichiers

30