Strogo tipiziran jezik za opis deduktivnih sustava

diplomski rad

• Naslov (engleski): A strongly typed language for specification of deductive systems
• Autor: Frano Perleta
• Mentor: Siniša Srbljić (mentor)
• Član povjerenstva: Siniša Srbljić (predsjednik povjerenstva)
• Član povjerenstva: Dejan Škvorc (član povjerenstva)
• Član povjerenstva: Ante Đerek (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Fakultet elektrotehnike i računarstva; Zagreb
• Datum i država obrane: 2015-02-18, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: TEHNIČKE ZNANOSTI; Računarstvo

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.

Sažetak (engleski)

The system L• is presented as a language for defining deductive systems. By utilizing dependent types, more precisely indexed families, L• may be used to model the domain of discourse, propositions over its elements, proofs, as well as axiom schemata and rules of inference, in accordance with the "propositions as types" principle. Lambda-abstraction is not present in the language, object equivalence and type equivalence are trivial. A formal description of (first-order) unification and proof search is given. An interpreter for L• called thingy is implemented in the Haskell programming language. Its architecture and surface syntax are discussed, as well as several internal syntax representations and techniques. The described system is applicable to automated proof checking and logic programming.

• Ključne riječi: ovisni tipovi; propozicije kao tipovi; automatska provjera dokaza; logičko programiranje
• Ključne riječi (engleski): dependent types; propositions as types; automated proof checking; logic programming
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:168:350390
• Studijski program: Naziv: Računarstvo; Vrsta studija: sveučilišni; Stupanj studija: diplomski; Akademski / stručni naziv: magistar/magistra inženjer/inženjerka računarstva (mag.ing.comp.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Zatvoreni pristup
• Datum i vrijeme pohrane: 2019-03-13 23:50:39