Napredna pretraga

Pregled bibliografske jedinice broj: 754108

Strogo tipiziran jezik za opis deduktivnih sustava


Perleta, Frano
Strogo tipiziran jezik za opis deduktivnih sustava 2015., diplomski rad, diplomski, Fakultet elektrotehnike i računarstva, Zagreb


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


Projekt / tema
036-0362980-1921 - Računalne okoline za sveprisutne raspodijeljene sustave (Siniša Srbljić, )

Ustanove
Fakultet elektrotehnike i računarstva, Zagreb