Logical Foundations of Prolog



Logic is a very broad, interesting and also beautiful topic.

Video: Logic


There is no universally accepted definition for what logic actually is. However, what we can say is that logic is concerened—at least among other things—with the properties of, and the relations between: There are different logics, because changing these components yields different frameworks.

Logic and computation are closely related. For example, we can formulate logical statements about computations, and derive logical consequences from them that correspond to results of the computations.

It can be argued that programming is a form of theory building. See for example Programming as Theory Building by Peter Naur.

Prolog is based on classical first-order predicate logic.

Video: Predicate Logic


In fact, the core of Prolog is restricted to a Turing complete subset of first-order predicate logic called Horn clauses.
Video: Horn Clauses


A Prolog program is a sequence of Horn clauses that define what is true, and what follows from what.

Internally, Prolog uses a proof method called resolution. Resolution is based on the idea of proof by contradiction: To prove a logical consequence of a set of axioms, we assume the opposite of what we want to prove, and show that this contradicts the axioms which we take for granted.

Logically, when Prolog answers a query, it tries to find a resolution refutation of the negated query and the set of clauses that constitute a program. When a refutation is found, it means that the query, with the appropriate bindings, is a logical consequence of the program.

For Horn clauses, resolution can be implemented very efficiently.

Regarded as a theorem prover, Prolog is incomplete in the sense that, in general, not all logical consequences of a theory are found.

Even though Prolog itself is incomplete in general, we can use it to implement complete theorem provers. This is because Prolog is a programming language and can be used to express all known computations.


More about Prolog


Main page