Designing a Theorem Prover
Lawrence Charles Paulson · 1992
Abstract Because many different forms of logic are applicable to computer science, a common question is — How do I write a theorem prover? This question can be answered with general advice. For instance, first do enough paper proofs to show that automation of your logic is both necessary and feasible. The question can also be answered with a survey of existing provers, as will be done in this chapter. But automatic theorem proving involves a combination of theoretical and coding skills that is best illustrated by a case study. So this chapter presents a toy theorem prover, called Folderol, highlighting the key design issues. Code fragments are discussed in the text; a full program listing appears at the end of the chapter.