Tools for semi-formal proofs

We propose a semi-formal proof structure, in which the overall arrangement of a proof is a formal data structure, while individual propositions within the structure are expressed either formally or informally. We hypothesize that such proofs are easier to check accurately, compared with standard informal prose proofs. Our framework is conceptually simple, and proofs written in it look similar to informal proofs. We also give the definitions and the main theorem on the correctness of our structure-checking algorithm. The theorem is essentially that the proofs accepted by our algorithm are indeed correct. The thesis also includes an empirical study which involves experimentation of our proposed version of semi-formal proof structure in comparison to traditionally written prose proofs. If our hypothesis is correct, the system should be easier for students to learn, and yield intuitions that can be more effectively leveraged toward reading actual proofs in computer science literature.