In his later years, Jack Schwartz devoted much energy to the implementation of a proof-checker based on set theory and to the preparation of a large script file to be fed into it. His goal was to attain a verified proof of the Cauchy integral theorem of complex analysis. This contribution to the memorial volume for Jack reflects that effort: it briefly reports the chronicle of his proof-checking project and highlights some features of the system as implemented; in an annex, it presents a proof scenario leading from bare set theory to two basic theorems about claw-free graphs.

The Ref Proof-Checker and Its “Common Shared Scenario”

OMODEO, EUGENIO;
2013-01-01

Abstract

In his later years, Jack Schwartz devoted much energy to the implementation of a proof-checker based on set theory and to the preparation of a large script file to be fed into it. His goal was to attain a verified proof of the Cauchy integral theorem of complex analysis. This contribution to the memorial volume for Jack reflects that effort: it briefly reports the chronicle of his proof-checking project and highlights some features of the system as implemented; in an annex, it presents a proof scenario leading from bare set theory to two basic theorems about claw-free graphs.
2013
9781447142812
File in questo prodotto:
Non ci sono file associati a questo prodotto.
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/2625839
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact