Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:instantiation_plus_ground_resolution [2009/05/14 11:57]
vkuncak
sav08:instantiation_plus_ground_resolution [2015/04/21 17:30] (current)
Line 11: Line 11:
 === Ground Instantiation Rule === === Ground Instantiation Rule ===
  
-\[+\begin{equation*}
 \frac{C}{subst(\sigma)(C)} \frac{C}{subst(\sigma)(C)}
-\]+\end{equation*}
 where $C$ is a clause and $\sigma$ is a ground substitution. where $C$ is a clause and $\sigma$ is a ground substitution.
  
Line 21: Line 21:
  
 If $A$ is a ground atom and $C,D$ are ground claues, then If $A$ is a ground atom and $C,D$ are ground claues, then
-\[+\begin{equation*}
 \frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}} \frac{C \cup \{\lnot A\}\ \ \ D \cup \{A\}}
      {C \cup D}      {C \cup D}
-\]+\end{equation*}
  
 Note that this is propositional resolution where propositional variables have "long names" (they are ground atoms). Note that this is propositional resolution where propositional variables have "long names" (they are ground atoms).
  
 ==== 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.
  
  
 
sav08/instantiation_plus_ground_resolution.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice