Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:homework01 [2008/02/23 21:18] piskac |
sav08:homework01 [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 24: | Line 24: | ||
} | } | ||
</code> | </code> | ||
- | You should be able to save this file as BinarySearchTree.scala, compile it with "scalac BinarySearchTree.scala", run it witn "scala BinarySearchTree", and obtain as a result "Inside". | + | You should be able to save this file as BinarySearchTree.scala, compile it with "scalac BinarySearchTree.scala", run it with "scala BinarySearchTree", and obtain as a result "Inside". |
* for fun, test [[piVC tool]] and on BinarySearch.pi example (install piVC if needed) | * for fun, test [[piVC tool]] and on BinarySearch.pi example (install piVC if needed) | ||
Line 30: | Line 30: | ||
* you may also wish to check the tutorial and this [[http://afp.sourceforge.net/browser_info/current/HOL/BinarySearchTree/BinaryTree_TacticStyle.html|Binary Search Tree example]] | * you may also wish to check the tutorial and this [[http://afp.sourceforge.net/browser_info/current/HOL/BinarySearchTree/BinaryTree_TacticStyle.html|Binary Search Tree example]] | ||
* for fun, Use formDecider.opt from [[:Jahob system]] to prove the same [[Proofs and Induction#Example|example from class]], as well as the examples in Exercises (install [[:Jahob system]] as well as provers CVC3 and E if needed) | * for fun, Use formDecider.opt from [[:Jahob system]] to prove the same [[Proofs and Induction#Example|example from class]], as well as the examples in Exercises (install [[:Jahob system]] as well as provers CVC3 and E if needed) | ||
+ | * if you log into your EPFL account, the Jahob verifier should be accessible by invoking: | ||
+ | <code> | ||
+ | ~kuncak/software/bin/verify --help | ||
+ | </code> | ||
===== Problem 1 ===== | ===== Problem 1 ===== | ||
Line 87: | 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 93: | 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 99: | 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 104: | 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 110: | 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. |