Why horn clauses, specifically? By the way, are you aware of resources that explain Prolog the way you did (in terms of logic?) the ones that I do know either explain how to _implement_ prolog (eg. the WAM), or provide a "high-level" explanation of unification --- missing out the details that you've just pointed out. I'd love for an authoritative reference!
Another question: do you know of an easy way to _implement_ prolog? The problem with the WAM is that it is incredibly hard to debug: I had begun implementing it (https://github.com/bollu/warren) but then gave up due to getting boggled in large heap data structures that weren't doing what I wanted, and debugging this manually got far too painful :(
That's a very good question. My (sloppy) answer is that satisfiability of sets of
clauses is undecidable for arbitrary clausal languages, but a variant of the
resolution rule, SLDNF-Resolution, is refutation-complete for sets of Horn
clauses and sound (and complete) for sets of definite clauses. Definite
clauses are a subset of Horn clauses having exactly one positive literal (i.e.
facts and rules in Prolog). Horn clauses are clauses with at most one positive
literal.
Given a set of definite clauses and a Horn goal clause, it is possible to
prove by refutation that the goal is true in the context of the program, in a
finite number of steps. This is how the Prolog interactive mode works: the
user enters a goal clause as a "query" and Prolog tries to refute the query by
SLDNF-resolution.
SLDNF-resolution is "SLD resolution with Negatation as (finite) Failure".
"SLD resolution" stands for Selective, Linear Definite resolution (it's a long
story). Negation as (finite) failure (NAF) accepts that a statement is true if
it cannot be proven false under a closed-world assumption (that all we know
that is true, is all that we can assume is true). NAF means that Prolog
programs can include clauses with negated literals, which is very handy because
one often wants to say things like "X is an Evil Demon Bear from Mars if X has
green fur and purple-glowing eyes _unless_ X plays the hurdy-gurdy".
These are some of the basic assumptions of Prolog: SLDNF-resolution, definite
clauses and negation-as-failure under a closed-world assumption. The goal is
to have a package that, under some conditions, can prove a goal given a
logic program. Given that, it's possible to write a logic theorem and have it
execute like a program, by proving a goal.
In terms of learning resources- if you have a bit of a logic background I
think that "Programming in Prolog" by Clocksin and Mellish does a good job of
going over both the declarative and imperative reading of Prolog (but it's
been more than 10 years since I first read it so I might be wrong).
I haven't even tried implementing Prolog. Too much hard work and it's already
been done by others :) So no idea how to do it. But it's probably the easiest
way to get a good set of deep insights in the language and I should probably
plonk my arse down and do it, myself.
Another question: do you know of an easy way to _implement_ prolog? The problem with the WAM is that it is incredibly hard to debug: I had begun implementing it (https://github.com/bollu/warren) but then gave up due to getting boggled in large heap data structures that weren't doing what I wanted, and debugging this manually got far too painful :(