A strongly typed language for specification of deductive systems

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.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