Naslov
Strogo tipiziran jezik za opis deduktivnih sustava
(Strongly typed language for specification of deductive systems)

Autori
Perleta, Frano

Vrsta, podvrsta i kategorija rada
Ocjenski radovi, diplomski rad, diplomski

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
18.02

Godina
2015

Stranica
49

Mentor
Srbljić, Siniša

Neposredni voditelj
Vladimir, Klemo

Ključne riječi
ovisni tipovi; propozicije kao tipovi; automatska provjera dokaza; logičko programiranje
(dependent types; propositions as types; automated proof checking; logic programming)

Sažetak
Predstavljen je L, jezik za opis deduktivnih sustava. Korištenjem ovisnih tipova, točnije indeksiranih familija, L može modelirati elemente domene diskursa, propozicije nad njima, dokaze te shematske aksiome i pravila zaključivanja, u skladu s načelom "propozicije kao tipovi". Lambda–apstrakcija nije dostupna, ekvivalencija objekata i tipova je trivijalna. Formalno su opisani algoritmi za unifikaciju (prvog reda) i pretraživanje. Također je predstavljen thingy, interpreter za L ostvaren u programskom jeziku Haskell. Opisana je arhitektura sustava, konkretna sintaksa, različite interne reprezentacije sintakse te druge tehnike korištene u razvoju. Sustav je primjenjiv na automatsku provjeru dokaza i logičko programiranje.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA