The Ackermann approach for modal logic, correspondence theory and second-order reduction
The Ackermann approach for modal logic, correspondence theory and second-order reduction
复制标题
模态逻辑、对应理论和二阶约简的阿克曼方法
DOI：
10.1016/j.jal.2012.01.001
复制
发表时间：
2012
影响因子：
--
通讯作者：
Schmidt R
中科院分区：
文献类型：
--
作者：
Schmidt R
消除谓词符号上的二阶量化的问题通常是不可判定的。由于二阶量词消除的应用是模态逻辑中的对应理论，因此理解二阶量词消除方法何时成功是一个重要问题，它揭示了与一阶对应性质等价的公理类型，并可用于获得模态逻辑的完整公理化。本文介绍了一种基于阿克曼引理的替代重写方法，用于模态逻辑中的二阶量词消除。与相关方法相比，该方法包括许多增强功能：可以灵活指定需要消除的量化符号。推理规则受到与消除顺序兼容的顺序的限制，这提供了更多的控制并减少了推导中的非确定性，从而提高了效率和成功率。该方法配备了强大的冗余概念，允许灵活定义实际的简化和优化技术。我们提出正确性、终止性和规范性结果，并考虑两种应用：（i）计算模态公理和规则的一阶框架对应属性，以及（ii）将二阶模态问题重写为等效的更简单形式。该方法允许我们定义和表征两类新的公式，它们是基本的和规范的，并包含 Sahlqvist 公式类和一元归纳公式类。
The problem of eliminating second-order quantification over predicate symbols is in general undecidable. Since an application of second-order quantifier elimination is correspondence theory in modal logic, understanding when second-order quantifier elimination methods succeed is an important problem that sheds light on the kinds of axioms that are equivalent to first-order correspondence properties and can be used to obtain complete axiomatizations for modal logics. This paper introduces a substitution-rewrite approach based on Ackermannʼs Lemma to second-order quantifier elimination in modal logic. Compared to related approaches, the approach includes a number of enhancements: The quantified symbols that need to be eliminated can be flexibly specified. The inference rules are restricted by orderings compatible with the elimination order, which provides more control and reduces non-determinism in derivations thereby increasing the efficiency and success rate. The approach is equipped with a powerful notion of redundancy, allowing for the flexible definition of practical simplification and optimization techniques. We present correctness, termination and canonicity results, and consider two applications: (i) computing first-order frame correspondence properties for modal axioms and rules, and (ii) rewriting second-order modal problems to equivalent simpler forms. The approach allows us to define and characterize two new classes of formulae, which are elementary and canonical, and subsume the class of Sahlqvist formulae and the class of monadic inductive formulae.
登录
查看更多内容
DOI：
--
发表时间：
1994
期刊：
Applicable Algebra in Engineering, Communication and Computing
影响因子：
--
作者：
L. Bachmair;H. Ganzinger;Uwe Waldmann
通讯作者：
Uwe Waldmann
二阶量词消去的不动点方法及其在对应论中的应用
DOI：
--
发表时间：
1999
期刊：
影响因子：
--
作者：
Andreas Nonnengart;A. Szałas
通讯作者：
A. Szałas
论模态逻辑与经典逻辑之间的对应关系：一种自动化方法
影响因子：
0.7
作者：
A. Szałas
通讯作者：
A. Szałas
DOI：
--
发表时间：
2005
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
B. Courcelle
通讯作者：
B. Courcelle
基本规范公式：扩展 Sahlqvist 定理
DOI：
10.1016/j.apal.2005.10.005
发表时间：
2006
期刊：
Ann. Pure Appl. Log.
影响因子：
--
作者：
V. Goranko;D. Vakarelov
通讯作者：
D. Vakarelov