Your statement 2==1+1 is (I'd claim) a weird case in Prolog. Unless you want to code the Peano postulates you need some way to do numerical calculations, and "2 is 1+1" does indeed work in the body of a clause.
Your mathematical explanation of Prolog's theorem proving is precise and correct but almost impenetrable to the average software engineer trying to "get" Prolog. Such explanations only make sense once someone already mostly understands what's going on, and hence aren't useful for beginners. As a first approximation I thought the OP's work wasn't bad.
?- 2 =:= 1+1.
true.
The same goes for "simple" explanations that completely miss the point. Logic programming and Prolog are not simple subjects. That's not by design: theorem proving is bloody hard by nature and making a first-order logic language run on a digital computer is even bloody harder. First-order logic is undecidable in the general case and we must jump through hoops constantly to stick to the special cases where a theorem can be proved automatically and the proof procedure is sound and complete, or at least sound. Without an understanding of this fundamental difficulty in automated theorem proving, Prolog does not make sense, in the long run. For example- why those weird Horn clauses? Why not arbitrary clauses? Why depth-first search? Why unification? And so on.
It is certainly possible to learn Prolog incrementally, without first having to digest, I don't know, the proof of the Subsumption Theorem. But every small step in the way must be taken on firm ground, else the student loses her footing and falls down bottomless pits of despair. I know this from first-hand experience and there is even some scholarship on the trouble that university students get in with Prolog because they form the wrong mental models for it. Let me see if I can locate it online.
Yep, here it is:
What's wrong? Understanding beginners' problems with Prolog
https://link.springer.com/article/10.1007/BF00116441
I'm quoting a bit of the abstract:
The problems that underlie these and other errors seem to be (a) the
complexity of the Prolog primitives (unification and backtracking) and (b)
the misfit between students' naive solutions to a problem and the constructs
that are available in Prolog (e.g. iterative solutions do not map easily to
recursive programs). This suggests that learning Prolog could be helped by
(1) coherent and detailed instruction about how Prolog works, (2) emphasis
on finding recursive solutions that do not rely on primitives such as
assignment and (3) instruction in programming techniques that allow students
to implement procedural solutions.Normally moderators would downweight a submission when this is the consensus from knowledgeable commenters. But this thread is so good that I want to leave it up.
Edit: Should we change the link to https://www.j-paine.org/dobbs/prolog_lightbulb.html (via the inimitable DonHopkins at https://news.ycombinator.com/item?id=22242854)? It hasn't been discussed on HN before.
I have no idea if you should change the link to point to it. What's best for HN?
Edit: I just realised who the author is of the lightbulb joke page: Jocelyn Ireson-Paine. He's the spreadsheet guy! Check out his stuff on making spreadsheets safer... with category theory (and Prolog):
http://www.j-paine.org/old_index.html#making_spreadsheets_sa...
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.
There are some examples on the Web; I'm not sure about quality, but here is a couple:
1) https://github.com/norvig/paip-lisp/tree/master/lisp
Norvig implements (some pieces of?) Prolog in Lisp in his book (book text is freely available)
2) https://github.com/prolog8/awkprolog
An implementation of Prolog in AWK.
Sure, one may not be able to write full prolog programs after these Y minutes. But much more importantly, hopefully they are sparked with some interest in learning the language further!
Just for the most blatant example of made-up semantics: unification is not "essentially a combination of assignment and equality".
Unification is not assignment: Prolog predicates are immutable. You can't assign to an immutable data structure.
Unification is not equality, either. For example, in Prolog 2 = 1+1 fails because "2" does not unify with "1+1" (and not because "unification can't do arithmetic"; it's because unification is not equality).
Unification is an algorithm to decide whether two Horn clauses can be resolved with each other. Resolution is the inference rule used in Prolog's automated theorem proving. This is it:
The horizontal line is read as "entails". p and q are predicates. The rule says that if we can show that p is false or q is true and that p is true, then we can show that q is true. If ¬p and p unify, they can be resolved and q can be shown to be true.Resolution is used in Prolog to prove a query by refutation. Queries are the goals that the author calls "commands". These are not commands: they are predicates, just like "facts" and "rules". Prolog tries to disprove a goal by finding a clause with a head literal that unifies with the query (only "facts" and "rules" have heads, whereas goals only have bodies). If it can, it then recursively proves each literal in the body of the clause, by finding a clause with a head that unifies with the literal.
Unfortunately, none of this will make sense if you try to understand Prolog in terms of assignment and equality tests, and so on. Reading this article and trying to "learn Prolog in Y minutes" will only serve to confuse any further attempts to understand and learn the language.