| Popis: |
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 есть конечный базис для пассивных правил |
