prikaz prve stranice dokumenta Strogo tipiziran jezik za opis deduktivnih sustava
No public access
master's thesis
Strogo tipiziran jezik za opis deduktivnih sustava
Zagreb: University of Zagreb, Faculty of Electrical Engineering and Computing, 2015. urn:nbn:hr:168:350390
Perleta, Frano
University of Zagreb
Faculty of Electrical Engineering and Computing

Institutional repository: FER Repository

Cite this document

Perleta, F. (2015). Strogo tipiziran jezik za opis deduktivnih sustava (Master's thesis). Zagreb: University of Zagreb, Faculty of Electrical Engineering and Computing. Retrieved from https://urn.nsk.hr/urn:nbn:hr:168:350390

Perleta, Frano. "Strogo tipiziran jezik za opis deduktivnih sustava." Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, 2015. https://urn.nsk.hr/urn:nbn:hr:168:350390

Perleta, Frano. "Strogo tipiziran jezik za opis deduktivnih sustava." Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, 2015. https://urn.nsk.hr/urn:nbn:hr:168:350390

Perleta, F. (2015). 'Strogo tipiziran jezik za opis deduktivnih sustava', Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, accessed 26 December 2024, https://urn.nsk.hr/urn:nbn:hr:168:350390

Perleta F. Strogo tipiziran jezik za opis deduktivnih sustava [Master's thesis]. Zagreb: University of Zagreb, Faculty of Electrical Engineering and Computing; 2015 [cited 2024 December 26] Available at: https://urn.nsk.hr/urn:nbn:hr:168:350390

F. Perleta, "Strogo tipiziran jezik za opis deduktivnih sustava", Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, Zagreb, 2015. Available at: https://urn.nsk.hr/urn:nbn:hr:168:350390

Metadata
TitleStrogo tipiziran jezik za opis deduktivnih sustava
Title (english)A strongly typed language for specification of deductive systems
AuthorFrano Perleta
MentorSiniša Srbljić (mentor)
Committee memberSiniša Srbljić (predsjednik povjerenstva)
Committee memberDejan Škvorc (član povjerenstva)
Committee memberAnte Đerek (član povjerenstva)
GranterUniversity of Zagreb
Faculty of Electrical Engineering and Computing
Zagreb
Defense date and country2015-02-18, Croatia
Scientific / art field,
discipline and subdiscipline		TECHNICAL SCIENCES
Computing
Abstract
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.
Abstract (english)
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.
Keywords
Keywords (english)
Languagecroatian
URN:NBNurn:nbn:hr:168:350390
Study programmeTitle: Computing
Study programme type: university
Study level: graduate
Academic / professional title: magistar/magistra inženjer/inženjerka računarstva (magistar/magistra inženjer/inženjerka računarstva)
Type of resourceText
File originBorn digital
Access conditionsClosed access
Terms of useLicence In copyright icon
Public note
Created on2019-03-13 23:50:39