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

DOI10.1007/978-3-319-66107-0_21zbMATH Open1484.68311DBLPconf/itp/KohlhaseMOR17OpenAlexW2750522419WikidataQ57389276 ScholiaQ57389276MaRDI QIDQ1687752FDOQ1687752

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

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

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)

Cites Work

• A Search Engine for Mathematical Formulae
• System Description: MathHub.info
• The Mizar Mathematical Library in OMDoc: translation and applications
• How to identify, translate and combine logics?
• Generic Literals
• A scalable module system
• A framework for defining logics
• Towards Knowledge Management for HOL Light
• HOL(y)Hammer: online ATP service for HOL Light
• Translating higher-order clauses to first-order clauses
• A mechanized translation from higher-order logic to set theory
• Title not available (Why is that?)
• Matching Concepts across HOL Libraries
• Importing HOL Light into Coq
• A Modular Type Reconstruction Algorithm
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge

Cited In (2)

• Title not available (Why is that?)
• Experiences from exporting major proof assistant libraries

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)