Return to the class
Homework 5
#1.20: Determine whether or not the following Horn formulas are satisfiable. If it is satisfiable, then find an assignment that models the formula.
(a): $(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_3 \rightarrow A_4) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_5)\\
\wedge (A_1 \wedge A_2 \wedge A_3 \wedge A_4 \rightarrow A_6) \wedge (A_5 \wedge A_6 \rightarrow A_7) \wedge (A_2 \rightarrow A_3) \wedge (A_7 \rightarrow \bot)$
Solution: Apply the Horn algorithm.
Step 1:
$$\underbrace{(T \rightarrow A_1)}_{\text{mark } A_1} \wedge \underbrace{(T \rightarrow A_2)}_{\text{mark } A_2} \wedge (A_1 \wedge A_2 \wedge A_3 \rightarrow A_4) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_5)\\
\wedge (A_1 \wedge A_2 \wedge A_3 \wedge A_4 \rightarrow A_6) \wedge (A_5 \wedge A_6 \rightarrow A_7) \wedge (A_2 \rightarrow A_3) \wedge (A_7 \rightarrow \bot)$$
At the conclusion of Step 1, we have marked only $A_1$ and $A_2$. Now proceed to Step 2:
Step 2 (round 1):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_3 \rightarrow A_4) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_5)\\
\wedge (A_1 \wedge A_2 \wedge A_3 \wedge A_4 \rightarrow A_6) \wedge (A_5 \wedge A_6 \rightarrow A_7) \wedge \underbrace{(A_2 \rightarrow A_3)}_{\text{mark } A_3} \wedge (A_7 \rightarrow \bot)$$
At the conclusion of Step 2 (round 1) we have marked $A_1$, $A_2$, and $A_3$.
Step 2 (round 2):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge \underbrace{(A_1 \wedge A_2 \wedge A_3 \rightarrow A_4)}_{\text{mark } A_4} \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_5)\\
\wedge (A_1 \wedge A_2 \wedge A_3 \wedge A_4 \rightarrow A_6) \wedge (A_5 \wedge A_6 \rightarrow A_7) \wedge (A_2 \rightarrow A_3) \wedge (A_7 \rightarrow \bot)$$
At the conclusion of Step 2 (round 2) we have marked $A_1$, $A_2$, $A_3$, and $A_4$.
Step 2 (round 3):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_3 \rightarrow A_4) \wedge \underbrace{(A_1 \wedge A_2 \wedge A_4 \rightarrow A_5)}_{\text{mark } A_5}\\
\wedge \underbrace{(A_1 \wedge A_2 \wedge A_3 \wedge A_4 \rightarrow A_6)}_{\text{mark } A_6} \wedge (A_5 \wedge A_6 \rightarrow A_7) \wedge (A_2 \rightarrow A_3) \wedge (A_7 \rightarrow \bot)$$
At the conclusion of Step 2 (round 3) we have marked $A_1, A_2, A_3, A_4, A_5$, and $A_6$.
Step 2 (round 4):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_3 \rightarrow A_4) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_5)\\
\wedge (A_1 \wedge A_2 \wedge A_3 \wedge A_4 \rightarrow A_6) \wedge \underbrace{(A_5 \wedge A_6 \rightarrow A_7)}_{\text{mark } A_7} \wedge (A_2 \rightarrow A_3) \wedge (A_7 \rightarrow \bot)$$
At the conclusion of Step 2 (round 4) we have marked $A_1, A_2, A_3, A_4, A_5, A_6$, and $A_7$. This concludes Step 2.
Step 3:
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_3 \rightarrow A_4) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_5)\\
\wedge (A_1 \wedge A_2 \wedge A_3 \wedge A_4 \rightarrow A_6) \wedge (A_5 \wedge A_6 \rightarrow A_7) \wedge (A_2 \rightarrow A_3) \wedge \underbrace{(A_7 \rightarrow \bot)}_{\text{conclude not satisfiable}}$$
(b): $(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_3) \wedge (A_1 \wedge A_5 \wedge A_6) \wedge (A_2 \wedge A_7 \rightarrow A_5)$
$\wedge (A_1 \wedge A_3 \wedge A_5 \rightarrow A_7) \wedge (A_2 \rightarrow A_4) \wedge (A_4 \rightarrow A_8) \wedge (A_2 \wedge A_3 \wedge A_4 \rightarrow A_9)$
$\wedge (A_3 \wedge A_9 \rightarrow A_6) \wedge (A_6 \wedge A_7 \rightarrow A_8) \wedge (A_7 \wedge A_8 \wedge A_9 \rightarrow \bot)$
Solution:
Step 1:
$$\underbrace{(T \rightarrow A_1)}_{\text{mark } A_1} \wedge \underbrace{(T \rightarrow A_2)}_{\text{mark } A_2} \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_3) \wedge (A_1 \wedge A_5 \wedge A_6) \wedge (A_2 \wedge A_7 \rightarrow A_5)$$
$$\wedge (A_1 \wedge A_3 \wedge A_5 \rightarrow A_7) \wedge (A_2 \rightarrow A_4) \wedge (A_4 \rightarrow A_8) \wedge (A_2 \wedge A_3 \wedge A_4 \rightarrow A_9)$$
$$\wedge (A_3 \wedge A_9 \rightarrow A_6) \wedge (A_6 \wedge A_7 \rightarrow A_8) \wedge (A_7 \wedge A_8 \wedge A_9 \rightarrow \bot)$$
At the conclusion of Step 1, we have marked $A_1$ and $A_2$.
Step 2 (round 1):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_3) \wedge (A_1 \wedge A_5 \wedge A_6) \wedge (A_2 \wedge A_7 \rightarrow A_5)$$
$$\wedge (A_1 \wedge A_3 \wedge A_5 \rightarrow A_7) \wedge \underbrace{(A_2 \rightarrow A_4)}_{\text{mark } A_4} \wedge (A_4 \rightarrow A_8) \wedge (A_2 \wedge A_3 \wedge A_4 \rightarrow A_9)$$
$$\wedge (A_3 \wedge A_9 \rightarrow A_6) \wedge (A_6 \wedge A_7 \rightarrow A_8) \wedge (A_7 \wedge A_8 \wedge A_9 \rightarrow \bot)$$
At the conclusion of Step 2 (round 1) we have marked $A_1$, $A_2$, and $A_4$.
Step 2 (round 2):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge \underbrace{(A_1 \wedge A_2 \wedge A_4 \rightarrow A_3)}_{\text{mark } A_3} \wedge (A_1 \wedge A_5 \wedge A_6) \wedge (A_2 \wedge A_7 \rightarrow A_5)$$
$$\wedge (A_1 \wedge A_3 \wedge A_5 \rightarrow A_7) \wedge (A_2 \rightarrow A_4) \wedge \underbrace{(A_4 \rightarrow A_8)}_{\text{mark } A_8} \wedge (A_2 \wedge A_3 \wedge A_4 \rightarrow A_9)$$
$$\wedge (A_3 \wedge A_9 \rightarrow A_6) \wedge (A_6 \wedge A_7 \rightarrow A_8) \wedge (A_7 \wedge A_8 \wedge A_9 \rightarrow \bot)$$
At the conclusion of Step 2 (round 2) we have marked $A_1, A_2, A_3, A_4$, and $A_8$.
Step 2 (round 3):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_3) \wedge (A_1 \wedge A_5 \wedge A_6) \wedge (A_2 \wedge A_7 \rightarrow A_5)$$
$$\wedge (A_1 \wedge A_3 \wedge A_5 \rightarrow A_7) \wedge (A_2 \rightarrow A_4) \wedge (A_4 \rightarrow A_8) \wedge \underbrace{(A_2 \wedge A_3 \wedge A_4 \rightarrow A_9)}_{\text{mark } A_9}$$
$$\wedge (A_3 \wedge A_9 \rightarrow A_6) \wedge (A_6 \wedge A_7 \rightarrow A_8) \wedge (A_7 \wedge A_8 \wedge A_9 \rightarrow \bot)$$
At the end of Step 2 (round 3) we have marked $A_1, A_2, A_3, A_4, A_8$, and $A_9$.
Step 2 (round 4):
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_3) \wedge (A_1 \wedge A_5 \wedge A_6) \wedge (A_2 \wedge A_7 \rightarrow A_5)$$
$$\wedge (A_1 \wedge A_3 \wedge A_5 \rightarrow A_7) \wedge (A_2 \rightarrow A_4) \wedge (A_4 \rightarrow A_8) \wedge (A_2 \wedge A_3 \wedge A_4 \rightarrow A_9)$$
$$\wedge \underbrace{(A_3 \wedge A_9 \rightarrow A_6)}_{\text{mark } A_6} \wedge (A_6 \wedge A_7 \rightarrow A_8) \wedge (A_7 \wedge A_8 \wedge A_9 \rightarrow \bot)$$
At the end of Step 2 (round 4) we have marked $A_1, A_2, A_3, A_4, A_6, A_8$, and $A_9$. This is the end of Step 2.
Step 3:
$$(T \rightarrow A_1) \wedge (T \rightarrow A_2) \wedge (A_1 \wedge A_2 \wedge A_4 \rightarrow A_3) \wedge (A_1 \wedge A_5 \wedge A_6) \wedge (A_2 \wedge A_7 \rightarrow A_5)$$
$$\wedge (A_1 \wedge A_3 \wedge A_5 \rightarrow A_7) \wedge (A_2 \rightarrow A_4) \wedge (A_4 \rightarrow A_8) \wedge (A_2 \wedge A_3 \wedge A_4 \rightarrow A_9)$$
$$\wedge (A_3 \wedge A_9 \rightarrow A_6) \wedge (A_6 \wedge A_7 \rightarrow A_8) \wedge (A_7 \wedge A_8 \wedge A_9 \rightarrow \bot)$$
Notice that we do not have $A_7$, $A_8$, and $A_9$ all simultaneously marked. Therefore the last implication to $\bot$ is not satisfied. Therefore we conclude that the formula is satisfiable.
Prolog homework
1. succ(succ(succ(0)))
2. add(succ(succ(succ(0))),X,succ(succ(succ(succ(0))))) --- the result is: X=succ(0), meaning X=1
3. the result is: succ(succ(succ(succ(0)))); it is computing 2*2=4
4. the result is:
P = succ(succ(succ(0)))
X = succ(0)
meaning that P=3 and X=1 in the formula 1+P=4 where P=3X
5. The following code will do it:
expo(_X,0,succ(0)).
expo(X,succ(N),E):-
expo(X,N,P), mult(P,X,E).
The first line encodes X^0=1 and the second line encodes X^(N+1)=E provided that P=X^N and PX=E
6. Calculate 2^3 by running
expo(succ(succ(0)),succ(succ(succ(0))),X)
the result is
X = succ(succ(succ(succ(succ(succ(succ(succ(0))))))))
7. The following code will do it:
fac(0,succ(0)).
fac(succ(N),F):-
fac(N,P), mult(succ(N),P,F).
8. Calculate 3!=6 by running
f(succ(succ(succ(0))),X)
which returns
X=succ(succ(succ(succ(succ(succ(0))))))
