hrvatski

Strogo tipiziran jezik za opis deduktivnih sustava

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.

ovisni tipovi; propozicije kao tipovi; automatska provjera dokaza; logičko programiranje

nije evidentirano