Toward sharing libraries of mathematics between theorem provers
From MaRDI portal
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)