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;
2012-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.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.
