Final sample

Question 1: Boolean function classification
(50 × 3 + 150 = 300 pts.)
Boolean functions can be valid, satisfiable, unsatisfiable, or falsifiable.
(a) Determine the status of the following Boolean formulas, regarding these properties. The
properties can overlap; you must state all of the four properties a formula fulfills. For
example, formula p ∨ ¬p is valid and satisfiable, and nothing else.
Give evidence for your decisions, as follows:
• simplify valid formulas to T , or show the truth table,
• simplify unsatisfiable formulas to F , or show truth table,
• for satisfiable and falsifiable formulas, give a satisfying and a falsifying assignment.
(i) ¬q ∧ (p ⇒ q) ⇒ q
(ii) a ∨ ¬b ⇒ ((a ⇒ b) ⇔ (a ⇔ b))
2
(iii) a ∧ (b ⇒ (¬(a ∨ c))) ∧ b
(b) Two Boolean formulas are called inconsistent if their conjunction is not satisfiable. Give
an algorithm to check inconsistency of two formulas f and g using a falsifiability oracle, i.e.
a machine that takes a formula h as input and returns true if and only if h is falsifiable.
Your algorithm should take f and g as inputs and return true if and only if f and g are
inconsistent. The body of the algorithm may build new formulas from f and g using propositional connectives, and it may pass any such formula to the oracle, as often as you like.
Your algorithm also has decision making capabilities, i.e. it is allowed to have if statements.
These are all control structures available to your algorithm.
For full credit, you must show the algorithm, and you must show the propositional reasoning
that explains why your algorithm is correct.
3
Question 2: Admissibility (50 + 100 + 150 = 300 pts.)
The function evenp : All -> Boolean returns t exactly if its argument is an even integer.
(a) Consider function foo below.
• If foo is not admissible, state so, and why. For example, if your reason for nonadmissibility is a body contract violation, show an input that satisfies foo’s input contract, and a function in the body of foo whose input contract fails when foo is called
on your input. If your reason for non-admissibility is that foo is non-terminating, give
an input on which foo runs forever.
• If foo is admissible, state so without proof. Then determine the induction scheme the
function gives rise to. Write down all (that means, all ) claims that need to be proved,
in order to prove some property phi using the induction scheme suggested by foo.
(defunc foo (m n)
:input-contract (and (natp m) (evenp n))
:output-contract (integerp (foo m n))
(cond ((equal m 0)
-3)
((and (evenp m) (> n 2)) 10)
((evenp m)
(foo (/ m 2) (+ (/ m 2) n)))
(t
(foo (- m 1) (+ n 2)))))
4
(b) Repeat the tasks in (a) for the following function bar:
(defunc bar (m n)
:input-contract (and (natp m) (evenp n))
:output-contract (integerp (bar m n))
(cond ((equal m 0)
-3)
((and (evenp m) (> n 2)) 10)
((evenp m)
(bar (/ m 2) n))
(t
(bar (- m 1) (+ n 2)))))
5
(c) The following function foobar is admissible (you do not have to prove this fact).
(defunc foobar (m n)
:input-contract (and (natp m) (evenp n))
:output-contract (integerp (foobar m n))
(if (equal m 0)
-3
(foobar (- m 1) (+ n 2))))
It thus gives rise to a valid induction scheme, for any target conjecture phi. (Write it down.)
Someone now claims: we can simplify this induction scheme, by dropping the first proof
obligation
(*)
~((natp m) /\ (evenp n)) => phi .
Show that this claim is wrong: give a simple formula phi that is not valid, but all proof
obligations of the induction scheme are valid for phi, except (*).
6
Question 3: Termination (250 + 100 = 350 pts.)
For each of the two functions below, decide whether it terminates for all legal inputs.
• If not, provide a legal input on which the function runs forever, and show the arguments the
function is called on during the first five recursive calls. For example, for the non-terminating
function f:Nat->All defined via (f n) = (f (+ n 1)), you might write:
(f 0)
(f 1)
(f 2)
(f 3)
(f 4) ...
• If yes, (i) define a measure function (in ACL2 notation, with contracts), and (ii) prove that
the value of the measure function decreases in each recursive call, under the conditions that
lead to that recursive call. The proof for (ii) does not have to be formal equational reasoning,
but the arithmetic argument must be correct and evident from your proof.
(a) (defunc h (a b c)
:input-contract (and (natp a) (integerp b) (listp c))
:output-contract t
(cond ((equal a 0) (len c))
((endp c)
(+ a b))
((<= b 1)
(+ a (h (- a 1) (+ b 1) (rest c))))
(t
(h a (- b 2) c))))
7
(. . . more space . . . )
(b) (defunc z (l1 l2)
:input-contract (and (listp l1) (listp l2))
:output-contract t
(cond ((endp l1)
())
((endp l2)
(first l1))
((< (len l1) (len l2))
(z (cons 1 l1) (rest l2)))
((equal (len l1) (len l2)) (list (first l1) (first l2)))
(t
(z (rest l1) (cons 2 l2)))))
8
Question 4: Induction (100 + 100 + 200 + 200 = 600 pts.)
Consider the following definitions:
(defunc in (x l)
:input-contract (listp l)
:output-contract (booleanp
(cond ((endp l)
((equal x (first l))
(t
(in x l))
nil)
t)
(in x (rest l)))))
(defunc union (l1 l2)
:input-contract (and (listp l1) (listp l2))
:output-contract (listp (union l1 l2))
(if (endp l1)
l2
(cons (first l1) (union (rest l1) l2))))
and the following conjecture:
phi :: (listp l1) /\ (listp l2) => (in x (union l1 l2)) = (in x l1) \/ (in x l2)
Convince yourself that all functions occurring in the conjecture satisfy their respective input contracts. Then prove the conjecture using induction. Follow these hints:
• Use the induction scheme suggested by function in, applied to arguments x and l1. This
will give rise to four proof obligations. Prove them all. You may use the shortcut phi to
denote the conjecture in writing down the proof obligations, but when you extract context
and do the proof, spell everything out.
• You may use the following lemma psi without proof. If you do, show the substitution that
makes psi applicable.
psi :: (listp l) /\ (not (endp l)) /\ (x != (first l))
=> (in x l) = (in x (rest l))
9
(. . . more space . . . )
10
(. . . more space . . . )
11
Question 5: Easter basket (50 × 6 + 150 = 450 pts.)
(a) Clearly mark the following statements as “true” or “false”. If “true”, explain your answer.
If “false”, give a counterexample.
(i) Let f be a Boolean formula. If f is neither valid nor unsatisfiable, then f is both
satisfiable and falsifiable.
(ii) Let f be a Boolean formula. If the conjunctive normal form of f is valid, then the
disjunctive normal form of f is unsatisfiable.
(iii) Let f and g be Boolean formulas such that exactly one of f , g is satisfiable, and both
are falsifiable. Then both f ⇔ g and f ⊕ g are satisfiable.
12
(iv) Let f and g be Boolean formulas such both f ⇔ g and f ⊕ g are satisfiable. Then
exactly one of f , g is satisfiable.
(v) Let f be a recursively defined ACL2 function of one argument that we want to admit,
and x an input that satisfies f’s input contract. Function f terminates on input x if and
only if the set of arguments f is called on recursively while evaluating (f x) is finite.
(vi) For any admissible ACL2 function, there exists a measure function.
13
(b) Analyze the following statement using propositional logic, as follows:
• Assign propositional variables to atomic facts in the sentence. (We suggest you write
the variables on top of the sentence parts in question. Do not use T and F as variables.)
• Derive a propositional formula that best represents the meaning of the sentence.
• Decide whether the sentence is valid. If it is, prove the validity using any means, e.g.
truth table or simplification. If it is not, provide an assignment to all your variables
such that your formula evaluates to F .
The dealer will not repair my car unless I have money. I never have money the
week after a Superbowl game. Last weekend was a Superbowl game. Therefore, the
dealer will not repair my car.
14

Download Report