CODEWITHSUNDEEP
prologtheorem-provinglogic-programming
2Application
2Application

Reputation: 165

Difference between logic programming and automated theorem proving

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.

Upvotes: 9

Views: 896

Answers (1)

mat
mat

Reputation: 40768

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 .

Upvotes: 13

Related Questions