Toward sharing libraries of mathematics between theorem provers
From MaRDI portal
The general problem discussed is the use of theorem provers that support the shallow embeddings of other logics. Particularly, importing mathematics from HOL to Nuprl is treated. In order to illustrate this problem, the author gives a simple version of the classical variant of Nuprl and an example of shallow embedding is presented.NEWLINENEWLINEFor the entire collection see [Zbl 0978.00029].
Recommendations
- scientific article; zbMATH DE number 1951627
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Designing mathematical libraries based on minimal requirements for theorems
- scientific article; zbMATH DE number 1552521
- Designing mathematical libraries based on requirements for theorems
- Aligning concepts across proof assistant libraries
- Shared-memory multiprocessing for interactive theorem proving
- Artificial Intelligence and Symbolic Computation
- Experiences from exporting major proof assistant libraries
Cited in
(13)- FoCaLiZe and Dedukti to the rescue for proof interoperability
- Designing mathematical libraries based on requirements for theorems
- Experiences from exporting major proof assistant libraries
- Designing mathematical libraries based on minimal requirements for theorems
- scientific article; zbMATH DE number 1113859 (Why is no real title available?)
- scientific article; zbMATH DE number 1951627 (Why is no real title available?)
- scientific article; zbMATH DE number 1424013 (Why is no real title available?)
- Hybrid interactive theorem proving using Nuprl and HOL
- Mathematical Knowledge Management
- Cooperative Repositories for Formal Proofs
- Information-intensive proof technology
- Importing mathematics from HOL into Nuprl
- Innovations in computational type theory using Nuprl
This page was built for publication: Toward sharing libraries of mathematics between theorem provers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2782486)
