Differences

This shows you the differences between two versions of the page.

--- sav08:instantiation_plus_ground_resolution [2009/05/14 11:57]
vkuncak
+++ sav08:instantiation_plus_ground_resolution [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== 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 ===
-\[
-\frac{C}{subst(\sigma)(C)}
-\]
-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
-\[
-\frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}}
-     {C \cup D}
-\]
-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|Compactness Theorem for Propositional Formulas]], there is 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.