Verification, Induction, Termination Analysis
Verification, Induction, Termination Analysis
复制标题
验证、归纳、终止分析
DOI：
10.1007/978-3-642-17172-7_7
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Benzmüller C
中科院分区：
文献类型：
--
作者：
Benzmüller C
著名的逻辑，包括量化的多模态逻辑，可以优雅地嵌入简单类型理论（经典高阶逻辑）。此外，现成的简单类型理论推理系统存在，可以统一用于推理内和关于嵌入式逻辑。在本文中，我们专注于推理约模态逻辑，并利用我们的框架自动验证的包含和等价关系之间。相关的工作应用一阶自动定理证明的任务。我们的解决方案实现了显着的改进，最值得注意的是，在优雅和简单的问题编码以及自动化性能方面。
Prominent logics, including quantified multimodal logics, can be elegantly embedded in simple type theory (classical higher-order logic). Furthermore, off-the-shelf reasoning systems for simple type type theory exist that can be uniformly employed for reasoningwithinandaboutembedded logics. In this paper we focus on reasoningaboutmodal logics and exploit our framework for the automated verification of inclusion and equivalence relations between them. Related work has applied first-order automated theorem provers for the task. Our solution achieves significant improvements, most notably, with respect to elegance and simplicity of the problem encodings as well as with respect to automation performance.