korona wrote:Logic programming is much more expressive. How can I get from a set of horn clauses to a functional program that computes a refutation of those clauses without implementing a theorem prover?

See The Reasoned Schemer, linked above. It's an easy read. Alternatively, you can try

On Lisp, in which Paul Graham demonstrates how to compile a logic program into a functional one.

Haskell has very lovely methods for doing this using the MonadPlus typeclass.

korona wrote:No. You have to trust the underlying theorem prover to do the correct unifications (or in the Prolog case: know about the order in which unifications are done). In C/C++ you know that int c = a + b will be translated to a single (or a few) machine instructions. A logic program has to compute a resolution refutation to obtain the same result.

Oh, so you know how C will resolve the operation, and yet you

don't know that there is a maximum time for Prolog to do so? Of course it can be malformed and take infinite time, but you can do that with any Turing complete language.

Laguana wrote:headprogrammingczar wrote:Prolog isn't even that great of a logic language. It's pretty much just the the type level of Haskell, with even wonkier syntax. It's even Turing-complete, so using it as a basis for formal proof is out of the question.

Why do you say that? There are even some very effective theorem provers written in prolog, such as

ileanCoP.

If you turn on all the Haskell language extensions (those concerning type classes, that is), then you get logic programming for free in that you can construct an infinite number of types by making statements about those types in order to describe arbitrary calculations. The syntax isn't great, but it's the gist of logic programming.

Now, the fact that you can write theorem provers in a language isn't evidence that it's a good

for proving theorems. And while you can write theorems in Prolog, it doesn't prove any but the most trivial for you. You can write theorem provers in any language. The fact that it's been done for a particular language doesn't say anything.

And don't even get me started on the Law of Excluded Middle.