CS262 Logic and Verification test 2
UNIVERSITY OF WARWICK Class Test
Logic and Verification
Time allowed: 45 minutes Answer all questions.
Copyright By PowCoder代写 加微信 powcoder
Write your answers into the provided boxes. Use additional white paper for inter- mediate calculations. These will be ignored by the marker.
Enter your University Registration Number (library card number) in the space below.
University Registration Number
Do not write below this line
8 8 8 14 12
1. Compute the truth table for the following Boolean function:
f (x, y, z) = ((x ← ¬y) ∨ (¬x → (z ∧ y))). [8]
x y z TTT TTF TFT TFF FTT FTF FFT FFF
2. Draw the parse tree for the function f from before. [8]
3. What is the conjunctive normal form of the function g(x, y, z) = (x ∧ y ∧ z) ∨ (¬x∧y∧¬z)∨(¬x∧¬y∧z)∨(x∧¬y∧z)∨(¬x∧¬y∧¬z)∨(x∧¬y∧¬z)? Hint: Consider the truth table of this function. [8]
4. Consider the following tableau proof for (x ∧ (y → (z ∨ w))) → (x ∨ y):
0. ¬((x∧(y→(z∨w)))→(x∨y)) 1. x∧(y→(z∨w))
4. y→(z∨w)
5. ¬y 8. z ∨ w
7.¬y 9. z 12. w
10.¬x 13. ¬x 11.¬y 14. ¬y
Annotate this proof, by writing one line for each application of an expansion rule, in the correct order. In each line, write the name of the rule, the number of the tree node to which this rule applies, and the number(s) of the tree node(s) that the rule creates. An example of such a line would be
‘β-expansion on 3 creates 7 and 12’.
Step Rule i
iv v vi vii
5. Consider the following Prolog program:
g(c,d(e)).
f(X,Y):-X>=2, T is X-1, f(T,Z), Y is Z*X. What is the result of each of the following queries?
[7 · 2 = 14]
?- g(a,b).
?- g(X,d(e)).
?- g(c,d(Z)).
?- f(1,X).
?- f(1,X),X>3.
?- f(4,X).
[6 · 2 = 12]
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com