2a)
{1}     (1)  A -> B   P
{2}     (2)  -A -> C  P
{3}     (3)  -B       P
{1,2,3} (4) -A & C    T 1,2,3
(Satslogiska bevis blir triviala när vi har regel T.)

2b)
{1}     (1)  A | (B | C)  P
{2}     (2)  A -> B & C   P
{3}     (3)  B -> C       P
{1,2,3} (4)  C            T 1,2,3
(Satslogiska bevis blir triviala när vi har regel T.)

2c)
{} (1)  A | -A  T
(Tautologier kan införas direkt med regel T.)

4a)
{1}   (1)  Stålman(clark) & Ax (Stålman(x) -> x = clark)  P
{2}   (2)  -(jimmy = clark)                               P
{1}   (3)  Ax (Stålman(x) -> x = clark)                   T 1
{1}   (4)  Stålman(jimmy) -> jimmy = clark                AE 3
{1,2} (5)  -Stålman(jimmy)                                T 2,4

4b)
==>
{1} (1)  -Ex P(x)  P
{1} (2)  Ax -P(x)  Q 1
<==
{1} (1)  Ax -P(x)  P
{1} (2)  -Ex P(x)  Q 1
(De Morgan's lagar för kvantifierare blir triviala när vi har regel Q.)

6b)
{1}   (1)  Ax (Bil(x) & -Besiktigad(x) -> Körförbud(x))  P
{2}   (2)  Ey (Äger(john,y) & Bil(y) & -Körförbud(y))    P
{3}   (3)  Äger(john,c) & Bil(c) & -Körförbud(c)         P
{1}   (4)  Bil(c) & -Besiktigad(c) -> Körförbud(c)       AE 1
{1,3} (5)  Äger(john,c) & Bil(c) & Besiktigad(c)         T 3,4
{1,3} (6)  Ez (Äger(john,z) & Bil(z) & Besiktigad(z))    EI 5
{1,2} (7)  Ez (Äger(john,z) & Bil(z) & Besiktigad(z))    EE 2,3,6