First Order Logic in Practice

John Harrison

To appear in FTP'97.


There is a trend away from monolithic automated theorem provers towards using automation as a tool in support of interactive proof. We believe this is a fruitful drawing together of threads in automated reasoning. But it raises a number of issues that are often neglected in the classical first order theorem proving literature such as the following. Is first order automation actually useful, and if so, why? How can it be used for richer logics? What are the characteristic examples that require solution in practice? How do the traditional algorithms perform on these `practical' examples --- are they deficient or are they already too powerful? We discuss these and similar questions in the light of our own recent experience in this area using the HOL prover.

DVI or PostScript or PDF