Logic Programming using Prolog

This is an introductory page to:

According to Wikipedia on Logic Programming and Prolog:

  1. Logic programming is a type of programming paradigm which is largely based on formal logic.
  2. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain.
  3. Prolog is a general-purpose logic programming language associated with artificial intelligence and computational linguistics.
  4. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily as a declarative programming language: the program logic is expressed in terms of relations, represented as facts and rules.
  5. Prolog was one of the first logic programming languages, and remains the most popular among such languages today, with several free and commercial implementations available. The language has been used for theorem proving, expert systems, term rewriting, type inference, and automated planning, as well as its original intended field of use, natural language processing.

Logic Programming

A logic program is written as a set of logical sentences known as axioms

Some axioms correspond to what are generally known as “rules”.

Some axioms correspond to what are generally known as “facts”.

Axioms of propositional logic consist of atoms which may be connected or negated ('¬')

A literal represents the truth or falsehood of an atomic proposition.

The explicit representation of falsehoods is required by the open-world assumption.

The well-founded semantics defines a means of handling contradiction using a third truth-value.

In effect, the  well-founded semantics allows mixing of the open- and closed-world assumptions.

Predicate calculus allows for a term to be a variable.

First-order logic is a predicate calculus that allows quantified variables as the arguments of atoms. 

Higher-order logics may allow for variables to range over functions or predicates.

Defeasible logics allow for exceptions to axioms.


Prolog is simply a restricted form of logic in which axioms in which:

In practice, Prolog provides extensions such as aggregation.

XSB Prolog supports both open- and closed-world interpretations of negation.

Flora-2 extends XSB Prolog by allowing first-order logic expressiveness in antecedents.

Theorem Proving

Theorem proving, in general, is a sophisticated area.  In its pure form it has limited commercial application, as discussed at Wikipedia.  The primary applications are rigorous proofs in mathematics and in circuit verification, but there are important commercial and regulatory applications in compliance, especially with regard to safety (e.g., in aerospace & aviation).

Nonetheless, theorem proving techniques are important and powerful in many areas of artificial intelligence.  When we say techniques, we mean inference using theorem proving techniques such as unification and resolution.

One of our favorite works is Mark Stickel’s and Jerry Hobb’sInterpretation as Abduction”. 

In the course of that work, Stickel developed a Prolog technology theorem prover (PTTP). 

TTP differs from Prolog in its use of

  1. unification with the occurs check for soundness,
  2. depth-first iterative deepening search instead of unbounded depth-first search to make the search strategy complete, and
  3. the model elimination inference rule that is added to Prolog inferences to make the inference system complete.

The PTTP approach is even better today using XSB Prolog.  It is not a theorem prover for proofs many dozens or hundreds of steps long but performs well for answering questions or making decisions that require fewer inferences, which includes most questions and decisions, in practice.

[1] the difference between functions and predicates is a detail discussed here

[2] Note that implication adds no expressive power since A→B is logically equivalent to ¬AB.

Copyright © 2018 by Automata, Inc. All rights reserved.