PVS Embeddings of Propositional and Quantified Modal Logic

TL;DR

This paper presents a method to embed propositional and quantified modal logic within the PVS verification system, enabling formal reasoning and automation for modal logic properties.

Contribution

It introduces formal embeddings of modal logic into PVS, supporting standard syntax and automating reasoning about modal axioms, accessibility relations, and the Barcan Formula.

Findings

Formal specifications of modal axioms and accessibility properties

Verification of the Barcan Formula in different domain contexts

Enhanced automation for modal logic reasoning in PVS

Abstract

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.