Resolution Calculi for Non-normal Modal Logics

被引：1
|
作者：
Pattinson, Dirk [1 ]
Olivetti, Nicola [2 ]
Nalon, Claudia [3 ]
机构：
[1] Australian Natl Univ, Sch Comp, Canberra, ACT, Australia
[2] Aix Marseille Univ, CNRS, LIS, Marseille, France
[3] Univ Brasilia, Dept Comp Sci, Brasilia, DF, Brazil
来源：
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023 | 2023年 / 14278卷
关键词：
Modal Logic; Automated Reasoning; Resolution;
D O I：
10.1007/978-3-031-43513-3_18
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present resolution calculi for the cube of classical non-normal modal logics. The calculi are based on a simple clausal form that comprises both local and global clauses. Any formula can be efficiently transformed into a small set of clauses. The calculi contain uniform rules and provide a decision procedure for all logics. Their completeness is based on a new and crucial notion of inconsistency predicate, needed to ensure the usual closure properties of maximal consistent sets. As far as we know the calculi presented here are the first resolution calculi for this class of logics.
引用
收藏
页码：322 / 341
页数：20
相关论文
共 50 条
12345