Menu
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.
983
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science .
First-order theorem proving is one of the most mature subfields of automated theorem proving. The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way.
Not all theorem provers use the same input and output format, and some of them offer more interaction with the user (in some cases this option is necessary for the proving process). Depending on the selected tools, the process of theorem proving will be different.
Logical Programming is a type of programming paradigm that uses logic circuits to control how facts and rules about the problems within the system are represented or expressed. In it, logic is used to represent knowledge, and inference is used to manipulate it. It tells the model about how to accomplish a goal rather than what goal to accomplish.
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.
163
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
