TABLEAU-BASED TRANSLATION FROM FIRST-ORDER LOGIC TO MODAL LOGIC

被引：0

作者：

Perkov, Tin ^{[1
]}

Mikec, Luka ^{[2
]}

机构：

[1] Univ Zagreb, Fac Teacher Educ, Chair Math & Stat, Sayska C 77, HR-10000 Zagreb, Croatia

[2] Univ Zagreb, Fac Sci, Dept Math, Bijenicka C 30, HR-10000 Zagreb, Croatia

来源：

REPORTS ON MATHEMATICAL LOGIC | 2021年 / 56卷

关键词：

modal logic; bisimulation invariance; tableaux AMS subject classification;

D O I：

10.4467/20842589RM.21.006.14375

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

We define a procedure for translating a given first-order formula to an equivalent modal formula, if one exists, by using tableau-based bisimulation invariance test. A previously developed tableau procedure tests bisimulation invariance of a given first-order formula, and therefore tests whether that formula is equivalent to the standard translation of some modal formula. Using a closed tableau as the starting point, we show how an equivalent modal formula can be effectively obtained.

引用

页码：57 / 74

页数：18