"Higher-Order" Mathematics in B

Abstract : In this paper, we investigate the possibility to mechanize the proof of some real complex mathematical theorems in B [1]. For this, we propose a little structure language which allows one to encode mathematical structures and their accompanying theorems. A little tool is also proposed, which translates this language into B, so that Atelier B, the tool associated with B, can be used to prove the theorems. As an illustrative example, we eventually (mechanically) prove the Theorem of Zermelo [6] stating that any set can be well-ordered. The present study constitutes a complete reshaping of an earlier (1993) unpublished work (referenced in [4]) done by two of the authors, where the classical theorems of Haussdorf and Zorn were also proved.
Type de document :
Communication dans un congrès
D. Bert, J.P. Bowen, M.C. Henson, K. Robinson. 2nd International Conference of B and Z Users - ZB'2002, Jan 2002, Grenoble, France, Springer, 2272, pp.370-393, 2002, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100923
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:52:54
Dernière modification le : jeudi 11 janvier 2018 - 06:21:04

Identifiants

  • HAL Id : inria-00100923, version 1

Collections

Citation

Jean-Raymond Abrial, Dominique Cansell, Guy Laffitte. "Higher-Order" Mathematics in B. D. Bert, J.P. Bowen, M.C. Henson, K. Robinson. 2nd International Conference of B and Z Users - ZB'2002, Jan 2002, Grenoble, France, Springer, 2272, pp.370-393, 2002, Lecture Notes in Computer Science. 〈inria-00100923〉

Partager

Métriques

Consultations de la notice

164