The way in which Martin Davis conceived the first chapter of his book “Applied nonstandard analysis ” is a brilliant example of information hiding as a guiding principle for the design of widely applicable constructions and methods of proof. We discuss here a common trait that we see between that book and another writing of the year 1977, “Metamathematical extensibility for theorem provers and proof-checkers”, which Martin coauthored with Jacob T. Schwartz . To tie the said part of Martin’s study on nonstandard analysis to proof technology, we undertake a verification, by means of a proof-checker based on set theory, of key results of the non-standard approach to analysis.

Banishing Ultrafilters from Our Consciousness

OMODEO, EUGENIO;
2016-01-01

Abstract

The way in which Martin Davis conceived the first chapter of his book “Applied nonstandard analysis ” is a brilliant example of information hiding as a guiding principle for the design of widely applicable constructions and methods of proof. We discuss here a common trait that we see between that book and another writing of the year 1977, “Metamathematical extensibility for theorem provers and proof-checkers”, which Martin coauthored with Jacob T. Schwartz . To tie the said part of Martin’s study on nonstandard analysis to proof technology, we undertake a verification, by means of a proof-checker based on set theory, of key results of the non-standard approach to analysis.
2016
978-3-319-41841-4
978-3-319-41842-1
978-3-319-41841-4
978-3-319-41842-1
File in questo prodotto:
File Dimensione Formato  
banishingUltrafilters.pdf

Accesso chiuso

Descrizione: Versione preliminare dell'articolo, nella forma originariamente sottomessa per la pubblicazione (precedente la valutazione dei revisori anonimi)
Licenza: Digital Rights Management non definito
Dimensione 580.01 kB
Formato Adobe PDF
580.01 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
cover+index+chapter 10.pdf

Accesso chiuso

Tipologia: Documento in Versione Editoriale
Licenza: Digital Rights Management non definito
Dimensione 1.35 MB
Formato Adobe PDF
1.35 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

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: https://hdl.handle.net/11368/2893490
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact