We present three newsletters drawn from the documentation of a project aimed at developing a software system which ingests proofs formalized within Zermelo-Fraenkel set theory and checks their compliance with mathematical rigor. Our verifier will accept trivial steps as obvious and will be able to process large proof scripts (say dozens of thousands of proofware lines written on persistent files). To test our prototype proof-checker we are developing, starting from the bare rudiments of set theory, various proof scenarios, the largest of which concerns the Cauchy Integral Theorem. The first newsletter is devoted to the treatment of inductive sets and to the issue of proof modularization, in sight of possible applications of our computerized proof environment in program correctness verification. The second newsletter proposes a decision procedure for ordered Abelian groups, examined in detail, as a candidate for inclusion in the inferential core of our verification system. The third newsletter discusses how to best define the set of real numbers and prove their basic properties. After having experienced difficulties with the classical approach devised by Dedekind, we now incline to follow the approach originally developed by Cantor and recently adapted by E. A. Bishop and D. S. Bridges.

Notes from the logbook of a proof checker's project

URSINO, PIETRO
2004

Abstract

We present three newsletters drawn from the documentation of a project aimed at developing a software system which ingests proofs formalized within Zermelo-Fraenkel set theory and checks their compliance with mathematical rigor. Our verifier will accept trivial steps as obvious and will be able to process large proof scripts (say dozens of thousands of proofware lines written on persistent files). To test our prototype proof-checker we are developing, starting from the bare rudiments of set theory, various proof scenarios, the largest of which concerns the Cauchy Integral Theorem. The first newsletter is devoted to the treatment of inductive sets and to the issue of proof modularization, in sight of possible applications of our computerized proof environment in program correctness verification. The second newsletter proposes a decision procedure for ordered Abelian groups, examined in detail, as a candidate for inclusion in the inferential core of our verification system. The third newsletter discusses how to best define the set of real numbers and prove their basic properties. After having experienced difficulties with the classical approach devised by Dedekind, we now incline to follow the approach originally developed by Cantor and recently adapted by E. A. Bishop and D. S. Bridges.
File in questo prodotto:
File Dimensione Formato  
CanOmScUrs.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: DRM non definito
Dimensione 345.17 kB
Formato Adobe PDF
345.17 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11383/20907
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact