|
|
|
|
| LEADER |
02652na a2200229 4500 |
| 003 |
HR-ZaFER |
| 008 |
160221s2015 ci ||||| m||| 00| 0 hr d |
| 035 |
|
|
|a (HR-ZaFER)ferid4583
|
| 040 |
|
|
|a HR-ZaFER
|b hrv
|c HR-ZaFER
|e ppiak
|
| 100 |
1 |
|
|a Perleta, Frano
|
| 245 |
1 |
0 |
|a Strogo tipiziran jezik za opis deduktivnih sustava :
|b diplomski rad /
|c Frano Perleta ; [mentor Siniša Srbljić].
|
| 246 |
1 |
|
|a A strongly typed language for specification of deductive systems
|i Naslov na engleskom:
|
| 260 |
|
|
|a Zagreb,
|b F. Perleta,
|c 2015.
|
| 300 |
|
|
|a 45 str. ;
|c 30 cm +
|e CD-ROM
|
| 502 |
|
|
|b diplomski studij
|c Fakultet elektrotehnike i računarstva u Zagrebu
|g smjer: Računarska znanost, šifra smjera: 56, datum predaje: 2015-02-06, datum završetka: 2015-02-18
|
| 520 |
3 |
|
|a Sažetak na hrvatskom: 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.
|
| 520 |
3 |
|
|a Sažetak na engleskom: 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.
|
| 653 |
|
1 |
|a ovisni tipovi
|a propozicije kao tipovi
|a automatska provjera dokaza
|a logičko programiranje
|
| 653 |
|
1 |
|a dependent types
|a propositions as types
|a automated proof checking
|a logic programming
|
| 700 |
1 |
|
|a Srbljić, Siniša
|4 ths
|
| 942 |
|
|
|c Y
|
| 999 |
|
|
|c 49694
|d 49694
|