Laboratorio di Logica Applicata

© (2005-2017) Marco Maggesi

Questa pagina contiene un semplice tutorial sulla meccanizzazione della matematica basato sul sistema di dimostrazione assistita Coq.

Presentazione

Slides di una breve Introduzione alla Meccanizzazione della Matematica.

Come fare

  1. Scaricare l'archivio zip con i file sorgenti.
  2. Aprire con Coq i file e seguire le spiegazioni e le istruzioni che si trovano nei commenti. Seguire i file nell'ordine specificato nel seguente indice.

Indice dei file

  1. Tauto.v: Tautologie
  2. FOL.v: Logica del primo ordine (First Order Logic)
  3. Nat.v: Numeri naturali
  4. Group.v: Teoria dei gruppi
  5. Lists.v: Teoria delle liste
  6. Trees.v: Teoria degli alberi binari

Altro materiale


Ultima modifica: luglio 2017.