Logical Foundations of Prolog
Logic is a very broad, interesting and also beautiful
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.
This is the formalization of languages according to rules. It
includes for example defining what a formula or a sentence looks
This is assigning meaning to the
syntactic constructs of languages. This includes
defining how sentences are interpreted, and stating under what
conditions they are true.
This stems from the Latin
verb inferre, which means "to carry forward". An
inference rule allows us to derive logical consequences
from premises, i.e., to bring premises to conclusions.
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.
In fact, the core of Prolog is restricted to a
Turing complete subset of first-order predicate logic
called 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