Logical Consequence by Satisfiability Preserving Transformations

To show that C is a logical consequence of Ax, it is sufficient to:

Show that S' = Ax U {~C} is unsatisfiable.

Thus the ability to detect that a set of formulae is unsatisfiable, is important.

A satisfiability preserving transformation (SPT) takes a set of formulae and transforms it to a new set, such that if the original set is satisfiable then so is the transformed set. Conversely, if the transformed set is unsatisfiable then so is the original set. If, by repetitive use, the application of SPTs produces a set that is obviously unsatisfiable (e.g., containing a contradiction or FALSE) from a set of formulae, then, iteratively, this means that the very original set is also unsatisfiable. If the original set is of the form Ax U {~C}, this establishes that C is a logical consequence of Ax.

The operation of applying a sound inference rule to parents from a set, and then adding the inferred formula back into the set, is a SPT (think why!). (There are other SPTs, but this is an important one.) Thus sound inference rules form the basis of a a simple algorithm for establishing logical consequence. The basic procedure is:

Put the axioms and negated conjecture in the initial set
While a contradiction has not been found
    Copy formulae from the set
    Generate logical consequences
    Put logical consequences into the set

The process of finding a contradiction is called finding a refutation. An inference system is refutation complete if, by repetitive use, it can infer a contradiction from every unsatisfiable set.

Note: A complete inference system can infer all logical consequences, while a refutation complete inference system can only check (via the unsatisfiability idea) for logical consequence.

Clause Normal Form

Clause Normal Form (CNF) is a sub-language of 1st order logic. A clause is an expression of the form L₁ |... | L_m where each L_i is a literal.

There are satisfiability preserving transformations from 1st order logic to CNF, i.e., a set of formulae is satisfiable iff its clause normal form is satisfiable.

To show that C is a logical consequence of Ax, it is sufficient to:

Show that S' = Ax U {~C} is unsatisfiable.

S' is unsatisfiable iff S = CNF(S') is unsatisfiable

Show that S is unsatisfiable.

The Herbrand World

The Herbrand universe of a 1st order language is the set of all ground terms. If the language has no constants, then the language is extended by adding an arbitrary new constant. It is enumerable, and infinite (the same cardinality as the integers) if a functor of arity greater than 0 exists. The Herbrand base of a 1st order language is the set of all ground atoms formed using elements of the Herbrand universe as arguments. Like the Herbrand universe, it is enumerable, and infinite if the Herbrand universe is infinite and there is a predicate symbol of arity greater than 0.

A Herbrand interpretation has

D = the Herbrand universe,
F = the identity function,
R = a subset of the Herbrand base that is TRUE.

R defines a mapping from the Herbrand base to {TRUE,FALSE}.

A set of clauses has a model iff it has a Herbrand model.

To show that C is a logical consequence of Ax, it is sufficient to:

Show that S = CNF(Ax U {~C}) is unsatisfiable.

A set of clauses has a model iff it has a Herbrand model, so

Show that S is Herbrand unsatisfiable.

Resolution Inference Rules

Resolution is an inference rule (with many variants) that takes two or more parent clauses and soundly infers new clauses. A special case of resolution is when the parent causes are contradictory, and an empty clause is inferred. Resolution is a general form of modus ponens.

Resolution is a sound inference rule, i.e., if a set S of clauses is Herbrand satisfiable, then S U {a resolvant from S} is also Herbrand satisfiable..

To show that C is a logical consequence of Ax, it is sufficient to:

Show that S = CNF(Ax U {~C}) is Herbrand unsatisfiable.

If a set S U {a resolvant from S} of clauses is Herbrand unsatisfiable, then S is Herbrand unsatisfiable, so

Repeatedly do resolution on S and its resolvants, and hope an obviously unsatisfiable set is produced, e.g., one containing an empty clause.

The CNF Saturation Procedure

The basic CNF saturation procedure is:

While a refutation has not been found
    Copy two clauses from the set
    Generate all logical consequences, e.g., by resolution
    Put logical consequences into the set

Note the "Copy", indicating that a clause may be used multiple times with a new set of variables each time.

The CNF saturation procedure is refutation complete

To show that C is a logical consequence of Ax, it is sufficient to:

Repeatedly do resolution on S = CNF(Ax U {~C}) and its resolvants, and hope an obviously unsatisfiable set is produced, e.g., one containing an empty clause.

The CNF saturation procedure is refutation complete, so

Confidently repeatedly do the CNF saturation procedure on S until an empty clause is produced

Exam Style Questions

What does it mean for an inference system to be {sound, complete, refutation complete}? Which of these properties are desireable in an CNF based ATP system?