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; Tomescu, Alexandru. - STAMPA. - (2013), pp. 121-167. [10.1007/978-1-4471-4282-9_8]
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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.


