Prolog is a declarative language that can solve any puzzles and prove theorems.

Imagine a high-level language in which you do not need to indicate HOW to get the result, instead you just need to indicate WHAT you want to get. At the same time, the scope of the language is not limited and the language is able to solve the same problems as any other high-level language, like JAVA. Sounds fantastic, doesn't it? However, there is such a language and it is called PROLOG. Let's see how PROLOG copes with this task by making prologues to some riddles as an example and ask PROLOG to issue a proof of the theorem.

Riddle 1. Simple, mathematical. "?" - an arbitrary mathematical operation (+, -, *, /), the equation is given (((((1? 2)? 3)? 4)? 5)? 6 = 35. Find unknown operations.

We begin to describe what we want to get. Since the sign of the operation is unknown, it will be a parameter.

formula (X1, X2, X3, X4, X5, X6, Sign1, Sign2, Sign3, Sign4, Sign5, Result): -
operation (X1, X2, Sign1, PartialResult1),
operation (PartialResult1, X3, Sign2, PartialResult2),
operation (PartialResult2, X4, Sign3, PartialResult3),
operation (PartialResult3, X5, Sign4, PartialResult4),
operation (PartialResult4, X6, Sign5, Result).

This line describes the formula 1? 2? 3? 4? 5? 6 = Result. In fact, it means: the formula is true if there is a partial result 1, a partial result 2 ... a partial result 4, such that the operations are true. However, the prologue does not know what the operation is, so we will describe in which cases they are correct:

operation (X1, X2, "+", Result): - Result = X1 + X2.
operation (X1, X2, "*", Result): - Result = X1 * X2.
operation (X1, X2, "/", Result): - Result = X1 / X2.
operation (X1, X2, "-", Result): - Result = X1 - X2.

We have described the formula, and now we can ask any questions regarding it. For example, we can ask the following questions: 1) if X1 = 1 X2 = 2 ... X6 = 6 Result = 35 then what operations are possible? 2) the part of the numerical parameters and part of the operations, as well as the result, is indicated, find out what are the missing parameters? 3) all operations, numerical parameters, result are indicated; find out if the formula is correct. In this case, you do not need to worry about how the prologue will find the answer - you just need to ask a question.

So the question is:
askMainQuestion (): -
formula (1,2,3,4,5,6, Sign1, Sign2, Sign3, Sign4, Sign5,35),
stdio :: write (Sign1, Sign2, Sign3, Sign4, Sign5),
stdio :: nl,% new line
fail.

Answer: ++ * ++, + ** + -, *** ++ (To ask a question about numerical parameters, you will have to write a couple more lines, but more on that later.)

Riddle 2. Simple, non-mathematical. Given the names of people and family relationships between them. Find all the brothers.

We indicate specific family relationships:
parent ("Tom", "Jake").
parent ("Jim", "Jake").
parent ("Timmi", "Tom").
uncle ("Tom", "Peter").
brother ("Timmi", "Cartman").

Now we describe what the relationship means:

brother (Man1, Man2): - parent (Man1, Parent), parent (Man2, Parent), Man1 <> Man2.

(Man1 and Man2 are brothers if there is a ManParent who is a parent for Man1 and Man2, and at the same time Man1 is not Man2).

brother (Man1, Man2): - parent (ChildMan1, Man1), uncle (ChildMan1, Man2).

(Man1 and Man2 are brothers, if Man1 has a child, and Man2 is the uncle of this child).

Now ask a question about who the brothers are:

askMainQuestion (): -
brother (X, Y),
stdIO :: write (X, "", Y),
stdio :: nl,
fail.



Program Output: Timmi Cartman, Jake Peter, Tom Jim, Jim Tom. Compare with how much code you would have to write in an imperative programming language.
Now let's look at something more complicated than Hello World's programs and talk about the pitfalls of the prologue.

Riddle 3. On the chessboard there are 8 queens. No queen beats another queen. Find the location of the queens.

First, we describe how the queen can go:

attack (X1, Y1, X2, Y2): - X2 = X1. % the queen can attack if the attacked cell and the original on the same vertical
attack (X1, Y1, X2, Y2): - Y2 = Y1. % the queen can attack if the attacked cell and the original on the same horizontal
attack (X1, Y1, X2, Y2): - abs (X2 - X1, Abs), abs (Y2 - Y1, Abs). % ... on one diagonal

Now we indicate in what cases the queen cannot beat another queen:

any (0).
any (1).
any (2).
any (3).
any (4).
any (5).
any (6).
any (7).
dontAttack (X1, Y1, X2, Y2): -
any (X1), any (Y1), any (X2), any (Y2), not (attack (X1, Y1, X2, Y2)).

This raises the question of why an enumeration of all possible coordinates of the queen (any) is necessary. The fact is that the prologue is designed so that it cannot iterate over all possible numeric or string values. All possible values ​​of the value relative to which the question is asked must be either listed in the code (for example, characters in the example for finding characters), or directly calculated on the basis of the input in the question (such as the result of the formula in the example for finding characters, if do not consider rounding errors in the formula). Of course, such a restriction makes the prologue not the most convenient language for solving equations; however, this was never the main purpose of this language.

So, we have described what it means that “one queen does not beat the other queen”, now we need to indicate that each of the 8 queens does not beat the other 7 queens, however, writing 8 * 7 = 56 rules is tedious, so we describe this rule recursively. We set an empty array and iteratively add one queen to it one by one.

dontAttack ([]).

(if there are no queens, then no queen beats any other)

dontAttack (X, Y, []): - any (X), any (Y).

(if there is one single queen, then he does not beat other queens)

dontAttack (X1, Y1, [X2, Y2 | OtherElements]): -
dontAttack ([X2, Y2 | OtherElements]), dontAttack (X1, Y1, X2, Y2 ), dontAttack (X1, Y1, OtherElements).

(if there is a queen with coordinates X1 and Y1 and an array of queens, then no queen beats the other, if 1) inside the queens array no queen beats the other 2) queen (X1, Y1) does not beat the first queen from the queens array 3) if we remove the first queen from the queens array, then in the set of queens, no queen also beats the other)

dontAttack ([X1, Y1 | OtherElements]): -
dontAttack (X1, Y1, OtherElements).

(if there is a queen with coordinates X1 and Y1 and an array of queens, and no queen beats the other, then if you add the queen to the queens array, no queen will still beat the other)

Now it remains to ask a question about the coordinates of these queens. However, in order not to get many identical answers, differing only in the numbering of queens, let's say that the first queen is in the first column, the second is in the second, etc.:

askMainQuestion (): -
X1 = 0, X2 = 1, X3 = 2, X4 = 3, X5 = 4, X6 = 5, X7 = 6, X8 = 7,
dontAttack ([X1, Y1, X2, Y2, X3, Y3, X4, Y4, X5, Y5, X6, Y6, X7, Y7, X8, Y8]),
stdio :: write (X1, ":", Y1, "-", X2, ":", Y2, "-", X3, ":", Y3, "-" , X4, ":", Y4, "-", X5, ":", Y5, "-", X6, ":", Y6, "-", X7, ":", Y7, "-", X8 , ":", Y8),
stdio :: nl,% new line
fail.

Now let's ask the prologue to prove a simple theorem

Let us prove that a subset of a group is a subgroup if and only if, for any elements A and B from this subset, the product of A by the inverse of B lies in this subset. In order to prove that a subset is a subgroup, three points must be proved: 1) the neutral element lies in the subset 2) for each element in the subset its inverse element lies in the subset 3) the product of any two elements of the subset lies in the subset.

We designate the neutral element as “E” and define the neutral element:

operation (A, “E”, A): - any (A).
operation ("E", A, A): - any (A).

An element is neutral if, when multiplying any element by a neutral one, the initial element is obtained. (for example, in integers 1 is a neutral element).

Add a couple of specific elements.

any ("E").
any ("M").
any ("A").
any ("B").
any ("notA").
any ("notB").

Some other elements were introduced here, in addition to “E”, we explain what these elements are, describing their properties:

ofGroup (“M”, “Set”).
ofGroup ("A", "SubSet").
ofGroup ("B", "SubSet").

A and B are elements from a subset, M is an element from a set.

obratni ("B", "notB").
obratni ("notB", "B").
obratni ("A", "notA").
obratni ("notA", "A").
obratni ("E", "E").

“NotA” is the inverse of “A”, “notB” is the inverse of “B”

Now we define the inverse element:

operation (A, B, “E”): - obratni (A, B).
operation (B, A, “E”): - obratni (A, B).

And the inverse to B, if, when A is multiplied by B, a neutral element is obtained (for example, 2 * 0.5 = 1). As you can see, A and B do not have quotation marks here, which means that they do not mean specific elements “A” and “B”, but any elements.

Subset Definition:

ofGroup (X, “Set”): - ofGroup (X, “SubSet”).

(an element belongs to a set if it belongs to a subset)

Now we point out that for any elements A and B from a subset the result of the product of A and the inverse of B lies in this subset (by hypothesis of the theorem).

ofGroup (C, “SubSet”): - obratni (B, NotB), operation (A, NotB, C), ofGroup (A, “SubSet”), ofGroup (B, “SubSet”), stdio :: write (C , "is from subset, because", A, "*", NotB, "=", C, "."), stdio :: nl.

As you can see, here we added the output to the screen (stdio :: write), this was done to trace the actions of the prolog, to find out how the prolog used this rule to see the progress of the proof of the theorem.

Now it remains to prove three points from the theorem.
We ask a question about the neutral element “E”:

firstQuestion (): -
ofGroup (“E”, “SubSet”),
stdio :: write (“E is from subset”) ,!
..
firstQuestion (): - stdio :: write ("E is NOT from subset").

About the inverse element:

secondQuestion (): -
ofGroup ("notA", "SubSet"),
stdio :: write ("notA is from subset") ,!
..
secondQuestion (): - stdio :: write ("NotA is NOT from subset ").

Here you might have a question: you need to prove that for any element of the subset, its inverse element belongs to the subset, however, in the prologue question, we indicated one single concrete element - “notA”. In fact, since we did not impose any restrictions on the “notA” element (except that it is the inverse element to the element belonging to the subset), then if we take any inverse element, then all the same reasonings that we applied to notA. Mathematicians often use this technique to prove theorems. This technique is especially important for Prolog, because it cannot iterate over all string and numerical values.

Well, now we ask a question about the membership of a subset of the result of the product of two elements from the subset:

operation ("A", "B", "AB").
thirdQuestion (): -
operation ("A", "B", AB),
ofGroup (AB, "SubSet"),
stdio :: write ("A * B is from subset") ,!
..
thirdQuestion (): - stdio :: write ("A * B is NOT from subset").

We start ... And the program crashes, hanging from a stack overflow! Let's see why this happened. In fact, the prologue is trying to find a solution by enumerating the facts entered into it. When searching for the answer to the main question, the prologue goes through all the facts, at least somehow related to the question. If it is not known whether a fact is true, he, in turn, goes through all the facts related to this fact. And so, until it comes to unconditional facts, for example, to obratni (“A”, “notA”) - “notA” is the opposite of “A”. The question was asked: does the neutral element belong to a subset. The prologue sees the rule ofGroup (C, "SubSet"): - obratni (B, NotB), operation (A, NotB, C), ofGroup (A, "SubSet"), ofGroup (B, "SubSet") and understands that if we substitute a neutral element as C and find A and B that satisfy the rule, then, according to the rule, the neutral element will belong to a subset. The first element among the existing ones is exactly the reverse (any ("E")), so Prolog selects it as B. So, obratni ("E", NotB). After that, Prolog asks the question: what element is the inverse of "E"? - and finds the answer (obratni ("E", "E")). So, NotB = "E". After that, Prolog goes further by the rule and sees operation (A, NotB, C), in this case operation (A, "E", "E") and asks the question: which element when multiplied by "E" gives "E" - and finds the answer "E" (from the rule operation (A, "E", "E"): - obratni (A, "E") and the fact obratni ("E", "E").). So, A = "E". We follow the original rule further: ofGroup (A, "SubSet"), in this case ofGroup ("E", "SubSet"). And here Prolog tries to answer the same question, what we asked at the beginning - does “E” belong to “SubSet” (neutral to a subgroup)? The program goes in cycles and begins to sort through the same facts and rules again, walking in a vicious circle. Well, let's rewrite the original rule a bit:

ofGroup (C, "SubSet"): - obratni (B, NotB), NotB <> "E", NotB <> "M", operation (A, NotB, C), ofGroup (A, "SubSet"), ofGroup (B, “SubSet”), stdio :: write (C, "is from subset, because", A, "*", NotB, "=", C, "."), Stdio :: nl.

Now you can not use “E” and “M” as NotB, and the program will not hang (yes, yes, it also hangs on “M”).
After that, the program at the same second gives a proof of three points of the theorem:

E is from subset, because B * notB = E.
E is from subset
(A and B are in the subset, so the product of A and the inverse to B are in the subset. In this case, instead of A and B, we take the same element “B.” The proof can be made more detailed if we add more write commands to the rules)

E is from subset,
notA is from subset, because E * notA = notA.
notA is from subset

E is from subset, because B * notB = E.
notB is from subset, because E * notB = notB.
AB is from subset, because A * B = AB.
A * B is from subset

Conclusion

Prolog is a wonderful declarative language, however constant hangs do not honor him (if anyone knows how to deal with this, please share in the comments). In fact, the task of finding cycles in graphs has been solved a long time ago, and eliminating the problem at the language level is a completely solvable problem! If this problem were solved, it would be possible to compile a knowledge base of all known mathematical facts, and ask any questions! Or for example, change one of the basic axioms of mathematics and instantly find out how other laws change (a la Lobachevsky’s geometryin no time)! Of course, I am somewhat optimistic, and the language needs a bit more improvements, but still ... For example, one of the possible improvements: Prolog must be able to not only get out of the loop, but also be able to process the loop in accordance with certain rules in order to operate with infinite sequences that satisfy condition of the theorem, as for example in the Bolzano-Weierstrass theorem . However, in the current state, is Prolog viable for anything at all: it took me even more time to find the reasons for the loops than to prove the theorem itself! (IMHO, just my opinion)