Toward sharing libraries of mathematics between theorem provers (Q2782486)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Toward sharing libraries of mathematics between theorem provers |
scientific article; zbMATH DE number 1724414
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Toward sharing libraries of mathematics between theorem provers |
scientific article; zbMATH DE number 1724414 |
Statements
5 August 2002
0 references
theorem prover
0 references
semantics of a formal system
0 references
inference rule
0 references
0 references
0 references
0.8680818
0 references
0.86049736
0 references
0.8599366
0 references
0.85908157
0 references
0.8416597
0 references
0.83771896
0 references
Toward sharing libraries of mathematics between theorem provers (English)
0 references
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].
0 references
