Sistemi di riduzione astratti, forma normale, convertibilità,
grafi di riduzione. Proprietà di confluenza e Church-Rosser e loro
equivalenza. Locale confluenza, terminazione, canonicità.
Principio di induzione noetheriana, lemma di Newman e sua
dimostrazione [1].
Segnature, termini del prim'ordine, rappresentazione ad albero
dei termini. Posizioni, occorrenze, sottotermini e contesti. Sostituzioni,
sostituzioni istanziatrici ed unificatrici, mgu.
Identità ed equazioni, teoria equazionale E, relazione
di riduzione in E, chiusura rispetto a sostituzioni ed operazioni.
Deduzione equazionale, sistema deduttivo per l'uguaglianza modulo E.
Modelli, validità, soddisfacibilità, varietà e
teorema di completezza di Birkhoff.
Sistemi di riscrittura di termini, redesso, passo di riscrittura.
Terminazione: ordinamenti di riduzione, di semplificazione e per cammino
ricorsivo (rpo), ordinamento su multinsiemi.
Confluenza: decidibilità della convertibilità, spectra
delle regole,
sovrapposizione di regole, coppie critiche, sistemi ambigui.
Lemma di Huet e sua dimostrazione.
Problema della parola e sua decidibilità, teorema di Knuth-Bendix.
Procedure di completamento tramite regole di inferenza, terminazione e
divergenza del completamento (pattern di divergenza).
Riscrittura modulo equazioni, E-unificazione di termini, insieme minimale
e completo di E-unificatrici. Relazione di narrowing, procedura di
E-unificazione basata su narrowing, narrowing normale e basilare, albero
di derivazione di narrowing [2].
Formule booleane, soddisfacibilità, tautologia. Formule in forma CNF ed
algoritmo di Davis-Putnam. Refutazione ed algoritmo di Stålmarck.
Deduzione naturale: logica intuizionistica e logica naturale.
Logica predicativa: predicati, funzioni, variabili, quantificatori,
regole di deduzione naturale. Forma prenex DNF ed algoritmo di Presburger.
Isomorfismo di Curry-Howard: equivalenza tra tipo e formula e tra
programma e prova. Introduzione al sistema Coq: tipi, proposizioni,
insiemi, tipi dipendenti. Definizioni induttive e non induttive.
Funzioni ricorsive e non ricorsive. Prove in Coq: prove per ricorsione
e per casi. Prove interattive e tattiche di base
[3].