Ground Instantiation plus Ground Resolution as a Proof System

We introduce this proof system as an intermediate step between the naive enumeration algorithm based on Herbrand's theorem and resolution for first-order logic.

Our goal is to avoid explicit enumeration and apply proof system where we do as little search (guessing) as possible, while still being complete.

Definition

The proof system has two rules: ground instantiation and ground resolution.

Ground Instantiation Rule

$\begin{equation*} \frac{C}{subst(\sigma)(C)} \end{equation*}$

where $C$ is a clause and $\sigma$ is a ground substitution.

Ground substitution is of the form $\{x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\}$ where each $t_i$ is a ground term.

Ground Resolution Rule

If $A$ is a ground atom and $C,D$ are ground claues, then

$\begin{equation*} \frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}} {C \cup D} \end{equation*}$

Note that this is propositional resolution where propositional variables have “long names” (they are ground atoms).

Example

Completeness

The proof is based on Herbrand's Expansion Theorem (see also the proof of Compactness for First-Order Logic).

Suppose a set $S$ of clauses is contradictory. By Herbrand's Expansion Theorem and Compactness Theorem for Propositional Formulas, some finite subset $S_0 \subseteq expand(S)$ is contradictory. Then there exists a derivation of empty clause from $S_0$ viewed as set of propositional formulas, using propositional resolution. In other words, there exists a derivation of empty clause from $S_0$ using ground resolution rule. Each element of $S_0$ can be obtained from an element of $S$ using instantiation rule. This means that there exists a proof tree whose leaves are followed by a single application of instantiation rule, and inner nodes contain ground resolution steps.