- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav08:deriving_propositional_resolution [2008/03/19 17:18] tatjana |
sav08:deriving_propositional_resolution [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 4: | Line 4: | ||

We are extending the notion of [[Substitution Theorems for Propositional Logic|substitution on formulas]] to sets of formulas by | We are extending the notion of [[Substitution Theorems for Propositional Logic|substitution on formulas]] to sets of formulas by | ||

- | \[ | + | \begin{equation*} |

subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \} | subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \} | ||

- | \] | + | \end{equation*} |

To make intuition clearer, we will next use quantification over potentially infinitely many variables and conjunctions over infinitely many formulas. | To make intuition clearer, we will next use quantification over potentially infinitely many variables and conjunctions over infinitely many formulas. | ||

Line 17: | Line 17: | ||

The condition that $S$ is satisfiable is equivalent to the truth of | The condition that $S$ is satisfiable is equivalent to the truth of | ||

- | \[ | + | \begin{equation*} |

\exists p_1,p_2,p_3,\ldots.\ \bigwedge_{F \in S} F | \exists p_1,p_2,p_3,\ldots.\ \bigwedge_{F \in S} F | ||

- | \] | + | \end{equation*} |

which, by changing the order of quantifiers, is: | which, by changing the order of quantifiers, is: | ||

- | \[ | + | \begin{equation*} |

\exists p_2,p_3,\ldots.\ \exists p_1. \bigwedge_{F \in S} F | \exists p_2,p_3,\ldots.\ \exists p_1. \bigwedge_{F \in S} F | ||

- | \] | + | \end{equation*} |

By expanding existential quantifier, $\exists p_1. \bigwedge_{F \in S} F$ is eqivalent to | By expanding existential quantifier, $\exists p_1. \bigwedge_{F \in S} F$ is eqivalent to | ||

- | \[ | + | \begin{equation*} |

((\bigwedge_{F \in S} subst(p_1 \mapsto {\it false},F)) \lor | ((\bigwedge_{F \in S} subst(p_1 \mapsto {\it false},F)) \lor | ||

(\bigwedge_{F \in S} subst(p_1 \mapsto {\it true},F)) | (\bigwedge_{F \in S} subst(p_1 \mapsto {\it true},F)) | ||

- | \] | + | \end{equation*} |

which, by distributivity of $\lor$ through $\land$ is: | which, by distributivity of $\lor$ through $\land$ is: | ||

- | \[ | + | \begin{equation*} |

\bigwedge_{F_1,F_2 \in S} | \bigwedge_{F_1,F_2 \in S} | ||

(subst(p_1 \mapsto {\it false},F_1) \lor | (subst(p_1 \mapsto {\it false},F_1) \lor | ||

subst(p_1 \mapsto {\it true},F_2)) | subst(p_1 \mapsto {\it true},F_2)) | ||

- | \] | + | \end{equation*} |

Let | Let | ||

- | \[ | + | \begin{equation*} |

ProjectForm(F_1,F_2,p) = (subst(p \mapsto {\it false},F_1) \lor | ProjectForm(F_1,F_2,p) = (subst(p \mapsto {\it false},F_1) \lor | ||

(subst(p \mapsto {\it true},F_2)) | (subst(p \mapsto {\it true},F_2)) | ||

- | \] | + | \end{equation*} |

Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,p)$ defined by | Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,p)$ defined by | ||

- | \[ | + | \begin{equation*} |

ProjectSet(S,p) = \{ ProjectForm(F_1,F_2,p) \mid F_1,F_2 \in S \} | ProjectSet(S,p) = \{ ProjectForm(F_1,F_2,p) \mid F_1,F_2 \in S \} | ||

- | \] | + | \end{equation*} |

==== Projection Proof Rules ==== | ==== Projection Proof Rules ==== | ||

- | Th justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule. We write such rule: | + | Above we justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule. We write such rule: |

- | \[ | + | \begin{equation*} |

\frac{F_1 \; \ F_2} | \frac{F_1 \; \ F_2} | ||

{(subst(p \mapsto {\it false},F_1) \lor | {(subst(p \mapsto {\it false},F_1) \lor | ||

(subst(p \mapsto {\it true},F_2))} | (subst(p \mapsto {\it true},F_2))} | ||

- | \] | + | \end{equation*} |

The soundness of projection rule follows from the fact that | The soundness of projection rule follows from the fact that | ||

for every interpretation $I$, if $I \models S$, then also $I \models ProjectSet(S,p)$. | for every interpretation $I$, if $I \models S$, then also $I \models ProjectSet(S,p)$. | ||

Applying the projection rule we obtain formulas with fewer and fewer variables. We therefore also add the "ground contradiction rule" | Applying the projection rule we obtain formulas with fewer and fewer variables. We therefore also add the "ground contradiction rule" | ||

- | \[ | + | \begin{equation*} |

\frac{F} | \frac{F} | ||

{{\it false}} | {{\it false}} | ||

- | \] | + | \end{equation*} |

- | where $F$ is formula that has no variables and that evaluates to //false// (ground contradictory formula). This rule is trivially sound. | + | where $F$ is formula that has no variables and that evaluates to //false// (ground contradictory formula). This rule is trivially sound: we can never |

+ | have a model of a ground formula that evaluates to false. | ||

==== Iterating Rule Application ==== | ==== Iterating Rule Application ==== | ||

Given some enumeration $p_1,p_2,\ldots$ of propositional variables in $S$, we define the notion of applying projection along all propositional variables, denoted $P^*$: | Given some enumeration $p_1,p_2,\ldots$ of propositional variables in $S$, we define the notion of applying projection along all propositional variables, denoted $P^*$: | ||

- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |

P_0(S) = S \\ | P_0(S) = S \\ | ||

P_{n+1}(S) = ProjectSet(P_n(S),p_{n+1}) \\ | P_{n+1}(S) = ProjectSet(P_n(S),p_{n+1}) \\ | ||

P^*(S) = \bigcup_{n \geq 0} P_n(S) | P^*(S) = \bigcup_{n \geq 0} P_n(S) | ||

- | \end{array}\] | + | \end{array}\end{equation*} |

- | | + | |

==== Completeness of Projection Rules ==== | ==== Completeness of Projection Rules ==== | ||

Line 90: | Line 87: | ||

Consider any finite $T \subseteq S$. We show that $T$ it is satisfiable. Let $T = \{F_1,\ldots,F_n\}$ and let $FV(F_1) \cup \ldots \cup FV(F_n) \subseteq \{p_1,\ldots,p_M\}$. Consider the set | Consider any finite $T \subseteq S$. We show that $T$ it is satisfiable. Let $T = \{F_1,\ldots,F_n\}$ and let $FV(F_1) \cup \ldots \cup FV(F_n) \subseteq \{p_1,\ldots,p_M\}$. Consider the set | ||

- | \[ | + | \begin{equation*} |

A = \bigcup_{i=1}^M P_i(S) | A = \bigcup_{i=1}^M P_i(S) | ||

- | \] | + | \end{equation*} |

By definition of $P_i$, we can show that the set $A$ contains the conjunctive normal form of the expansion of | By definition of $P_i$, we can show that the set $A$ contains the conjunctive normal form of the expansion of | ||

- | \[ | + | \begin{equation*} |

\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n) | \exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n) | ||

- | \] | + | \end{equation*} |

Each of these conjuncts is a ground formula (all variables $p_1,\ldots,p_M$ have been instantiated), so the formula evaluates to either //true// or //false//. By assumption, $P^*(S)$ and therefore $A$ do not contain a ground contradiction. Therefore, each conjunct of $\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)$ is true and $T$ is satisfiable. | Each of these conjuncts is a ground formula (all variables $p_1,\ldots,p_M$ have been instantiated), so the formula evaluates to either //true// or //false//. By assumption, $P^*(S)$ and therefore $A$ do not contain a ground contradiction. Therefore, each conjunct of $\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)$ is true and $T$ is satisfiable. | ||

Line 110: | Line 107: | ||

Instead of arbitrary formulas, use clauses as sets of literals. The projection rule becomes | Instead of arbitrary formulas, use clauses as sets of literals. The projection rule becomes | ||

- | \[ | + | \begin{equation*} |

\frac{C_1 \; \ C_2} | \frac{C_1 \; \ C_2} | ||

{(subst(p \mapsto {\it false},C_1) \cup | {(subst(p \mapsto {\it false},C_1) \cup | ||

(subst(p \mapsto {\it true},C_2))} | (subst(p \mapsto {\it true},C_2))} | ||

- | \] | + | \end{equation*} |

If $C$ is a clause, then | If $C$ is a clause, then | ||

- | \[ | + | \begin{equation*} |

subst(\{p \mapsto {\it false}\},C) | subst(\{p \mapsto {\it false}\},C) | ||

- | \] | + | \end{equation*} |

++++ | ++++ | ||

is equivalent to | is equivalent to | ||

| | | | ||

- | \[ | + | \begin{equation*} |

\left\{\begin{array}{l} | \left\{\begin{array}{l} | ||

C \setminus \{p\}, \ \ p \in C \\ | C \setminus \{p\}, \ \ p \in C \\ | ||

Line 129: | Line 126: | ||

C, \mbox{ otherwise} | C, \mbox{ otherwise} | ||

\end{array}\right. | \end{array}\right. | ||

- | \] | + | \end{equation*} |

++++ | ++++ | ||

Line 138: | Line 135: | ||

Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule. | Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule. | ||

+ |