Meta-analysis of type theories with an application to the design of formal proofs : doctoral thesis
Petković Komel, Anja
V 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.
Type of material - dissertation
; adult, serious
Publication and manufacture - Ljubljana : [A. Petković Komel], 2021
GS II 0000744268 glavno skladišče
GS II 744268 glavno skladišče
available - reading room
Shelf entry
Adding material to shelf was successful.
Adding material to shelf failed.
It was not necessary to add the material to the shelf.
Bibliographic material was successfully added on shelf.
Adding bibliographical material on shelf was not successful.
Material is already on the shelf.
Permalink
URL:
Impact factor
Access to the JCR database is permitted only to users from Slovenia. Your current IP address is not on the list of IP addresses with access permission, and authentication with the relevant AAI accout is required.
Year
Impact factor
Edition
Category
Classification
JCR
SNIP
JCR
SNIP
JCR
SNIP
JCR
SNIP
Select the library membership card:
DRS,
in which the journal is indexed
Database name
Field
Year
Links to authors' personal bibliographies
Links to information on researchers in the SICRIS system
Subject headings in COBISS General List of Subject Headings
Select pickup location
The material from the parent unit is free. If the material is delivered to the pickup location from another unit, the library may charge you for this service.
Naročanje gradiva za izposojo v čitalnice
Naročanje kopij člankov
Urnik dostave gradiva z oznako DS v signaturi