First Order Logic in Practice
John Harrison
To appear in FTP'97.
Abstract:
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.