PVS Embeddings of Propositional and Quantified Modal Logic
John Rushby
SRI-CSL Technical Report, November 2017, minor revision May 2022
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.
PDF
Also available as arXiv:2205.06391
PVS Files
TBD. In the meantime, it's OK to scrape PVS text from the pdf.
BibTeX Entry
@TECHREPORT{Rushby:ModalPVS17,
AUTHOR = {John Rushby},
TITLE = {PVS Embeddings of Propositional and Quantified Modal Logic},
INSTITUTION = {Computer Science Laboratory, SRI International},
YEAR = 2017,
ADDRESS = {Menlo Park, CA},
MONTH = nov,
NOTE = {Available at \url{http://www.csl.sri.com/users/rushby/papers/modalpvs.pdf}}
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page