Course blurb: There are many approaches to formal reasoning. The
objective of specifying computer programs, including the formalization
of worlds with which programs are to interact, has led to the creation
of numerous tools for formal reasoning. We will examine some systems
for formal reasoning while examining a number of mechanical formal
methods tools that support these different systems. Examples of such
system/tool pairs are:
System Tool
Primitive Recursive Arithmetic Boyer-Moore Prover, ACL2
First Order Logic Otter, Nelson's qed
Higher Order Logic HOL, IMPS
Equational Reasoning OBJ
Set Theory Mizar, Quaife/Otter, PVS
Type Theory NuPrl, Lego, Coq
Students will choose, with the help of the instructor, a system and/or
tool to examine and the grade will be based upon presentations about
these.