Efficient loop-check for KD 45 logic |
| |
Authors: | A Bir?tunas |
| |
Institution: | (1) Vilnius University, Naugarduko 24, LT-03225 Vilnius, Lithuania |
| |
Abstract: | We introduce a new sequent calculus for KD 45 logic. A loop-check technique is used to determine whether a sequent derivable or not. We concentrate ourselves on the
efficiency of the loop-check technique used. The efficiency is obtained by making the loop-check to act locally (then we need
to check only one or two current sequents), instead of a global loop-check used in known works as 3]. Moreover, the sequent
calculus introduced uses a marked operator □ to integrate loop-check into an inference rule.
Besides the efficient loop-check used, the sequent calculus introduced produces smaller derivation trees that reduce the derivation
time. We also prove a lemma which determines the maximal number of modality rule applications in one branch of a tree.
Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 1, pp. 55–66, January–March, 2006. |
| |
Keywords: | BDI logic loop-check sequent calculus KD45 |
本文献已被 SpringerLink 等数据库收录! |
|