Učitavanje video playera...
01:04:45
Vedran Čačić: Calculus of inductive constructions (2)
Sažetak: U drugom dijelu, upoznat ćemo se s automatskim dokazivačem (bolje: pomoćnikom pri dokazivanju) Coq, koji je razvijen na matematičkoj osnovi CIC-a. Coq je ujedno i moćan programski jezik, koji omogućuje funkcijsko programiranje vrlo visoke razine -- ali nije Turing-potpun, jer mora biti totalan kako bi sačuvao konzistentnost dokazanih tvrdnji. To znači da se svaki izraz može izračunati do kraja, odnosno svaki program sa svakim ulazom stane. Također ćemo vidjeti kako dihotomija između računanja i dokazivanja prirodno reprezentira dihotomiju između rekurzivnih i rekurzivno prebrojivih (odnosno odlučivih i poluodlučivih) svojstava.
Objavljeno: 19.05.2020
Unutar kategorije: Obrazovanje

Srodni zapisi