Computational Logic and Set Theory

Schwartz on computational logic and set theory and its application to proof verification techniques, culminating in the AEtnaNova system, a prototype computer program designed to verify the correctness of mathematical proofs presented in the language of set theory.