Skip to Content

PL: Logic Programming

From old CS 471 notes…

Logic Programming Languages

Mathematical logic has been used in mathematics and philosophy for hundreds of years to “prove” statements of believed truth.

Usual process:

  • Assert some “ground facts” as accepted truth. Hopefully everyone agrees with these;
  • Assert some “propositions” that connect the facts. Hopefully everyone agrees with these too;
  • Assert some desired property (“theorem”);
  • Use rules of logical inference to prove that the theorem is true – i.e., it can be supported by the assumed ground facts and the connecting rules.

Logic programming uses this basic model as the underlying model of computation that it supports.

Logic programming is extremely declarative rather than imperative: one should not care at all how the underlying computer deduces the truth or falseness of some theorem, only that it did so by correctly applying the logical rules of inference.

In practice, logic programming is not necessarily that perfect; sometimes the programmer needs to know how the underlying logic engine is going to interpret the program.

Logic

Consider the following logical inference:

Barney is a dog.
All dogs are mammals.
Therefore, Barney is a mammal.

The last line is the “computed” inference that is a derived statement of truth based on the first two assumed propositions, and the built-in axioms of logical inference.

To write this more formally, we might say:

dog(barney).
forall(X), dog(X) -> mammal(X).
mammal(barney)?

Here, we are asserting a fact that Barney is a dog, and an proposition that uses a universallly quantified variable to declare that anything that is known to be a dog implies that it is known also to be a mammal.

The final line is a query to our logic computation engine asking it if barney is a mammal. If it is working correctly it should return “True”.

Two very important components in a logic “computation”: implication and quantification.

Implication is that “->” operator that says that the truth of something implies the truth of something else.

The logical rule of Modus Ponens allows us to infer the implication: if “A -> B”, and A is known to be true, then we can infer that B is true.

Note that if A is false, nothing about B is known. Only if there is a bidirectional implication “A <-> B” (we say “A if and only if B”) can we infer that the falseness of one implies the falseness of the other. Single implication never implies falseness.

Quanification lets us make and infer generalized statements: two forms exist: universal (for-all) and existential (there-exists) quantification.

Universal says something about all entities, while existential simply says that there is at least one entity that satisfies a statement.

An incorrect inference of quantification is:

Joe is human.
Bob is human.
Joe is over six feet tall.
Bob is over six feet tall.
Therefore, all humans are over six feet tall.

In the above, only existential quantification can be inferred: there exists a human such that the human is over six feet tall.

Normal logical operators of AND, OR, NOT are also usable in logical assertions:

dog(X) AND wellfed(X) -> happy(X).

dog(X) OR cat(X) -> mammal(X).

dog(X) -> NOT cat(X).

Wikipedia has pages on Propositional Logic (no quantifiers) and First-order Logic (with quantifiers), and lots of other logic pages.

Wikipedia has a decent page with a list of inference rules, but they are in a hard to read mathematical form.

The propositional logic page has a similar list in a table with names and english descriptions (but it is missing quantification rules).

Horn Clauses

A Horn Clause is a particular form of logical statement where a conjunction (the AND operator) of one or more clauses implies some other single positive clause. The first statement above is a Horn clause, but the second two are not (the second uses disjunction, while the third implies a negative clause).

Horn clauses are the basis for most logic programming systems because they naturally lend themselves to certain computational approaches, and because almost any logical system can be represented by them.

In logic programming, Horn clauses are usually written backwards:

happy(X) :- dog(X), wellfed(X).

We read that as “happy(X) if dog(X) and wellfed(X)”. The reason for this order is because it is similar to the function name/body order. The truth of the “function” happy can be “computed” by going into the “body” and computing the truth of “dog” and of “wellfed”.

How to represent disjunction? Easy: separate Horn clauses:

mammal(X) :- dog(X).
mammal(X) :- cat(X).

Here, mammal(X) is found to be true if either of the Horn clauses are found to be true.

Prolog: a Logic Programming Language

Prolog is just one, but easily the most popular, logic programming language. (Wikipedia:Prolog has a good summary, with good links at the bottom.)

It is based on Horn clauses, it uses the comma as above to represent AND, and uses separate Horn clauses for OR.

In Prolog, identifiers beginning with lowercase are atoms, or constants. Identifiers beginning with uppercase are variables, or unknowns.

Similar to functional programming, variables are not stateful storage locations that change values, but simply identifiers that represent some “eventually known” value.

For data structures, Prolog is list-based, just like many functional programming languages. Identifier variables meant to represent lists are always named with an “s” at the end; e.g., “Xs” is a list of “X” elements.

To read in a Prolog file, use consult(basefilename) or compile('fullfilename') or ['filename'].

To stop a Prolog interpreter, use halt.

Computational Order of Prolog

When understanding how a Prolog computes, and most especially understanding how it can be more or less efficient, the order of Horn clause evaluation is important.

Within a Horn clause body, individual conjuncted rules (AND) are always evaluated left to right.

With multiple Horn clauses for a single rule name (OR), the individual clauses are always evaluated top to bottom. (if you imagine they are written in a file.)

Remember, for pure logical inference, order does not matter. However, for practical computing needs, order can greatly effect efficiency, and must be used to disambiguate and simplify the computational model.

Major assumption: the Closed World Assumption

In pure logic, if something is not known, the correct answer is “Don’t know”.

E.g., if we have

dog(barney).
dog(hope).

and we ask “dog(fido)?”, the logic answer is “Don’t know”.

In programming, we typically want our programs to provide an answer!

So, logic programming languages almost always operate under the closed world assumption, which states that everything needed to be known for the program has been provided, and anything else can assumed to be false.

See Wikipedia:Closed_world_assumption.

Operationally, this relates to the notion of negation as failure; the not(P) clause of Prolog succeeds (returns true) if P is failed to be proved true.

In other words, you do not assert “false” facts, only true facts. Then, everything else is assumed false.

See Wikipedia:Negation_as_failure.

Two big concepts: unification and backtracking

Logic programming is centered on these two concepts.

Unification is the process of finding “useful” values for variables, and being sure they satisfy all constraints.

The same variable name in multiple conjucted rule in a Horn clause body always refers to the same variable, so if the variable’s value is unknown, Prolog must infer a value that will satisfy all the rules in which it is used.

Backtracking is the process of backing up the logical inference steps and trying alternative paths (values or clauses) to see if some other choices might satisfy a query or intermediate clause.

In the Prolog interactive interpreter, when evaluating a query, if Prolog finds an answer it prints it out.

Unification and backtracking can often yield surprising results!

Mathematical operations in Prolog

For “normal” logical deductions, allowing Prolog to search for values which satisfy some relations is a good thing.

For math, however, we usually want to specify a computation to be performed, not simply a relation to hold.

E.g., with real values and the expression (x < 7 && x > 5), we wouldn’t want Prolog to backtrack and try all of the immensely large set of representable real values that satisfy the expression!

Prolog arithmetic relations: <, >, <=, >=, =:=, =\=

Prolog arithmetic relational operators only test currently unified (bound) values to see if they satisfy the relation, they cannot “generate” a value that satisfies the relation.

Prolog has the is “operator”, which immediately unifies (assigns) an unknown variable to a mathematical value computed by the right hand side expression.

CUT: An extra-logical Prolog operator

When writing Prolog programs, sometimes we know exactly where in the inference computation where we should have (or want) a single known solution.

For efficiency, we want to stop Prolog from searching for alternatives.

The answer is the CUT operator, which is an exclamation point (!).

The ! operator “cuts off” any search tree branches above it that have not yet been explored. Therefore, the only computational path left is the current one, and it alone will produce a result (or not).

Logic Programming Summary

Execution model (or the “virtual machine” you are programming) is logical inference over facts and Horn clause rules.

A “program” is very declarative – it simply declares the logical properties that hold, and allows the inference engine to figure out how to make them true.

As part of inference, data values are generated that make the rules true (if possible).

Unification “unifies” unknowns with data values that (hopefully) make the goal rule(s) true.

backtracking tries alternative data values and alternative rules to discard failed computational paths and/or find alternative successful paths with alternative solutions.