Difference between logic programming and automated theorem proving

Question

What is the difference between logic programming and automated theorem proving (ATP) (e.g. with E-Prover, Spass or Princess)?

I searched a lot and the only information I found is that ATP is the precursor of logic programming. But I do not see the difference. But I guess it is more than the syntax.

Nelle

This paper helps illustrate the difference: Implementing Theorem Provers in Logic Programming – Prevent

Answer 1

As far as the Prolog part of the question is concerned, this was best said by Richard O'Keefe:

Prolog is an efficient programming language because it is a stupid theorem prover.

Thus, there is a connection between Prolog and theorem proving. Prolog has some features of a theorem prover, for example, it searches for proofs or rather resolution refutations, but it does so in an incomplete way that is more tailored to a general purpose programming language.

Of course, the comparatively close affinity between Prolog and theorem provers makes Prolog an excellent choice to implement more full-fledged theorem provers.

In fact, it is comparatively easy to augment and extend the incomplete default execution strategy of Prolog so that the search becomes more complete.

Note though that Prolog also exhibits some extra-logical features that fall outside the scope of theorem proving and can in fact often get in the way of declarative reasoning. See also logical-purity.

Maiolica

The word incomplete merits some qualification here: It is incomplete in case Prolog goes into an infinite loop - or another error - only. – Tgroup

I would remove the word "another" from this qualification. What do you think? – Maiolica

Argh, should even better explain what is meant by error. That is some signalled exception. – Tgroup

@Maiolica do you have the reference for the quotation? – Alessandraalessandria