Seminar za matematičku logiku i osnove matematike

lokacija: 
PMF Matematički odsjek (virtualno)
vrijeme: 
18.05.2020 - 17:00 - 19:00

Na Seminaru za matematičku logiku i osnove matematike, u ponedjeljak 18. svibnja 2020. u 17 sati,

Vedran Čačić će održati predavanje

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.
 
Seminar će se održati putem Zoom-a. Link i potrebni podaci su ovdje (isti kao prošli put):
 
https://zoom.us/j/92305464243?pwd=TjUwa3VyTG5KT0pIbzluUURBemxJdz09

Meeting ID: 923 0546 4243
  

Ako nemate klijentski program za Zoom, možete ga besplatno skinuti ovdje:

 
 
Materijali s prošlog seminara:
 
 
Članak po kojem je napravljena većina predavanja: https://hal.inria.fr/hal-01094195/document
 
 
Upute za instalaciju Coqa:
Share this