Метод взаимного перевода индексированных и табличных выводов.

Abstract

There “indexed derivation” means a derivation in Gentzen-style modal sequent calculi with indexed formulae. These calculi admit direct constructive proof of cut-elimination theorem. As consequence we have explicit procedure of mutual transformation for indexed and tableaux-style derivations in so called “normal” modal propositional systems.