scientific article; zbMATH DE number 1951627

MaRDI QIDQ4413879zbMATH OpenFDO

Authors Claudio Sacerdoti Coen

Publication date 21 July 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2594/25940030.htm

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• A new export of the Mizar mathematical library
• Mathematical Knowledge Management
• Toward sharing libraries of mathematics between theorem provers
• A plugin to export Coq libraries to XML
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar

Cited in

(10)

• Experiences from exporting major proof assistant libraries
• A plugin to export Coq libraries to XML
• User interaction with the Matita proof assistant
• Procedural representation of CIC proof terms
• Toward sharing libraries of mathematics between theorem provers
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• A query language for formal mathematical libraries
• A Review of Mathematical Knowledge Management
• Mathematical Knowledge Management

Describes a project that uses

Uses Software

• MBase
• Coq
• Nuprl

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4413879)