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.