Equational problems and disunification

Abstract : Roughly speaking, an equational problem is a first order formula whose only predicate symbol is =. We propose some rules for the transformation of equational problems and study their correctness in various models. Then, we give completeness results with respect to some "simple" problems called solved forms. Such completeness results still hold when adding some control which moreover ensures termination. The termination proofs are given for a "weak" control and thus hold for the (large) class of algorithms obtained by restricting the scope of the rules. Finally, it must be noted that a by-product of our method is a decision procedure for the validity in the Herbrand Universe of any first order formula with the only predicate symbol =.
Type de document :
Rapport
[Research Report] RR-0904, INRIA. 1988
Liste complète des métadonnées

https://hal.inria.fr/inria-00075652
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 18:44:06
Dernière modification le : samedi 17 septembre 2016 - 01:06:52
Document(s) archivé(s) le : vendredi 13 mai 2011 - 14:00:33

Fichiers

Identifiants

  • HAL Id : inria-00075652, version 1

Collections

Citation

Hubert Comon, Pierre Lescanne. Equational problems and disunification. [Research Report] RR-0904, INRIA. 1988. 〈inria-00075652〉

Partager

Métriques

Consultations de la notice

137

Téléchargements de fichiers

65