Automated proof system for logic of correlated knowledge is presented in the dissertation. The system consists of the sequent calculus GS-LCK and the proof search procedure GS-LCK-PROC. Sequent calculus is sound, complete and satisfy the properties of invertibility of rules, admissibility of weakening, contraction and cut. The procedure GS-LCK-PROC is terminating and allows to check if the sequent is provable. Also decidability of logic of correlated knowledge has been proved. Using the terminating procedure GS-LCK-PROC the validity of all formulas of logic of correlated knowledge can be checked. / Automatinė įrodymų sistema koreliatyvių žinių logikai yra pristatoma disertacijoje. Sistemą sudaro sekvencinis skaičiavimas GS-LCK ir įrodymo paieškos procedūra GS-LCK-PROC. Sekvencinis skaičiavimas yra pagrįstas, pilnas ir tenkina taisyklių apverčiamumo, silpninimo, prastinimo ir pjūvio leistinumo savybes. Procedūra GS-LCK-PROC yra baigtinė ir leidžia patikrinti, ar sekvencija yra išvedama. Taip pat buvo įrodytas koreliatyvių žinių logikos išsprendžiamumas. Naudojant baigtinę procedūra GS-LCK-PROC, visų koreliatyvių žinių logikos formulių tapatus teisingumas gali būti patikrintas.
| Identifer | oai:union.ndltd.org:LABT_ETD/oai:elaba.lt:LT-eLABa-0001:E.02~2014~D_20141230_152734-55494 |
| Date | 30 December 2014 |
| Creators | Giedra, Haroldas |
| Contributors | DZEMYDA, GINTAUTAS, BAREIŠA, EDUARDAS, KULVIETIS, GENADIJUS, VAICEKAUSKAS, RIMANTAS, ŽILINSKAS, ANTANAS, ČAPLINSKAS, ALBERTAS, PRANEVIČIUS, HENRIKAS, Vilnius University |
| Publisher | Lithuanian Academic Libraries Network (LABT), Vilnius University |
| Source Sets | Lithuanian ETD submission system |
| Language | English |
| Detected Language | Unknown |
| Type | Doctoral thesis |
| Format | application/pdf |
| Source | http://vddb.library.lt/obj/LT-eLABa-0001:E.02~2014~D_20141230_152734-55494 |
| Rights | Unrestricted |
Page generated in 0.1207 seconds