Bisimulacije i bisimulacijske igre za Verbruggeinu semantiku

doctoral thesis

• 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
• Created on: 2024-02-06 10:35:47