1.  (A|!C) | ((A|B|!C)->(C&B))
    (A|!C) | (!(A|B|!C)|(C&B))
met resolutie tonen dat de uitdrukking altijd onwaar is, dus inverteren
en in CNV:
   ![(A|!C) | (!(A|B|!C)|(C&B))]
   !(A|!C) & !(!(A|B|!C)|(C&B))
   !A & C &  (A|B|!C) & !(C&B)
   !A & C &  (A|B|!C) & (!C|!B)
resolutie:
{!A} {C} {A,B,!C} {!C,!B}
 |     \ /        /
  \   {A,B}     /
    {B}       /
         []

2. !(A&!D&!C), !A->(!B|C), !C / (A|B)->(A&D)
in CNV:
!A|D|C         A|!B|C      !C   !(A|B)|(A&D)

3.
P Q R  if p then q else r
T T T  T
T T F  T
T F T  F
T F F  F
F T T  T
F T F  F
F F T  T
F F F  F

Alle gevallen waarbij uitkomst T is opschrijven:
(P&Q&R) | (P&Q&!R) | (!P&Q&R) | (!P&!Q&R)

4. Een connectief is functioneel volledig als het ! en & bevat.
!P kan worden verkregen door P@P te doen:

P !P P@P
T F  F
F T  T

P&Q is ingewikkelder:
P|Q kan door !(P@Q) te doen, oftewel (P@Q)@(P@Q).
Men kan P&Q verkrijgen met gebruik van '|' en '!' door !(!P|!Q) te doen

Dus: (!P|!Q)@(!P|!Q)
   ((P@P)|(Q@Q))@((P@P)|(Q@Q))
(((P@P)@(Q@Q)) @ ((P@P)@(Q@Q)))  @  (((P@P)@(Q@Q)) @ ((P@P)@(Q@Q))))

5. A->S, A, K->B, !B  /  S&!K    (pr1,pr2 .. / concl.)
  !A|S   A  !K|B  !B     S&!K
Met resolutie kijken of er een geval is met premissen waar en conclusie
onwaar, dus !(conclusie):
!(S&!K) geeft !S|K

 {!A,S} {A} {!K,B} {!B}   {!S,K}
    \   /      \    /      /
      S          !K     /
        \          \  /
          \         S!
	    \      /
	       []