A study in the application of theorem proving
David C. Luckham, Jorge J. Morales, Joachim Schreiber · 1978
With selected examples we illustrate some useful applications of theorem proving, which have been considered during the last few years, and show, at the same time, the difficulties which have arisen. We aim at some kind of hunch language to guide in the generation of clauses. This paper is a short account of an unpublished manuscript by the same authors.