--| home | research | txt | code | teach | specialfunctionswiki | timescalewiki | hyperspacewiki | links |--

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))))))