Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK

Abstract

We study unification of formulas in multi-modal LTK logic and give a syntactic description of all formulas which are non-unificable in this logic. Passive inference rules are considered, it is shown that in LTK logic there is a finite basis for passive rules

В статье исследуется унификация формул в многомодальной логике LTK и предложено синтак- сическое описание всех формул, которые не являются унифицируемыми в данной логике. Рас- смотрен вопрос пассивных правил вывода, показано, что в логике LTK есть конечный базис для пассивных правил