Proposizionale

• Normalizzazione
• DDP Esempio 1
• DDP Esempio 2

Primo ordine

• Sostituzione

• Trasformazione in FNP
• Skolemizzaione

• Tableaux - alberi di prova
• Rango
• Tableaux - formule valide
• Tableaux sistematici
• Hintikka set

• Forme di Skolem - chiusura esistenziale / universale
• Universo di Herbrand
• Modelli di Herbrand
• Espansione di Herbrand