La résolution

1. Sur $p$ : $q \lor r \lor \lnot s$. C'est la seule.
2. Sur $p$ : $q \lor \lnot q$ ; sur $q$ : $p \lor \lnot p$. Deux tautologies, inutiles. Pas de $\square$ : on ne résout pas sur deux littéraux d'un coup, et ces deux clauses sont satisfiables ensemble ($p = 1, q = 0$).
3. Aucune : pas de littéral et de son opposé.
4. $\square$.

Soit $v$ un modèle des deux clauses. Si $v(p) = 1$, $\lnot p$ est faux, donc $D$ est vraie ; si $v(p) = 0$, $p$ est faux, donc $C$ est vraie. Dans les deux cas $C \lor D$ est vraie dans $v$.

1. Clauses : $\lnot p \lor q$, $\lnot q \lor r$, et $\lnot(p \to r) \equiv p \land \lnot r$ donne $p$ et $\lnot r$. Puis $p$ et $\lnot p \lor q$ : $q$ ; $q$ et $\lnot q \lor r$ : $r$ ; $r$ et $\lnot r$ : $\square$.
2. On réfute la négation : $(\lnot p \lor q \lor r) \land (\lnot q \lor r) \land p \land \lnot r$. Clauses : $\lnot p \lor q \lor r$, $\lnot q \lor r$, $p$, $\lnot r$. Puis $p$ avec la première : $q \lor r$ ; avec $\lnot r$ : $q$ ; avec $\lnot q \lor r$ : $r$ ; avec $\lnot r$ : $\square$.
3. Négation : $((p \to q) \to p) \land \lnot p$. Or $(p \to q) \to p \equiv \lnot(\lnot p \lor q) \lor p \equiv (p \land \lnot q) \lor p$, en FNC $p \land (p \lor \lnot q)$. Clauses : $p$, $p \lor \lnot q$, $\lnot p$. Puis $p$ et $\lnot p$ : $\square$.
4. $t$ : train en retard, $x$ : il y a des taxis, $j$ : Jean est en retard. Hypothèses $t \land \lnot x \to j$, $\lnot j$, $t$ ; conclusion $x$. Clauses : $\lnot t \lor x \lor j$, $\lnot j$, $t$, $\lnot x$. Puis $\lnot j$ avec la première : $\lnot t \lor x$ ; avec $t$ : $x$ ; avec $\lnot x$ : $\square$. Le raisonnement est correct.

1. On ajoute $\lnot j$. Avec $\lnot a \lor j$ : $\lnot a$. Avec $p \lor j \lor a$ et $\lnot j$ : $p \lor a$, puis avec $\lnot a$ : $p$. Avec $\lnot p \lor j \lor a$ et $\lnot j$ : $\lnot p \lor a$, puis avec $\lnot a$ : $\lnot p$. Enfin $p$ et $\lnot p$ : $\square$. Donc les faits entraînent $j$.
2. On ajoute $p$, et l'on peut utiliser $j$ (démontré). $j$ et $\lnot j \lor \lnot p$ : $\lnot p$ ; avec $p$ : $\square$.

1. $p \lor q$ et $\lnot p \lor q$ : $q$. $p \lor q$ et $p \lor \lnot q$ : $p$. $\lnot p \lor q$ et $p \lor \lnot q$ : deux tautologies. Puis $q$ et $p \lor \lnot q$ : $p$ (déjà là) ; $p$ et $\lnot p \lor q$ : $q$ (déjà là). Plus rien de nouveau.
2. $\square$ n'est pas apparue : $S$ est satisfiable. Modèle : $p = 1, q = 1$.
3. On a déjà $p$ et $q$ ; avec $\lnot p \lor \lnot q$ et $p$ : $\lnot q$ ; avec $q$ : $\square$. $S'$ est insatisfiable : ses quatre clauses interdisent chacune une des quatre interprétations.