Mechanising the theory of intervals using OBJ3 (Q1916976)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 902713
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Mechanising the theory of intervals using OBJ3 |
scientific article; zbMATH DE number 902713 |
Statements
Mechanising the theory of intervals using OBJ3 (English)
0 references
16 February 1997
0 references
OBJ3 is a general purpose declarative language, which was introduced by \textit{J. Goguen, T. Winkler, J. Meseguer, K. Futatsigi} and \textit{J. Jouannaud} (Technical Report, SRI International, 1993, to appear). OBJ3 may be used for specifications (being a collection of modules of type ``theories'' and ``objects'') and for prototyping. A mechanism for theorem proving is included. -- The aim of the paper is to formalize the type ``interval'' within OBJ3 by means of arithmetic and set theoretical properties of intervals.
0 references
theory of intervals
0 references
interval arithmetic
0 references
OBJ3
0 references
collection of modules
0 references
theorem proving
0 references
0.80830914
0 references
0.8030886
0 references
0.80056655
0 references
