LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:instantiation_plus_ground_resolution [2009/05/14 11:57]
vkuncak
sav08:instantiation_plus_ground_resolution [2009/05/14 13:40]
vkuncak
Line 29: Line 29:
  
 ==== Example ==== ==== Example ====
 +
  
  
Line 35: Line 36:
 The proof is based on [[Herbrand'​s Expansion Theorem]] (see also the proof of [[Compactness for First-Order Logic]]). 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.+Suppose a set $S$ of clauses is contradictory. ​ By [[Herbrand'​s Expansion Theorem]] and [[Compactness Theorem|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.