Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074889
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 4:48:50 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Tuesday, April 12, 2011 - 7:55:14 PM

Identifiers

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

Share

Metrics

Record views

126

Files downloads

164