Making PVS accessible to generic services by interpretation in a universal format
type: Item
instance of: scholarly article
title: Making PVS accessible to generic services by interpretation in a universal format
zbMATH Open document ID: 1484.68311
DOI: 10.1007/978-3-319-66107-0_21
author: Michael Kohlhase
author: Dennis Müller
author: Sam Owre
author: Florian Rabe
publication date: 2018-01-04T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 68V20
Mathematics Subject Classification ID: 68V30
zbMATH DE Number: 6821860
describes a project that uses: Coq
describes a project that uses: MathHub.info
describes a project that uses: PVS
describes a project that uses: HOL Light
describes a project that uses: OMDoc
describes a project that uses: Mizar
describes a project that uses: HOLyHammer
describes a project that uses: vis.js
Wikidata QID: Q57389276
MaRDI profile type: Publication
full work available at URL: 978-3-319-66107-0 21
OpenAlex ID: W2750522419
cites work: Matching Concepts across HOL Libraries
cites work: A framework for defining logics
cites work: The Mizar Mathematical Library in OMDoc: translation and applications
cites work: System Description: MathHub.info
cites work: Towards Knowledge Management for HOL Light
cites work: QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
cites work: A Mechanized Translation from Higher-Order Logic to Set Theory
cites work: HOL(y)Hammer: online ATP service for HOL Light
cites work: Importing HOL Light into Coq
cites work: A Search Engine for Mathematical Formulae
cites work: Q3751042
cites work: Translating higher-order clauses to first-order clauses
cites work: How to identify, translate and combine logics?
cites work: Generic Literals
cites work: A Modular Type Reconstruction Algorithm
cites work: A scalable module system
DBLP publication ID: conf/itp/KohlhaseMOR17
description: scientific article; zbMATH DE number 6821860