Making PVS accessible to generic services by interpretation in a universal format

DOI10.1007/978-3-319-66107-0_21MaRDI QIDQ1687752zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Michael Kohlhase, Dennis Müller, Sam Owre, Florian Rabe

Publication date 4 January 2018

Full work available at URL https://doi.org/10.1007/978-3-319-66107-0_21

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Mathematical knowledge management (68V30)

Recommendations

• The Mizar Mathematical Library in OMDoc: translation and applications
• Translating the IMPS theory library to MMT/OMDoc
• Translation templates to support strategy development in PVS
• The Coq library as a theory graph
• Formalising foundations of mathematics

Cites work

• scientific article; zbMATH DE number 3988745 (Why is no real title available?)
• A Modular Type Reconstruction Algorithm
• A Search Engine for Mathematical Formulae
• A framework for defining logics
• A mechanized translation from higher-order logic to set theory
• A scalable module system
• Generic literals
• HOL(y)Hammer: online ATP service for HOL Light
• How to identify, translate and combine logics?
• Importing HOL Light into Coq
• Matching concepts across HOL libraries
• QED reloaded: towards a pluralistic formal library of mathematical knowledge
• System description: MathHub.info
• The Mizar Mathematical Library in OMDoc: translation and applications
• Towards Knowledge Management for HOL Light
• Translating higher-order clauses to first-order clauses

Cited in

(4)

• Translation templates to support strategy development in PVS
• Translating the IMPS theory library to MMT/OMDoc
• Experiences from exporting major proof assistant libraries
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• PVS
• Mizar
• HOL Light
• OMDoc
• HOLyHammer
• MathHub.info
• vis.js

This page was built for publication: Making PVS accessible to generic services by interpretation in a universal format

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687752)