hrvatski

Normalne forme i svojstvo konačnih modela za logiku interpretabilnosti

Rad se sastoji od tri dijela, od kojih je prvi uvodni. U prvom dijelu uvodimo logiku interpretabilnosti IL, reducirani jezik za nju, njenu sintaksu i aksiome, te dokazujemo neke rezultate unutar IL sintaktički, glavni od kojih je teorem o supstituciji. U drugom dijelu detaljno pratimo problem normalnih formi zatvorenog fragmenta neke modalne logike, i njegovo postojeće rješenje za logiku GL primjenom traga, te uvodimo pojam generaliziranog traga za logiku IL, služeći se pojmom dubine. Pomoću generaliziranog traga dokazujemo teorem o eliminaciji operatora \rhd, koji karakterizira (ne sve) situacije u kojima su IL formule ekvivalentne nekim GL formulama, te navodimo nekoliko važnih specijalnih slučajeva tipova takvih formula. Za primjenu tehnike generaliziranog traga na globalnu ekvivalenciju, dokazujemo teorem o generalizaciji, koji karakterizira globalnu ekvivalenciju formula preko lokalne ekvivalencije njihovih generalizacija. Takoder pokazujemo primjer gdje operator \rhd sigurno nije eliminabilan. Još jedan od rezultata u ovom dijelu je teorem o kratkim normalnim formama za GL. U trećem dijelu promatramo bisimulacije i n- bisimulacije Veltmanovih modela odnosno okvira, kao i veze s bisimulacijama i n- bisimulacijama GL struktura odnosno okvira. Opisujemo tehniku konstrukcije Veltmanovih modela iz GL struktura, te navodimo kako se može "podići" n-bisimulacija s GL okvira u Veltmanove okvire, služeći se pojmom dubine, ovaj put generalizirane preko omega na proizvoljne ordinale. Veza tako generalizirane dubine svjetova (koja može biti beskonačna) i modalne dubine IL formula (koja mora biti konačna) sugerira da "rezanje u dubinu", postupak prilikom uobičajenog dokaza svojstva konačnosti modela, prolazi i na Veltmanovim modelima. Također definiramo lance i Veltmanove lance, te pomoću njih navodimo primjer koji pokazuje da je slikovna konačnost nužni uvjet za Hennessy- Milnerov teorem, čak i u zatvorenom fragmentu od IL. Karakteriziramo i globalne bisimulacije pomoću pojma dubine okvira. Za kraj dajemo karakterizaciju bisimuliranosti i n- bisimuliranosti svjetova u Veltmanovim modelima preko pobjedničkih strategija u određenim igrama za dva igrača, koje su analogne igrama kakve postoje za utvrđivanje bisimuliranosti u Kripkeovim strukturama. Dokazujemo da svaka takva igra završava u konačno mnogo poteza, te koristimo rezultate iz prethodnih točaka da bismo dokazali da, usprkos tome, posjedovanje pobjedničke strategije u igri ograničenoj na n poteza za svaki n ne mora povlačiti posjedovanje pobjedničke strategije u neograničenoj igri - jer strategija ne mora biti uniformna s obzirom na n.

normalna forma ; model ; bisimulacija ; interpretabilnost

nije evidentirano