Laboratorio di Logica Applicata

© (2005-2018) Marco Maggesi

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

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 2018.