Solving disequations

Abstract : We present a general study of equations (objects of form s=t and disequations (objects of form s \ne t) solving. The problem is approached from its fully general mathematical definition clearly separating universally and existentially quantified variables. In addition it is showed to have many connections with unification in equational theories like associativity commutativity, in particular methods similar to those used to solve equational unification problem works in solving disequations. This abstract framework is then applied to study the sufficient completeness of a rewrite rule based definition of a function.
Type de document :
Rapport
[Research Report] RR-0686, INRIA. 1987
Liste complète des métadonnées

https://hal.inria.fr/inria-00075867
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 19:29:37
Dernière modification le : samedi 17 septembre 2016 - 01:06:54
Document(s) archivé(s) le : vendredi 13 mai 2011 - 15:57:07

Fichiers

Identifiants

  • HAL Id : inria-00075867, version 1

Collections

Citation

Claude Kirchner, Pierre Lescanne. Solving disequations. [Research Report] RR-0686, INRIA. 1987. 〈inria-00075867〉

Partager

Métriques

Consultations de la notice

145

Téléchargements de fichiers

69