Title Bisimulacije i bisimulacijske igre za Verbruggeinu semantiku
Title (english) Bisimulations and bisimulation games for Verbrugge semantics
Author Sebastijan Horvat
Mentor Mladen Vuković (mentor)
Mentor Tin Perkov (komentor)
Committee member Vedran Čačić (predsjednik povjerenstva)
Committee member Marko Horvat (član povjerenstva)
Committee member Tomislav Šikić (član povjerenstva)
Committee member Zvonko Iljazović (član povjerenstva)
Granter University of Zagreb Faculty of Science (Department of Mathematics) Zagreb
Defense date and country 2024-01-24, Croatia
Scientific / art field, discipline and subdiscipline NATURAL SCIENCES Mathematics
Universal decimal classification (UDC ) 51 - Mathematics
Abstract 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.
Abstract (english) 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.
Keywords
logika interpretabilnosti
Verbruggeina semantika
bisimulacije
bisimulacijske igre
slabe bisimulacije
slabe bisimulacijske igre
van Benthemov teorem karakterizacije
Keywords (english)
interpretability logics
Verbrugge semantics
bisimulations
bisimulation games
weak bisimulations
weak bisimulation games
Language croatian
URN:NBN urn:nbn:hr:217:999309
Study programme Title: Doctoral study Study programme type: university Study level: postgraduate Academic / professional title: doktor/doktorica u području prirodnih znanosti (doktor/doktorica u području prirodnih znanosti)
Type of resource Text
Extent v, 176 str.
File origin Born digital
Access conditions Open access
Terms of use
Created on 2024-02-06 10:35:47