“Higher-Order” Mathematics in B

  • Jean-Raymond Abrial
  • Dominique Cansell
  • Guy Laffitte
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


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.


Mathematical Structure Choice Function Proof Obligation Local Constant Complex Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.R. Abrial. The B-Book:Assigning Programs to Meanings. Cambridge University Press (1996).Google Scholar
  2. 2.
    N. Bourbaki. Théorie des ensembles. Hermann, Paris, 1970.Google Scholar
  3. 3.
    S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert PVS language reference version 2.3. Technical report, SRI International, September 1999.Google Scholar
  4. 4.
    L. C. Paulson and K. Grabczewski. Mechanizing set theory: Cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, 17(3):291–323, December 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Markus Wenzel. Using axiomatic type classes in Isabelle. part of the Isabelle distribution. Technical report, TU München, February 2001.Google Scholar
  6. 6.
    E. Zermelo. Neuer Beweis für die Möglichkeit einer Wohlordnung. Mathematische Annalen, 65:107–128, 1908.zbMATHGoogle Scholar
  7. 7.
    A. J. M. van Gasteren. On the Shape of Mathematical Arguments, volume 445 of Lecture Notes in Computer Science. Springer-Verlag, 1990.zbMATHGoogle Scholar
  8. 8.
    Clear Sy. Atelier B (version 3.6). 2001.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jean-Raymond Abrial
    • 1
  • Dominique Cansell
    • 2
  • Guy Laffitte
    • 3
  1. 1.ConsultantMarseilleFrance
  2. 2.LORIAMetzFrance
  3. 3.INSEENantesFrance

Personalised recommendations