The essential resource for Fundamental Proof Methods in Computer Science: A Computer-Based Approach is the Athena programming language/interactive theorem prover. Proof Central also provides the following additional resources.
The following Appendices are provided here for readers of the print edition (they are included in the electronic edition):
Click one of these download links to obtain files containing all of the Athena code that appears in the book, for use in experimenting with the book’s examples and developing solutions to its exercises:
Using the files to develop exercise solutions
Most exercises depend on some of the definitions, declarations, theorems, etc. that are defined in the book preceding the point where the exercise appears. Each chapter file includes the needed material within the file or loads it from the Athena library or from included supplementary files. So one way to work with the file is to load it (or a copy of it) into a text editor, write your solution within the file at the point of the exercise, and test it by loading the file into Athena. Alternatively, load just the part of the file up to the point of the exercise and then work on the solution in Athena’s interactive mode.
Some of the theorems proved in exercises are assumed to be available for use as lemmas in examples or solutions to exercises that appear farther on in the file. Thus it might seem that one must work on exercises in sequential order, and the file might not be fully loadable until all proofs called for have been supplied. To provide for greater flexibility, we have arranged that the files are fully loadable from the beginning and exercises can be tackled in any order: