The way in which Martin Davis conceived the first chapter of his book ``emph{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 see there a common trait between that book and another writing of the year 1977, ``emph{Metamathematical extensibility for theorem provers and proof-checkers}'', which Martin coauthored with Jacob T. Schwartz. To underline the contribution of the said part of Martin's study on nonstandard analysis to proof technology, we prepare the ground for its detailed verification with a proof-checker based on set theory.

Banishing ultrafilters from our consciousness

Domenico Cantone;
2016

Abstract

The way in which Martin Davis conceived the first chapter of his book ``emph{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 see there a common trait between that book and another writing of the year 1977, ``emph{Metamathematical extensibility for theorem provers and proof-checkers}'', which Martin coauthored with Jacob T. Schwartz. To underline the contribution of the said part of Martin's study on nonstandard analysis to proof technology, we prepare the ground for its detailed verification with a proof-checker based on set theory.
978-3-319-41841-4
Proof checking
Information hiding
Non-standard analysis
Foundations of infinitesimal calculus
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/20.500.11769/323153
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact