Proposizionale

Introduzione

Sintassi

Semantica

Soddisfacibilità e conseguenza logica

Conseguenza ed equivalenza logica: alcuni teoremi

Sostituzione proposizionale

Forme normali

Completezza funzionale

Calcoli a tableaux

Calcolo alla Hilbert

Teorema di compattezza

Risoluzione

Esempio di applicazione della CPL

Primo ordine

Introduzione

Sintassi

Semantica

Soddisfacibilità, validità e conseguenza logica

Equivalenza logica

Sostituzioni

Forme normali

Tableaux

Modelli di Herbrand

Risoluzione

Materiale utile

Dimostrazioni

Esempi

Definizioni

Esercizi

Semantica

Soddisfacibilità e conseguenza logica

Forme normali

Tableaux

Metodo di risoluzione


Modelli — Semantica

Modelli — Validità

Modelli — Equivalenze logiche

Forme normali

Tableau

Robinson

Risoluzione