ELIOS-OBJ theorem proving in a specification language

Abstract : In the context of the executable specification language OBJ3 an order-sorted completion procedure is implemented, providing automatically convergent specifications from user-given ones. This feature is of first importance to ensure unambiguity and termination of the rewriting execution process. We describe here how we specified a modular completion design in terms of inference rules and control language, using OBJ3 itself. On another hand, the specific problems encountered to integrate a completion process in an already reduction-oriented environment are pointed out.
Type de document :
Rapport
[Research Report] RR-1668, INRIA. 1992
Liste complète des métadonnées

https://hal.inria.fr/inria-00074889
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 16:48:50
Dernière modification le : lundi 17 septembre 2018 - 13:42:01
Document(s) archivé(s) le : mardi 12 avril 2011 - 19:55:14

Fichiers

Identifiants

  • HAL Id : inria-00074889, version 1

Collections

Citation

Isabelle Gnaedig. ELIOS-OBJ theorem proving in a specification language. [Research Report] RR-1668, INRIA. 1992. 〈inria-00074889〉

Partager

Métriques

Consultations de la notice

87

Téléchargements de fichiers

37