Advertisement

Mizar Correctness Proofs of Generic Fraction Field Arithmetic

  • Christoph Schwarzweller
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1766)

Abstract

We propose the Mizar system as a theorem prover capable of verifying generic algebraic algorithms on an appropriate abstract level. The main advantage of the Mizar theorem prover is its special proof script language that enables textbook style presentation of proofs, hence allowing proofs in the language of algebra.

Using Mizar we were able to give a rigorous machine assisted correctness proof of a generic version of the Brown/Henrici arithmetic in the field of fractions over arbitrary gcd domains.

Keywords

Integral Domain Great Common Divisor Natural Deduction Correctness Proof Addition Algorithm 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    George E. Collins, Algebraic Algorithms, chapter two: Arithmetics, Lecture manuscript, 1974.Google Scholar
  2. 2.
    Antoni Diller, Z—An Introduction to Formal Methods, 2nd ed., Wiley, New York, 1994.zbMATHGoogle Scholar
  3. 3.
    D. Knuth, Literate Programming, The Computer Journal 27(2), 97–111, 1984.Google Scholar
  4. 4.
    Rüdiger Loos and George E. Collins, Revised Report on the Algorithm Description Language ALDES, Technical Report WSI-92-14, Wilhelm-Schickard-Institut für Informatik, 1992.Google Scholar
  5. 5.
    Udi Manber and Burra Gopal, GLIMPSE—A Tool to Search Entire File Systems, available from http://glimpse.cs.arizona.edu.
  6. 6.
    Piotr Rudnicki, An Overview of the Mizar Project, available from http://web.cs.ualberta.ca:80/~piotr/Mizar, June 1992.
  7. 7.
    Sibylle Schupp, Generic Programming—SuchThat One Can Build an Algebraic Library, Ph.D. thesis, University of Tübingen, 1996.Google Scholar
  8. 8.
    Christoph Schwarzweller, Mizar Verification of Generic Algebraic Algorithms, Ph.D. thesis, University of Tübingen, 1997.Google Scholar
  9. 9.
    Andrzej Trybulec, Some Features of the Mizar Language, available from http://web.cs.ualberta.ca:80/~piotr/Mizar, July 1993.

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Christoph Schwarzweller
    • 1
  1. 1.Wilhelm-Schickard-Institute for Computer ScienceTübingen

Personalised recommendations