- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:homework01 [2008/05/29 11:47] barbara typo |
sav08:homework01 [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 91: | Line 91: | ||

Negation-normal form of a propositional formula contains only conjunction, disjunction, and negation operators. Such formula should not contain implication operator. Moreover, negation only can only apply to variables and not to other formulas. The following tautologies can be used to transform formula to negation normal form: | Negation-normal form of a propositional formula contains only conjunction, disjunction, and negation operators. Such formula should not contain implication operator. Moreover, negation only can only apply to variables and not to other formulas. The following tautologies can be used to transform formula to negation normal form: | ||

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

\lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ | \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ | ||

p \leftrightarrow \lnot (\lnot p) \\ | p \leftrightarrow \lnot (\lnot p) \\ | ||

Line 97: | Line 97: | ||

\lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) | \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) | ||

\end{array} | \end{array} | ||

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

Extend the solution for the previous problem with a function that takes formula syntax tree and transforms it into an equivalent formula in negation-normal form. For example, the function should transform formula $\lnot (p \rightarrow \lnot q)$ into formula $p \land q$. | Extend the solution for the previous problem with a function that takes formula syntax tree and transforms it into an equivalent formula in negation-normal form. For example, the function should transform formula $\lnot (p \rightarrow \lnot q)$ into formula $p \land q$. | ||

Line 103: | Line 103: | ||

* generate a random assignment to propositional variables of the formula | * generate a random assignment to propositional variables of the formula | ||

* compare the truth value of the original and of the transformed formula | * compare the truth value of the original and of the transformed formula | ||

+ | |||

===== Optional Problem 5 ===== | ===== Optional Problem 5 ===== | ||

Line 108: | Line 109: | ||

Consider [[:regular expression]]s with variables denoting subsets of $\Sigma^*$ where $\Sigma=\{0,1\}$. Define function $W$ that takes such a regular expression and replaces | Consider [[:regular expression]]s with variables denoting subsets of $\Sigma^*$ where $\Sigma=\{0,1\}$. Define function $W$ that takes such a regular expression and replaces | ||

* each constant 0 with some relation $r_0$ and each constant 1 with some relation $r_1$ | * each constant 0 with some relation $r_0$ and each constant 1 with some relation $r_1$ | ||

- | * for each variable $L$ denoting a subset of $\Sigma^*$, replaces all of its occurrences with some relation $r_L$ | + | * for each variable $L$ denoting a subset of $\Sigma^*$, replaces all of its occurrences with a relation variable $r_L$, denoting relations on $S$ |

* replaces regular set union with relation union $\cup$ | * replaces regular set union with relation union $\cup$ | ||

* replaces concatenation with relation composition $\circ$ | * replaces concatenation with relation composition $\circ$ | ||

Line 114: | Line 115: | ||

For example | For example | ||

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

W({(p+qp)*}\, p) = (r_p \cup (r_q \circ r_p))^* \circ r_p | W({(p+qp)*}\, p) = (r_p \cup (r_q \circ r_p))^* \circ r_p | ||

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

Is it the case that that if an equality $r_1 = r_2$ holds for all values of variables representing subsets of $\Sigma^*$, then $W(r_1) = W(r_2)$ holds for all values of relation variables? If so, prove it. If not, give a counterexample. | Is it the case that that if an equality $r_1 = r_2$ holds for all values of variables representing subsets of $\Sigma^*$, then $W(r_1) = W(r_2)$ holds for all values of relation variables? If so, prove it. If not, give a counterexample. |