论文标题
命题和量化模态逻辑的PVS嵌入
PVS Embeddings of Propositional and Quantified Modal Logic
论文作者
论文摘要
模态逻辑允许关于各种真理模式的推理：例如，某事可能是真实的意思，或者知道某事是真实的，而不是仅仅相信它。本报告描述了PVS验证系统中命题和量化模态逻辑的嵌入。 PV的资源允许以有吸引力的方式来完成模态逻辑的许多标准语法，同时提供有效的自动化。 该报告介绍并正式指定并验证模态逻辑中的几个标准主题，例如标准模态公理与可访问性关系的属性之间的关系，以及Barcan公式的属性及其在常数和变化域中的交谈。
Modal logics allow reasoning about various modes of truth: for example, what it means for something to be possibly true, or to know that something is true as opposed to merely believing it. This report describes embeddings of propositional and quantified modal logic in the PVS verification system. The resources of PVS allow this to be done in an attractive way that supports much of the standard syntax of modal logic, while providing effective automation. The report introduces and formally specifies and verifies several standard topics in modal logic such as relationships between the standard modal axioms and properties of the accessibility relation, and attributes of the Barcan Formula and its converse in both constant and varying domains.
