Open AccessSaturation method for reflexive common knowledge logic
Author(s) -
Regimantas Pliuškevičius,
Aurimas Paulius Girčys
Publication year - 2012
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.a.2012.19
Subject(s) - reflexivity , axiom , saturation (graph theory) , operator (biology) , computer science , mathematics , calculus (dental) , algorithm , sociology , chemistry , geometry , combinatorics , social science , biochemistry , repressor , transcription factor , gene , medicine , dentistry
This paper discusses the use of saturation procedure in order to check looping sequents in reflexive common knowledge logic. Traditional approach states that common knowledge operator is defined by some induction-like axiom and requires the use of some looping sequents. The loopcheck-free saturation-like procedure lets us obtain special loopfree sequents.