Under the premise that knaves always lie, if A is a knave, then their statement "I am a knave" must have been a lie, thus this solution cannot be correct.
A isn't making two statements. The (single) statement "I am a knave, but B isn't." is a conjunction that is false because it's right hand side is false.
I find the biggest challenge with these kinds of logic puzzles is in translating from the English (or other human language) into symbolic logic. It's not well-documented and bug-prone. Er, (not well-documented) /\ bug-prone. Not (not (well-documented /\ bug-prone)).
Like the famous Two Guardians riddle: one always lies, the other always tells the truth, you get one question, etc. There's a translation that starts "You have a wire and a NOT gate..." in which the puzzle becomes blindingly obvious. (Details omitted so as not to spoil the puzzle for anyone.)
Once you have developed a facility with the special jargon of logic puzzles and know Prolog, I've found that, while some puzzles become boring ( https://swish.swi-prolog.org/p/Boring%20Sudoku.swinb ), many are still interesting as an art form, much like le demo scene you could imaging puzzle scene and not be too far off metaphorically.
I recently released a match-burning logic puzzle app[1] based on a mensa calendar puzzle I saw and it took me a while to develop an (imperfect) solver algorithm in C#. Someone then told me that the general class of these puzzles is called "Thermometer Puzzles" and that there are a ton of Prolog-based solvers[2] out there.
This class of puzzle is not mentioned in the article, but I'm truly amazed at how versatile Prolog is at solving logic puzzles with so little code. I'm guessing the Prolog compiler is super complex compared to, say, a C compiler to be able to give developers that much power.
> I'm guessing the Prolog compiler is super complex compared to, say, a C compiler to be able to give developers that much power.
Nah. Both Prolog and C do a very similar step: they walk through call-sites and function signatures in your code and check them for compatibility with each-other in a way that can constrain both the call and the function, or they fail to make a match and they rewind and try again with other constraints. The only difference is that C is only doing this unification for the types of the parameters, whereas Prolog is doing it for the parameter values.
Any programming language that has static types but also has an “auto” variable type, where the type is deduced from the use-def and def-use chains that statement live in, is doing absolutely everything Prolog does, and just not exposing the power of it to you. (Hindley-Milner is an even more advanced constraint-solver than Prolog is.)
(Though, to be clear, if you can program in the type system, as you can in C++, then you do get an exposure to that power, and can write many backtracking algorithms with it.)
If I understand correctly, Hindley-Milner type inference performs unification but not resolution.
So I don't think the above is correct. I don't think there's any language that has built-in SLD-resolution theorem proving that isn't a logic programming language.
And Prolog is not really a constraint solver. Constraint Logic Programming languages have been implemented in Prolog but the concept of "constraint" is not built-in to Prolog.
Prolog has constraints but they're limited to "equality" for some notion of that word. Constraint solvers and constraint extensions to Prolog broaden that considerably.
Do you mean the equality predicates, like ==/2 or =:=/2 etc, or do you mean unification? I dont' really think of unification as a constraint but, I don't know, maybe you have a point.
> Nah. Both Prolog and C do a very similar step: they walk through call-sites and function signatures in your code and check them for compatibility with each-other in a way that can constrain both the call and the function,
C type checking does not "constrain the call and the function". It looks at existing, fixed types (not constraints on types) and fails or succeeds. I may be misunderstanding you, can you explain in more depth what you mean?
> or they fail to make a match and they rewind and try again with other constraints.
I don't think C compilers ever backtrack during type checking. Again, maybe I'm misunderstanding what you mean?
> The only difference is that C is only doing this unification for the types of the parameters, whereas Prolog is doing it for the parameter values.
Other big differences include the fact that the C compiler does this at compile time as a preparation for execution, while in Prolog this is most of execution; the fact that Prolog has logic variables; the fact that Prolog has arbitrary nested structures that can be unified; the fact noted above that Prolog does backtracking; and, in general, the big difference that Prolog is nothing like C at all.
> Any programming language that has static types but also has an “auto” variable type, where the type is deduced from the use-def and def-use chains that statement live in, is doing absolutely everything Prolog does, and just not exposing the power of it to you. (Hindley-Milner is an even more advanced constraint-solver than Prolog is.)
AFAIK plain Hindley-Milner does only unification but not backtracking, so I would call it strictly less powerful than Prolog. If we assume a backtracking version of Hindley-Milner, we might call it equally powerful to Prolog. I don't see at all how you can claim that it's "more advanced" than Prolog, though.
> (Though, to be clear, if you can program in the type system, as you can in C++, then you do get an exposure to that power, and can write many backtracking algorithms with it.)
I don't know enough about the intricacies of C++ template metaprogramming, but I'm not under the impression that it exposes backtracking as a primitive the way that Prolog does. (Modulo the trivial observation that C++ templates are known to be Turing complete, so you should be able to implement your own backtracking in them.)
When I learned Common Lisp, I devoured the available textbooks in 1989 and for a few years after. A book from the early 1990s is: Paradigms of AI Programming: Case Studies in Common Lisp. By Peter Norvig (now employed by Google)
The book first teaches you Common Lisp, which isn't that difficult to pick up. But that itself is a transformative experience.
Then the book shows you how to build a number of amazing things using Common Lisp. It starts IIRC, with pattern matching. Term rewriting. Unification matching.
Then you proceed to build a few things like:
1. A program that solves high school style algebra word problems.
2. A "prolog" (but expressed in Lisp syntax) that is a "hair's breadth" (in the author's words) from real prolog.
This book was mind blowing. A revelation. Insightful.
Learning Lisp (even from other textbooks before the one I mention here) was a transformative experience. But this single book stands out in providing so many amazing ideas expressed in Lisp.
Other Lisp texts I had read taught me things like playing two-player zero sum games (TicTacToe, Checkers, Reversi). I abstracted the technique to have a single re-usable AI engine implementing the Minimax with Alpha-Beta pruning, and then different layers on top of that which implemented different games (as listed earlier) by defining a game board, move generator and board scoring function.
One Lisp textbook I had from the late 1980s showed a program to plan movements of a robot arm to manipulate blocks according to english like commands.
All of these amazingly sophisticated things take up very little Lisp code. Often only a few pages.
The journey of learning Lisp, with a really good textbook, is an amazing learning experience. Learning Lisp will change the way you think about code for the rest of your entire life. I can confidently say that having learned Lisp starting in about 1986 and dabbling with it through 1993. The initial learning comes quickly. But you will play with this new toy for a long time.
Another book (The Elements of Artificial Intelligence Using Common Lisp) introduced me to the A-star search. I've used that technique, in Java, to build a "solver" for a game sometimes called "Traffic Jam" or "Unblock Me".
Speaking of constraint solvers, the author of Power of Prolog, Markus Triska, is now in the process of porting his clp(ℤ) constraint solver over to my system, having already ported his boolean constraint solver, clp(B). They are quite complex, but it helps that they're written entirely in Prolog.
FWIW, there's this paper that "[takes] a fresh, 'clean-room' look at implementing Prolog by deriving its translation to an executable representation and its execution algorithm from a simple Horn Clause meta-interpreter."
"A Hitchhiker’s Guide to Reinventing a Prolog Machine" Paul Tarau
I've been reading this book to get an overview of Prolog: http://www.learnprolognow.org/. It's much better than most of the tutorials I found out there, and provides a very gentle, very thorough introduction to what might be some fairly alien programming ideas (at least, they were to me).
I'm still chewing over the fact that a Prolog term looks exactly the same whether it's in a knowledge base (ie it's true), or whether you're feeding it to the prompt (ie you're asking if it's true or not). Maybe I'm just spooking myself out, but the identity of facts and queries feels reminiscent of Lisp's homoiconicity between code and data.
> Maybe I'm just spooking myself out, but the identity of facts and queries feels reminiscent of Lisp's homoiconicity between code and data.
Wait until you discover Prolog's homoiconicity ;-)
You can treat Prolog terms as data and also add them to the database as code and call the resulting goals like all others:
?- MyFact = f(x), assert(MyFact).
MyFact = f(x).
?- f(A).
A = x.
?- MyRule = (f(g(X)) :- f(X)), assert(MyRule).
MyRule = (f(g(X)):-f(X)).
?- f(A).
A = x ;
A = g(x) ;
A = g(g(x)) .
That is, asserting the "data" "f(x)" and "f(g(X)) :- f(X)" behaves the same as putting the identical-looking "code" in a source file.
You can also query the code and get back it back as identical-looking "data":
?- Head = f(_), clause(Head, Body).
Head = f(x),
Body = true ;
Head = f(g(_G1014)),
Body = f(_G1014).
(The first of these represents the fact "f(X)." as "f(X) :- true." to make things more uniform internally.)
As for what this is good for, you can use it to write your own metainterpreters that execute Prolog code in the normal way, or in some nonstandard or enhanced way, recording tracing data for example. There is a good writeup on metainterpreters at https://www.metalevel.at/acomip/
28 comments
[ 4.0 ms ] story [ 69.0 ms ] thread> (...code here...)
>
> Thus, in this example, both A and B are knaves.
Under the premise that knaves always lie, if A is a knave, then their statement "I am a knave" must have been a lie, thus this solution cannot be correct.
Still, makes me think that this could have been stated clearly instead of relying on the reader interpreting it in that manner.
Like the famous Two Guardians riddle: one always lies, the other always tells the truth, you get one question, etc. There's a translation that starts "You have a wire and a NOT gate..." in which the puzzle becomes blindingly obvious. (Details omitted so as not to spoil the puzzle for anyone.)
Once you have developed a facility with the special jargon of logic puzzles and know Prolog, I've found that, while some puzzles become boring ( https://swish.swi-prolog.org/p/Boring%20Sudoku.swinb ), many are still interesting as an art form, much like le demo scene you could imaging puzzle scene and not be too far off metaphorically.
I recently released a match-burning logic puzzle app[1] based on a mensa calendar puzzle I saw and it took me a while to develop an (imperfect) solver algorithm in C#. Someone then told me that the general class of these puzzles is called "Thermometer Puzzles" and that there are a ton of Prolog-based solvers[2] out there.
This class of puzzle is not mentioned in the article, but I'm truly amazed at how versatile Prolog is at solving logic puzzles with so little code. I'm guessing the Prolog compiler is super complex compared to, say, a C compiler to be able to give developers that much power.
[1] https://play.google.com/store/apps/details?id=com.umvirate.e...
[2] https://github.com/zettca/ist.lp.thermometers/blob/master/th...
Nah. Both Prolog and C do a very similar step: they walk through call-sites and function signatures in your code and check them for compatibility with each-other in a way that can constrain both the call and the function, or they fail to make a match and they rewind and try again with other constraints. The only difference is that C is only doing this unification for the types of the parameters, whereas Prolog is doing it for the parameter values.
Any programming language that has static types but also has an “auto” variable type, where the type is deduced from the use-def and def-use chains that statement live in, is doing absolutely everything Prolog does, and just not exposing the power of it to you. (Hindley-Milner is an even more advanced constraint-solver than Prolog is.)
(Though, to be clear, if you can program in the type system, as you can in C++, then you do get an exposure to that power, and can write many backtracking algorithms with it.)
So I don't think the above is correct. I don't think there's any language that has built-in SLD-resolution theorem proving that isn't a logic programming language.
And Prolog is not really a constraint solver. Constraint Logic Programming languages have been implemented in Prolog but the concept of "constraint" is not built-in to Prolog.
C type checking does not "constrain the call and the function". It looks at existing, fixed types (not constraints on types) and fails or succeeds. I may be misunderstanding you, can you explain in more depth what you mean?
> or they fail to make a match and they rewind and try again with other constraints.
I don't think C compilers ever backtrack during type checking. Again, maybe I'm misunderstanding what you mean?
> The only difference is that C is only doing this unification for the types of the parameters, whereas Prolog is doing it for the parameter values.
Other big differences include the fact that the C compiler does this at compile time as a preparation for execution, while in Prolog this is most of execution; the fact that Prolog has logic variables; the fact that Prolog has arbitrary nested structures that can be unified; the fact noted above that Prolog does backtracking; and, in general, the big difference that Prolog is nothing like C at all.
> Any programming language that has static types but also has an “auto” variable type, where the type is deduced from the use-def and def-use chains that statement live in, is doing absolutely everything Prolog does, and just not exposing the power of it to you. (Hindley-Milner is an even more advanced constraint-solver than Prolog is.)
AFAIK plain Hindley-Milner does only unification but not backtracking, so I would call it strictly less powerful than Prolog. If we assume a backtracking version of Hindley-Milner, we might call it equally powerful to Prolog. I don't see at all how you can claim that it's "more advanced" than Prolog, though.
> (Though, to be clear, if you can program in the type system, as you can in C++, then you do get an exposure to that power, and can write many backtracking algorithms with it.)
I don't know enough about the intricacies of C++ template metaprogramming, but I'm not under the impression that it exposes backtracking as a primitive the way that Prolog does. (Modulo the trivial observation that C++ templates are known to be Turing complete, so you should be able to implement your own backtracking in them.)
When I learned Common Lisp, I devoured the available textbooks in 1989 and for a few years after. A book from the early 1990s is: Paradigms of AI Programming: Case Studies in Common Lisp. By Peter Norvig (now employed by Google)
The book first teaches you Common Lisp, which isn't that difficult to pick up. But that itself is a transformative experience.
Then the book shows you how to build a number of amazing things using Common Lisp. It starts IIRC, with pattern matching. Term rewriting. Unification matching.
Then you proceed to build a few things like:
1. A program that solves high school style algebra word problems.
2. A "prolog" (but expressed in Lisp syntax) that is a "hair's breadth" (in the author's words) from real prolog.
This book was mind blowing. A revelation. Insightful.
Learning Lisp (even from other textbooks before the one I mention here) was a transformative experience. But this single book stands out in providing so many amazing ideas expressed in Lisp.
Other Lisp texts I had read taught me things like playing two-player zero sum games (TicTacToe, Checkers, Reversi). I abstracted the technique to have a single re-usable AI engine implementing the Minimax with Alpha-Beta pruning, and then different layers on top of that which implemented different games (as listed earlier) by defining a game board, move generator and board scoring function.
One Lisp textbook I had from the late 1980s showed a program to plan movements of a robot arm to manipulate blocks according to english like commands.
All of these amazingly sophisticated things take up very little Lisp code. Often only a few pages.
The journey of learning Lisp, with a really good textbook, is an amazing learning experience. Learning Lisp will change the way you think about code for the rest of your entire life. I can confidently say that having learned Lisp starting in about 1986 and dabbling with it through 1993. The initial learning comes quickly. But you will play with this new toy for a long time.
Another book (The Elements of Artificial Intelligence Using Common Lisp) introduced me to the A-star search. I've used that technique, in Java, to build a "solver" for a game sometimes called "Traffic Jam" or "Unblock Me".
I think there is ongoing effort to update it for better accessibility.
(Also responded directly to your comment above, but just in case this is helpful here as well :)
The logic programming bits in particular (the core of the Prolog interpreter) can be read in a maybe-nicer way here: http://dhconnelly.com/paip-python/docs/paip/logic.html
They're not that complex. I'm writing one from scratch right now:
http://github.com/mthom/scryer-prolog
Speaking of constraint solvers, the author of Power of Prolog, Markus Triska, is now in the process of porting his clp(ℤ) constraint solver over to my system, having already ported his boolean constraint solver, clp(B). They are quite complex, but it helps that they're written entirely in Prolog.
"A Hitchhiker’s Guide to Reinventing a Prolog Machine" Paul Tarau
https://www.cse.unt.edu/~tarau/research/2017/eng.pdf
Slides: https://software.imdea.org/Conferences/CICLOPS2017/files/tar...
Here - https://github.com/prolog8/awkprolog - is an interesting example of Prolog written in AWK. Not too long and neither too dense code.
I'm still chewing over the fact that a Prolog term looks exactly the same whether it's in a knowledge base (ie it's true), or whether you're feeding it to the prompt (ie you're asking if it's true or not). Maybe I'm just spooking myself out, but the identity of facts and queries feels reminiscent of Lisp's homoiconicity between code and data.
Wait until you discover Prolog's homoiconicity ;-)
You can treat Prolog terms as data and also add them to the database as code and call the resulting goals like all others:
That is, asserting the "data" "f(x)" and "f(g(X)) :- f(X)" behaves the same as putting the identical-looking "code" in a source file.You can also query the code and get back it back as identical-looking "data":
(The first of these represents the fact "f(X)." as "f(X) :- true." to make things more uniform internally.)As for what this is good for, you can use it to write your own metainterpreters that execute Prolog code in the normal way, or in some nonstandard or enhanced way, recording tracing data for example. There is a good writeup on metainterpreters at https://www.metalevel.at/acomip/