Great video! I really like your content. I have a question that is a bit out of the scope of this video: if Horn clauses in Prolog can express all computations, why is there negation in Prolog? I understand the negation in Prolog means "cannot be proven". So it is some kind of construct to simplify the representations of the application domain? Am I right in saying that negation in Prolog is not needed in the sense that all programs with negation can be written without it?
Yes, that is right: Negation is not needed in the sense that all programs can be written also without negation. You can show this by expressing a Turing machine with Horn clauses. Instead of negation as finite failure, use predicates like dif/2 and if_/3 to express "not equal" etc. in a pure way that allows logical reasoning about programs by means of failure slicing, generalizations etc. if_/3 was not yet found when the Prolog standard was written, it is a newer language construct with more desirable declarative properties. Thank you a lot for your kind words, and your interest. Enjoy!
The trade-off is between static type checking and meta-interpretation. With Mercury, you get static type checking, and lose the ability to write convenient meta-interpreters. In my own programs, I tend to rely heavily on meta-interpretation and therefore prefer to use Prolog.
Hi, I am interested to understand this video, but it seems my knowledge is still lacking. Is there perhaps any recommended beginner-friendly tutorials/books that builds up into this level knowledge that could help me understand this video? thank you
Nit: Horn clauses are sufficient for expressing not only all known computations, but in fact all CONCEIVABLE ones -- even the once that have never been expressed/formulated/run/&c yet.
At 17:07, I say that they are general enough to express ALL computations. The conceivable ones seem to fall well into this set. The reason I sometimes say "known" is that there may be different *types* of computation that are not yet known, I mean computations that are not Turing-computable.
Was ich bisher überhaupt nicht verstanden habe ist, wie ich eine 'goal clause' in Prolog abbilde. Für eine 'definite clause' ist es ja letztendlich nur A :- B. Aber wie sieht eine 'goal clause' aus. A :- 0 geht ja schlecht.
Goal clause entspricht einer Query: Eine Query wird implizit als negiertes Ziel interpretiert. D.h. ?- A. zu posten bedeutet aus Sicht von Resolution, dass ¬A zu den Klauseln hinzugefügt wird und dann versucht wird, einen Widerspruch abzuleiten. Gelingt das, so ist A logische Konsequenz des Programms.
@@ThePowerOfProlog Nun habe ich das Problem, dass ich einige Prädikate in Form von Horn-Klauseln habe. Diese möchte ich in ein Prolog Programm überführen. Beispielhafter Sourcecode: pred1(a). pred2(a). pred3(X) :- pred1(a), pred2(a). Jedoch habe ich jetzt die goal clause (¬pred1(X) ∧ ¬pred2(X) ∧ ¬pred(X)). Muss jetzt kein Sinn ergeben, nur um ein Beispiel zu haben. Wie würde ich diese im Sourcecode angeben? Und danke für die Antwort :).
@@callahan7257 Das entspricht der Query ?- pred1(X), pred2(X), pred(X). Deklarativ ist das die Behauptung, dass weder pred1(X), noch pred2(X), noch pred(X) gilt. Wenn das widerlegt werden kann, so ist dieses Ziel eine logische Konsequenz des Programms.
I don't understand why you reference "Programming as Theory Building". It is absolutely NOT relevant to the topic at hand. When Naur uses the word "theory" he is speaking of an intuitive understanding of what a large program is supposed to accomplish and mainly speaks about how this theory is separate from things like documentation and source code. He states, for example; "The dependence of a theory on a grasp of certain kinds of similarity between situations and events of the real world gives the reason why the knowledge held by someone who has the theory could not, in principle, be expressed in terms of rules." He is adamantly not talking about systems of rules or formal descriptions when he talks of "theories"; he's talking about intuitions instantiated in the minds of programmers, entirely separate from the content of the programs themselves. This completely goes against the way you're using "theory".
Naur states that he uses the word theory "in the sense of Ryle [1949]" (referring to Ryle's book "The Concept of Mind"), and explains in his paper: "Very briefly, a person who has or possesses a theory in this sense knows how to do certain things and in addition can support the actual doing with explanations, justifications, and answers to queries, about the activity of concern." This is very similar to a logical theory: We can use it to answer queries about the domain of interest, give explanations, justifications etc. And further, Naur says: "theory is understood as the knowledge a person must have in order not only to do certain things intelligently but also to explain them, to answer queries about them, and so forth." This further stresses the connection between theory, knowledge, answering queries etc., as we know them from logical theories. He gives a specific example: "A person having Newton's theory of mechanics must thus understand how it applies to the motions of pendulums and the planets, and must be able to recognize similar phenomena in the world, so as to be able to employ the mathematically expressed rules of the theory properly." Note that Naur is explicitly mentioning "the rules of the theory" in the paper. How the subsequent paragraph that you cite relates to these points seems a bit unclear, and in fact its truth could also be questioned: Is it really so clear that the kinds of similarity between situations and events "could not, in principle, be expressed in terms of rules"? Does the term "intuition" occur anywhere in the paper?
the work you do with prolog is the best it happened to the field, probably with an intangible value.
Thank you so much for your kind words, I greatly appreciate them! Enjoy!
Outstanding matrial! Danke!
Very interesting and well explained!! keep it up :)
Very well structured and very well explained, thank you.
Terrific content! I would love to see how you might solve Smullyan-type logic puzzles with Prolog!
Great presentation. Thank you.
Thank you a lot, I'm very glad you find it useful! Enjoy!
Great video! I really like your content. I have a question that is a bit out of the scope of this video: if Horn clauses in Prolog can express all computations, why is there negation in Prolog? I understand the negation in Prolog means "cannot be proven". So it is some kind of construct to simplify the representations of the application domain? Am I right in saying that negation in Prolog is not needed in the sense that all programs with negation can be written without it?
Yes, that is right: Negation is not needed in the sense that all programs can be written also without negation. You can show this by expressing a Turing machine with Horn clauses. Instead of negation as finite failure, use predicates like dif/2 and if_/3 to express "not equal" etc. in a pure way that allows logical reasoning about programs by means of failure slicing, generalizations etc. if_/3 was not yet found when the Prolog standard was written, it is a newer language construct with more desirable declarative properties. Thank you a lot for your kind words, and your interest. Enjoy!
Thank you😊
Thank you for the good work. OFF TOPIC What is your opinion of Mercury?
The trade-off is between static type checking and meta-interpretation. With Mercury, you get static type checking, and lose the ability to write convenient meta-interpreters. In my own programs, I tend to rely heavily on meta-interpretation and therefore prefer to use Prolog.
@@ThePowerOfProlog Thank you, of the explanation.
Hi, I am interested to understand this video, but it seems my knowledge is still lacking. Is there perhaps any recommended beginner-friendly tutorials/books that builds up into this level knowledge that could help me understand this video? thank you
Thank you a lot for your interest! For a very solid introduction, I recommend the book "Computability and Logic" by Boolos, Jeffrey and Burgess.
ty sir
Sir I need your help can you help me. I need Davis Putnam Sat procedure in prolog
Nit: Horn clauses are sufficient for expressing not only all known computations, but in fact all CONCEIVABLE ones -- even the once that have never been expressed/formulated/run/&c yet.
At 17:07, I say that they are general enough to express ALL computations. The conceivable ones seem to fall well into this set. The reason I sometimes say "known" is that there may be different *types* of computation that are not yet known, I mean computations that are not Turing-computable.
Was ich bisher überhaupt nicht verstanden habe ist, wie ich eine 'goal clause' in Prolog abbilde. Für eine 'definite clause' ist es ja letztendlich nur A :- B. Aber wie sieht eine 'goal clause' aus. A :- 0 geht ja schlecht.
Goal clause entspricht einer Query: Eine Query wird implizit als negiertes Ziel interpretiert. D.h. ?- A. zu posten bedeutet aus Sicht von Resolution, dass ¬A zu den Klauseln hinzugefügt wird und dann versucht wird, einen Widerspruch abzuleiten. Gelingt das, so ist A logische Konsequenz des Programms.
@@ThePowerOfProlog
Nun habe ich das Problem, dass ich einige Prädikate in Form von Horn-Klauseln habe. Diese möchte ich in ein Prolog Programm überführen.
Beispielhafter Sourcecode:
pred1(a).
pred2(a).
pred3(X) :- pred1(a), pred2(a).
Jedoch habe ich jetzt die goal clause (¬pred1(X) ∧ ¬pred2(X) ∧ ¬pred(X)). Muss jetzt kein Sinn ergeben, nur um ein Beispiel zu haben.
Wie würde ich diese im Sourcecode angeben?
Und danke für die Antwort :).
@@callahan7257 Das Beispiel ist keine Horn Klausel, und daher in Prolog nicht direkt hinschreibbar. Prolog unterstützt ausschließlich Horn-Klauseln.
@@ThePowerOfProlog
Sorry, natürlich Disjunktion: (¬pred1(X) ∨ ¬pred2(X) ∨ ¬pred(X)).
@@callahan7257 Das entspricht der Query ?- pred1(X), pred2(X), pred(X). Deklarativ ist das die Behauptung, dass weder pred1(X), noch pred2(X), noch pred(X) gilt. Wenn das widerlegt werden kann, so ist dieses Ziel eine logische Konsequenz des Programms.
I don't understand why you reference "Programming as Theory Building". It is absolutely NOT relevant to the topic at hand. When Naur uses the word "theory" he is speaking of an intuitive understanding of what a large program is supposed to accomplish and mainly speaks about how this theory is separate from things like documentation and source code. He states, for example;
"The dependence of a theory on a grasp of certain kinds of similarity between situations and events of the real world gives the reason why the knowledge held by someone who has the theory could not, in principle, be expressed in terms of rules."
He is adamantly not talking about systems of rules or formal descriptions when he talks of "theories"; he's talking about intuitions instantiated in the minds of programmers, entirely separate from the content of the programs themselves. This completely goes against the way you're using "theory".
Naur states that he uses the word theory "in the sense of Ryle [1949]" (referring to Ryle's book "The Concept of Mind"), and explains in his paper: "Very briefly, a person who has or possesses a theory in this sense knows how to do certain things and in addition can support the actual doing with explanations, justifications, and answers to queries, about the activity of concern." This is very similar to a logical theory: We can use it to answer queries about the domain of interest, give explanations, justifications etc. And further, Naur says: "theory is understood as the knowledge a person must have in order not only to do certain things intelligently but also to explain them, to answer queries about them, and so forth." This further stresses the connection between theory, knowledge, answering queries etc., as we know them from logical theories. He gives a specific example: "A person having Newton's theory of mechanics must thus understand how it applies to the motions of pendulums and the planets, and must be able to recognize similar phenomena in the world, so as to be able to employ the mathematically expressed rules of the theory properly." Note that Naur is explicitly mentioning "the rules of the theory" in the paper. How the subsequent paragraph that you cite relates to these points seems a bit unclear, and in fact its truth could also be questioned: Is it really so clear that the kinds of similarity between situations and events "could not, in principle, be expressed in terms of rules"? Does the term "intuition" occur anywhere in the paper?