12. Logic Programming¶
12.1. Feature of an ideal logic progarmming language¶
Declarative programming
Programs describe rules to get the result instead of step-by-step instractions.
Rules can be written in any order.
Non-deterministic behavior
You may explore several possibilities for a single input.
12.2. Prolog¶
Prolog is a language based on the first-order predicate logic (cf. First-Order Logic in Artificial Intelligence - GeeksforGeeks). Execution of a program corresponds to the proof of a theorem.
12.2.1. Program¶
A rule is of the form:
p :- q1, q2, ... , qn.
where each of p, q1, q2, …, qn is of the form pred(arg1, arg2, ..., argn).
It means “To show p, show q1, q2, …, qn”.
In case of n=0, it is called a fact.
A program is a set of rules (and facts).
“Human is mortal” and “Socrates is a human”
mortal(X) :- human(X).
human(socrates).
12.2.2. Query¶
A query is of the form:
?- q1, q2, ... , qn.
If all of q1, q2, … , qn can be shown from the given program, the output is “Yes”; otherwise “No”.
Is Socrates mortal?
?- mortal(socrates).
Yes
If the query contains variables, the output displays assignments to the variables that make the query true.
Who is mortal?
?- mortal(X).
X = socrates
12.2.3. More complicated example¶
The predicate append appends two lists into one.
[]is an empty list.[ A | B ]denotes a list whose first element isAand the remaining part isB.
append([], Y, Y).
append([H | X], Y, [H | Z]) :- append(X, Y, Z).
Does appending [a, b] and [c, d] result in [a, b, c, d] ?
?- append([a, b], [c, d], [a, b, c, d]).
yes
What is the result of appending [a, b] and [c, d] ?
?- append([a, b], [c, d], Z).
Z = [a, b, c, d]
Appending [a, b] and what result in [a, b, c, d] ?
?- append([a, b], Y, [a, b, c, d]).
Y = [c, d]
Appending what and [c, d] result in [a, b, c, d] ?
?- append(X, [c, d], [a, b, c, d]).
X = [a, b]
12.3. Theoretical foundation¶
12.3.1. Logical formula¶
A rule corresponds to a logical formula called Horn clause:
which is equivalent to:
A query corresponds to a logical formula called Goal clause:
which is equivalent to:
12.3.2. Proof¶
In order to show Q is true, a proof by contradiction is used.
We give a query
?- Qwhich is equivalent to \(\neg Q\).An automated theorem proving algorithm called resolution is used to derive a contradiction from \(\neg Q\) and the program \(P\).
\(\neg Q'\) (an instance of \(\neg Q\)) is produced when necessary.
If contradiction can be derived, we can say \(Q'\) is true.
We also get the assignment to variables that is used to produce \(\neg Q'\).
12.4. Issues with Prolog¶
12.4.1. Derivation order¶
To implement declarative programming, it is required to choose derivation steps in non-deterministic manner. However, Prolog adopts deterministic way of choosing next steps (top to bottom, left to right) because of simplicity and efficiency. So, a program may fall into an infinite loop depending on the order of rules.
Order sensitive program
When the predicate parent is defined, we want to apply it transitively to define a new predicate ancestor.
The following program falls into an infinite loop:
ancestor(X, X).
ancestor(X, Y) :- ancestor(Z, Y), parent(X, Z).
parent(alice, bob).
parent(bob, charlie).
?- ancestor(alice, charlie).
It should be:
ancestor(X, X).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
parent(alice, bob).
parent(bob, charlie).
?- ancestor(alice, charlie).
12.4.2. Negation¶
The resolution algorithm only deal with Horn clauses, so there should be no negative literal in the body part of a rule. We need some tricks to use not operator in a program.
The closed-world assumtion is the assumption that all the true statements are known to be true. Therefore, what is not known to be true is false.
In Prolog, based on the closed-world assumption, if we cannot prove \(Q\), we think \(\neg Q\) is true. This method is called negation as failure.
Alice is not mortal
If the program does not contain information about Alice, the computer concludes Alice is not mortal based on the closed-world assumption.
mortal(X) :- human(X).
human(socrates).
?- mortal(alice).
no
?- not(mortal(alice)).
yes