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

DOI10.1007/978-3-319-66107-0_21zbMath1484.68311OpenAlexW2750522419WikidataQ57389276 ScholiaQ57389276MaRDI QIDQ1687752

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

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)

Related Items (2)

Unnamed Item ⋮ Experiences from exporting major proof assistant libraries

Uses Software

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

Cites Work

• Unnamed Item
• A scalable module system
• The Mizar Mathematical Library in OMDoc: translation and applications
• HOL(y)Hammer: online ATP service for HOL Light
• Translating higher-order clauses to first-order clauses
• How to identify, translate and combine logics?
• Generic Literals
• A framework for defining logics
• A Modular Type Reconstruction Algorithm
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• A Search Engine for Mathematical Formulae
• Matching Concepts across HOL Libraries
• Towards Knowledge Management for HOL Light
• System Description: MathHub.info
• Importing HOL Light into Coq
• A Mechanized Translation from Higher-Order Logic to Set Theory

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