``Implementation of the Boyer and Moore Theorem Prover, version 2.0''
Computer Science Undergraduate Thesis

Summary

The version I developed was written in compilable Franz-LISP on a Micro-Vax II running UNIX. Approppriate data structures were used to store the theorems in both primary and secondary memory, in order to achieve efficient execution and low response time. A user-friendly interface based on menus was designed, allowing edition of the knowledge base at any moment and displaying the history of the proof of each theorem in a natural fashion.

Web Accessibility