# Predicate Calculus, Resolution Theorem Proving and Prolog

Proposition calculus is concerned with logical relations between elementary or atomic statements known as propositions.

Predicate calculus, or first-order logic, introduces more structure into the basic statements that are joined together by logical connectives.
In essence, we replace propositions by *predicate expressions* which may involve functions and variables.

For example, consider the statement that "\(x\) is greater than the sum of \(y\) and \(z\)."

A predicate calculus representation could be the following.

- \(P(x, f(y, z))\), where
- \(P\) is a predicate meaning "greater than"
- \(f\) is a function meaning "sum".

In addition, predicate calculus introduces two new logical formula types using quantifiers.

\(\exists x P(x)\) means that the statement \(P(x)\) is true for at least one possible value of \(x\).

\(\forall x P(x)\) means that the statement \(P(x)\) is true for all possible values of \(x\).

## Resolution Theorem Proving

Resolution theorem proving is a symbolic computing technique for proving statements in predicate calculus. It is also the basis underlying the programming language Prolog (programming in logic).

The method of resolution theorem proving first involves a transformation of logical formulas to a canonical representation
called *conjunctive normal form* (CNF).
The following steps are applied.

- Elimination of implications and equivalences
- Inward propagation of negations
- Variable standardization
- Elimination of existential quantifiers
- Elimination of universal quantifiers

Once this process is complete, the CNF formulas may then be converted to simpler representation called the clause-form-equivalent representation. In this representation, the entire set of original formulas is represented by a list of clauses. The clauses themselves are lists of literals, positive and negated predicate expressions. Each clause is implicitly a disjunction. All other logical connectives are eliminated.

The resolution inference rule is then systematically applied to the set of clauses to derive new clauses. Ultimately, the process completes when a null disjunct is found, i.e., a single clause which is empty.