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.
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.