Bisimulacije i bisimulacijske igre za Verbruggeinu semantiku

doktorski rad

• Naslov (engleski): Bisimulations and bisimulation games for Verbrugge semantics
• Autor: Sebastijan Horvat
• Mentor: Mladen Vuković (mentor)
• Mentor: Tin Perkov (komentor)
• Član povjerenstva: Vedran Čačić (predsjednik povjerenstva)
• Član povjerenstva: Marko Horvat (član povjerenstva)
• Član povjerenstva: Tomislav Šikić (član povjerenstva)
• Član povjerenstva: Zvonko Iljazović (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Prirodoslovno-matematički fakultet; (Matematički odsjek); Zagreb
• Datum i država obrane: 2024-01-24, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: PRIRODNE ZNANOSTI; Matematika
• Univerzalna decimalna klasifikacija (UDC): 51 - Matematika

Sažetak

U ovoj disertaciji proučavaju se bisimulacije i bisimulacijske igre za Verbruggeinu semantiku logike interpretabilnosti. Prvo se razmatraju bisimulacije i konačne bisimulacije za Verbruggeinu semantiku koje su se do sad koristile u literaturi. Dokazuju se svojstva koja one posjeduju te se ističu problemi koji se javljaju pri korištenju tih pojmova. Zatim se daju nove verzije definicija bisimulacija i konačnih bisimulacija koje se nazivaju slabe bisimulacije i konačne slabe bisimulacije (ili w-bisimulacije i n-w-bisimulacije). Dokazuje se da ti novi pojmovi zadržavaju sva dobra svojstva kao i bisimulacije i konačne bisimulacije, ali da vrijedi i više, tj. da nema problema koji su se javljali s ranijim definicijama. Kako bi se u dokazima lakše dokazala (n-)w-bisimuliranost svjetova, dokazuje se da je (n-)w-bisimuliranost svjetova ekvivalentna pobjedničkoj strategiji branitelja u odgovarajućim igrama (koje se nazivaju (n-)w-bisimulacijske igre). U nastavku se izlažu nove definicije vezane uz alate koji se koriste pri dokazivanju teorema karakterizacije, a to su standardna translacija te q-saturirano raspetljavanje. Preciznije, definira se signatura jezika dvosortne logike prvog reda u čije će formule standardna translacija preslikavati formule logike interpretabilnosti. Korištenjem svojstava q-saturiranog raspetljavanja i metode selekcije dokazuje se svojstvo konačnih modela za logiku interpretabilnosti. Konačno, korištenjem prethodno uvedenih pojmova i dokazanih rezultata, dokazuje se glavni rezultat ovog rada. Riječ je o analogonu van Benthemovog teorema karakterizacije za logiku intepretabilnosti uz Verbruggeinu semantiku koji pokazuje da logika interpretabilnosti uz Verbruggeinu semantiku odgovara fragmentu dvosortne logike prvog reda koji je invarijantan na w-bisimulacije.

Sažetak (engleski)

This doctoral thesis deals with bisimulations and bisimulation games for Verbrugge semantics of interpretability logic. First, bisimulations and finite bisimulations for Verbrugge semantics that have been used in the literature so far are considered. The properties they possess are proved and the problems that arise when using these notions are highlighted. Then, new notions of the bisimulations and finite bisimulations are given, which are called weak bisimulations and finite weak bisimulations (or w-bisimulations and n-w-bisimulations). It is proved that these new notions still have all the good properties of bisimulations and finite bisimulations, but that they also possess more good properties, i.e. that there are no problems that occurred with earlier definitions. In order to obtain a simpler technique for proving (n-)w-bisimilarity of two worlds in Verbrugge models, it is proved that (n-)w-bisimilarity of worlds is equivalent to the winning strategy of the defender in the corresponding games (called (n-)w-bisimulation games). In the next part of the thesis, new definitions related to the tools used in proving the characterization theorem are presented, namely standard translation and q-saturated unravelling. More precisely, the signature of the language of the two-sorted first-order logic is defined, into whose formulas the standard translation will map the formulas of the interpretability logic IL. Using the properties of q-saturated unravelling and the selection method, the finite model property of interpretability logic IL is proved. Finally, using previously introduced concepts and proved results, the main result of this paper is proved. It is an analogue of van Benthem’s characterization theorem for the logic of interpretability IL with respect to Verbrugge’s semantics, which shows that the logic of interpretability with Verbrugge’s semantics precisely corresponds to a fragment of the two-sorted first-order logic that is invariant to w-bisimulations.

• Ključne riječi: logika interpretabilnosti; Verbruggeina semantika; bisimulacije; bisimulacijske igre; slabe bisimulacije; slabe bisimulacijske igre; van Benthemov teorem karakterizacije
• Ključne riječi (engleski): interpretability logics; Verbrugge semantics; bisimulations; bisimulation games; weak bisimulations; weak bisimulation games
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:217:999309
• Studijski program: Naziv: Matematika; Vrsta studija: sveučilišni; Stupanj studija: doktorski studij; Akademski / stručni naziv: doktor/doktorica u području prirodnih znanosti (dr. sc. natur.)
• Vrsta resursa: Tekst
• Opseg: v, 176 str.
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Otvoreni pristup
• Datum i vrijeme pohrane: 2024-02-06 10:35:47