-
Meta-analysis of type theories with an application to the design of formal proofs : doctoral thesisPetković Komel, AnjaV doktorski disertaciji predstavimo meta-analizo širokega razreda splošnih teorij tipov. Osredotočimo se na tri vidike: transformacije teorij tipov, dopolnitev teorij tipov in splošen algoritem za ... preverjanje enakosti. Teorije tipov zagotavljajo matematično osnovo za mnoge dokazovalne pomočnike. Da bi lažje razumeli interakcije med teorijami, študiramo njihove meta-teoretične lastnosti in jih preverjamo z implementacijo fleksibilnega dokazovalnega pomočnika Andromeda 2, ki omogoča, da uporabnik sam poda teorijo tipov. Naša meta-analiza je zgrajena na definiciji končnih teorij tipov. Definiramo sintaktične transformacije teorij tipov in dokažemo, da tvorijo relativno monado za sintakso. Da bi vključili strukturo izpeljivosti nadgradimo definicijo v transformacije teorij tipov, ki pokrije nekatere znane primere, kot sta Curry-Howardova korespondenca in razširitev z definicijo. Nato dokažemo nekaj meta-izrekov o transformacijah. Uporabnost transformacij teorij tipov se pokaže v definiciji dopolnitve. Dokažemo izrek o dopolnitvi, ki pravi, da ima vsaka končna teorija tipov dopolnitev. Na strani implementacije oblikujemo splošen algoritem za preverjanje enakosti, ki ga lahko uporabimo na končnih teorijah tipov. Algoritem je sestavljen iz faze ekstenzionalnosti, kjer uporabljamo pravila ekstenzionalnosti, in faze normalizacije, ki temelji na pravilih za izračun. Obe vrsti pravil sta definirani s pomočjo pogoja objektne obrnljivosti. Podamo tudi zadosten sintaktični kriterij za prepoznavanje teh pravil in algoritem s preprostimi vzorci, ki pravila uporablja. Tretja komponenta algoritma je primeren pojem glavnih argumentov, ki določa normalno obliko. S spreminjanjem glavnih argumentov dobimo znane pojme, kot sta šibka in močna normalna oblika. Dokažemo, da algoritem zadošča izreku skladnosti. Algoritem je implementiran v dokazovalnem pomočniku Andromeda 2.Vrsta gradiva - disertacija ; neleposlovje za odrasleZaložništvo in izdelava - Ljubljana : [A. Petković Komel], 2021Jezik - angleškiCOBISS.SI-ID - 91931395
Povezava(-e):
Repozitorij Univerze v Ljubljani – RUL
Digitalna knjižnica Slovenije - dLib.siDostop z namenskih računalnikov v prostorih NUK
Avtor
Petković Komel, Anja
Drugi avtorji
Bauer, Andrej
Teme
Matematična logika |
Disertacije |
matematika |
logika |
odvisna teorija tipov |
algebrajska teorija |
dokazovalni pomočnik |
dopolnitev teorij tipov |
preverjanje enakosti |
mathematics |
logic |
dependent type theory |
algebraic theory |
proof assistant |
type-theoretic elaboration equality checking
Rezervirajte gradivo na želenem mestu prevzema.
Mesto prevzema |
Status gradiva | Rezervacija |
---|---|---|
Časopisna čitalnica |
prosto - za čitalnico
|
|
Velika čitalnica |
prosto - za čitalnico
|
Signatura – lokacija, inventarna št. ... |
Status izvoda |
---|---|
GS II 0000744268 glavno skladišče GS II 744268 glavno skladišče |
prosto - za čitalnico
|
Vnos na polico
Trajna povezava
- URL:
Faktor vpliva
Dostop do baze podatkov JCR je dovoljen samo uporabnikom iz Slovenije. Vaš trenutni IP-naslov ni na seznamu dovoljenih za dostop, zato je potrebna avtentikacija z ustreznim računom AAI.
Leto | Faktor vpliva | Izdaja | Kategorija | Razvrstitev | ||||
---|---|---|---|---|---|---|---|---|
JCR | SNIP | JCR | SNIP | JCR | SNIP | JCR | SNIP |
Baze podatkov, v katerih je revija indeksirana
Ime baze podatkov | Področje | Leto |
---|
Povezave do osebnih bibliografij avtorjev | Povezave do podatkov o raziskovalcih v sistemu SICRIS |
---|---|
Petković Komel, Anja | 50816 |
Bauer, Andrej | 15854 |
Izberite prevzemno mesto:
Prevzem gradiva po pošti
Obvestilo
Gesla v Splošnem geslovniku COBISS
Izbira mesta prevzema
Mesto prevzema | Status gradiva | Rezervacija |
---|
Prosimo, počakajte trenutek.
Naročanje gradiva za izposojo v čitalnice
Naročanje kopij člankov
Urnik dostave gradiva z oznako DS v signaturi