Return to search

Įrodymų sistema koreliatyvių žinių logikai / Proof system for logic of correlated knowledge

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. / 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.

Identiferoai:union.ndltd.org:LABT_ETD/oai:elaba.lt:LT-eLABa-0001:E.02~2014~D_20141230_152716-86030
Date30 December 2014
CreatorsGiedra, Haroldas
ContributorsDZEMYDA, GINTAUTAS, BAREIŠA, EDUARDAS, KULVIETIS, GENADIJUS, VAICEKAUSKAS, RIMANTAS, ŽILINSKAS, ANTANAS, ČAPLINSKAS, ALBERTAS, PRANEVIČIUS, HENRIKAS, Vilnius University
PublisherLithuanian Academic Libraries Network (LABT), Vilnius University
Source SetsLithuanian ETD submission system
LanguageLithuanian
Detected LanguageEnglish
TypeDoctoral thesis
Formatapplication/pdf
Sourcehttp://vddb.library.lt/obj/LT-eLABa-0001:E.02~2014~D_20141230_152716-86030
RightsUnrestricted

Page generated in 0.0023 seconds