Tarkvarateaduse instituudi doktorant, Cheng-Syuan Wan kaitseb 25. juunil 2025. a algusega kl 14:00 (UTC +3 / Eastern European Time (EEST)) oma doktoritööd ”Pool-allstruktuursete loogikate tõestusteooria” (“Proof Theory of Semi-Substructural Logics”), juhendajad prof Tarmo Uustalu ja prof Niccolo Veltri. Kaitsmine toimub Küberneetika maja ruumis CYB-101 (Akadeemia tee 21b, Tallinn) ning on jälgitav veebirakenduse Zoom vahendusel.
Käesolevas doktoritöös „Pool-allstruktuursete loogikate tõestusteooria“ toome sisse ühe nõrkade loogikate klassi ja uurime nende tõestusteooriat.
Klassikalises loogikas huvitume valemite kui tõeväidete omavahelistest seostest. Etteantud hulga tõeste väidete kohta tahame teada, milliseid teisi väiteid saab nendest järeldada. Tõed on priilt käes – neid võib kasutada nii palju kordi, kui tarvis läheb, või üldse mitte. Intuitsionistlikus loogikas nõuab tõde küll tõestust, kuid tõeste väidete taaskasutatavus säilib.
Allstruktuursetes loogikates, näiteks lineaarloogikas, toimivad valemid aga pigem ressurssidena kui tõeväidetena. Näiteks võib tuua müügiautomaadi: kui üks purk kokakoolat maksab ühe euro, siis ühe euro sisestamisel saad täpselt ühe purgi, mitte kaks. Kui sisestad kaks eurot, ootad vastu kas kahte purki või üht purki ja ühte eurot tagasi. Loogika nõuab täpset tasakaalu: kasutatud ressursid peavad vastama saadud toodetele.
Käesolev doktoritöö toob sisse ja käsitleb loogikaid, milles järeldusseos on veelgi piiratum — nimetame neid pool-allstruktuurseteks loogikateks. Need loogikad sobivad ressursside kohta järelduste tegemiseks olukordades, kus tähtis ei ole mitte ainult ressursside kogus, vaid ka nende laekumise järjekord, ning kus ressursside järjekorra töötlemine võib olla rangelt reguleeritud. Tüüpiliselt saab ressursse töödelda vaid erilises positsioonis järjekorra ees. Sellisel juhul kehtib struktuurne seadus assotsiatiivsusest ainult ühes suunas „pool-assotsiatiivsusena“: ressursi (A ja B) ja C saab ümber töödelda ressursiks A ja (B ja C), kuid mitte vastupidi.
Doktoritöö ”Pool-allstruktuursete loogikate tõestusteooria” on avaldatud Tehnikaülikooli raamatukogu digikogus.
Juhendajad:
- prof Tarmo Uustalu (TalTech).
- kaasjuhendaja: prof Niccolo Veltri (TalTech).
Oponendid:
- prof Pierre-Louis Curien, National Centre for Scientific Research (CNRS) ja Université Paris Cité, Prantsusmaa;
- prof Peter Dybjer, Chalmers University of Technology, Rootsi.
Jälgi avalikku kaitsmist Zoomis
Meeting ID: 955 5238 4468
Passcode: 769494