Paper Info
Title
Making Pvs Accessible To Generic Services By Interpretation In A Universal Format
Abstract
PVS is one of the most powerful proof assistant systems and its libraries of formalized mathematics are among the most comprehensive albeit under-appreciated ones. A characteristic feature of PVS is the use of a very rich mathematical and logical foundation, including e.g., record types, undecidable subtyping, and a deep integration of decision procedures. That makes it particularly difficult to develop integrations of PVS with other systems such as other reasoning tools or library management periphery.This paper presents a translation of PVS and its libraries to the OMDoc/MMT framework that preserves the logical semantics and notations but makes further processing easy for third-party tools. OMDoc/MMT is a framework for formal knowledge that abstracts from logical foundations and concrete syntax to provide a universal representation format for formal libraries and interface layer for machine support. Our translation allows instantiating generic OMDoc/MMT-level tool support for the PVS library and enables future translations to libraries of other systems.
Year
DOI
Venue
2017
10.1007/978-3-319-66107-0_21
INTERACTIVE THEOREM PROVING (ITP 2017)
Field
DocType
Volume
Deep integration,Programming language,Computer science,Library management,Algorithm,Subtyping,Proof assistant,Undecidable problem
Conference
10499
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
11
4
Name
Order
Citations
PageRank
Michael Kohlhase11095127.65
Dennis Muller297.43
Sam Owre31323104.39
Florian Rabe433341.66