>   Dipartimento di Informatica   >   Toni Mancini
[login|nuovo account]      [Italiano|English]
Laurea Specialistica in Ingegneria Informatica, Corso di

Metodi Formali nell'Ingegneria del Software

 Edizione dell'a.a. 2007/08

Logica dei predicati del prim'ordine

Dispense del corso

Codice Descrizione
D.II.2 Logica dei predicati del prim'ordine

Programmi disponibili

Nome Descrizione
Otter e Mace2 Dimostratore di teoremi e ricercatore di modelli al prim'ordine

Esempi di file Otter/Mace2

Problema Descrizione
Consegne Dimostrazione di ridondanza nel cartello: "Spediamo in tutto il mondo. Anche in Italia"
Socrate Dimostrazione del sillogismo: 1. Tutti gli uomini sono mortali; 2. Socrate è un uomo; 3. Socrate è mortale
3-Coloring, model checking Specifica Mace2 per il problema di verificare che un dato assegnamento di colori ai nodi di un grafo sia una sua corretta 3-colorazione (model checking)
3-Coloring, model expansion Specifica Mace2 per il problema di trovare una corretta 3-colorazione di un grafo (model expansion)
Schur's lemma, model expansion Specifica Mace2 per il problema di trovare una soluzione al problema Shur's lemma (model expansion)

[This web site could never be realised without the sophisticated features of a pure text editor and the extreme power of 220V]