I have the following task
"Check the following expressions with the horn satisfiability algorithm, and, if necessary, provide an assignment which fulfills satisfiability."
- $((\neg q \lor \neg p) \land (\neg r \lor p) \land \neg q \land \neg r)$
- $((\neg q \lor p) \land (\neg r \lor p) \land q \land r)$
- $((\neg q \lor \neg p) \land (\neg r \lor p) \land q \land r )$
Progress so far:
I have been provided with the following algorithm:
" a) For each implication of the form $\top \to B$, assign True to $B$.
b) If for an implication of the form $(A_1 \land \dots \land A_n) \to B$ the atomic sentences $A_1, \dots, A_n$ have already been assigned True, then assign true to B aswell.
c) Repeat step b as much as possible.
d) If the following result is reached $(A_1 \land \dots \land A_n) \to \perp$, and all atomic sentences $A_1, \dots, A_n$ have been assigned true, then S is not truth table satisfiable. Otherwise, for all atomic sentences from S which have not yet been assigned a value, assign them the value False. The assignment thus obtained makes S true."
My problem is that it is not intuitive to me how the verum and falsum symbols are used in the first place. I am aware that $a \to b \equiv \neg a \lor b$, and that this is a key property of horn expressions, but that's about it. Could someone help me make a start on one of above examples so I check my understanding with the other two?
further progress:
As has been proposed, a good starting point would be to write the formula as a set of implications. In order to do this step, I found a Youtube video in German which indicates the necessary transformations by use of colour coding.
Step $0$: Implication form.
1) $((\neg q \lor \neg p) \land (\neg r \lor p) \land \neg q \land \neg r) \equiv (((q \land r) \to \perp) \land (r \to p) \land (q \to \perp) \land (r \to \perp))$
2) $((\neg q \lor p) \land (\neg r \lor p) \land q \land r) \equiv ((q \to p) \land (r \to p) \land (\top \to q) \land (\top \to r))$
3) $((\neg q \lor \neg p) \land (\neg r \lor p) \land q \land r ) \equiv (((q \land p) \to \perp) \land (r \to p) \land (\top \to q) \land (\top \to r))$
step $1$: Apply the algorithm.
part 1) $((q \to p) \land (r \to p) \land (\top \to q) \land (\top \to r))$
a) Not applicable here.
b) & c) There are no sentences in this form, so also not applicable here.
d) Assign the value $\perp$ to $q$ and $r$.
At this point $p$ in $(r \to p)$ is the only variable which hasn't been assigned a value. As it appears, it can be assigned any value and the expression will eb true.
Thus, I would conclude that part 1 is truth table satisfiable and propose the solution for part 1 as $q = \perp, r = \perp, r = \perp$ OR $q = \perp, r = \perp, r = \top$
part 2) $((q \to p) \land (r \to p) \land (\top \to q) \land (\top \to r))$
a) Assign the value $\top$ to $q$ and $r$..
b) and c) the value $\top$ to $p$
Thus, I would conclude that part 1 is truth table satisfiable I would propose the solution for part 2 as $q = \top, r = \top, r = \top$.
part 3) $(((q \land p) \to \perp) \land (r \to p) \land (\top \to q) \land (\top \to r))$
a) Assign $\top$ to $q$ and $r$
b) and c) Assign $\top$ to $p$
d) Since the above assignment furnishes the result $(q = \top \land p = \top) \to \perp$, the expression is not satisfiable.
Solution for part 3: The expression is not satisfiable (and no truth value assignment is provided)