Generation and presentation of formal mathematical documents

MaRDI QIDQ2760868zbMATH OpenFDO

Authors Martijn Oostdijk

Publication date 13 December 2001

zbMATH Keywords

Coq theorem provertype theoretical theorem provingtype theory

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Algebraic theory of languages and automata (68Q70) Computing methodologies for text processing; mathematical typography (68U15)

Recommendations

• Formal and efficient primality proofs by use of computer algebra oracles
• Certified and portable mathematical documents from formal contexts
• Proof by computation in the Coq system
• Autarkic computations in formal proofs
• A Computational Approach to Pocklington Certificates in Type Theory

Cited in

(3)

• How to formally and efficiently prove prime(2999)
• Certified and portable mathematical documents from formal contexts
• A Computational Approach to Pocklington Certificates in Type Theory

Describes a project that uses

Uses Software

• Coq
• Theorema
• OMRS
• Nuprl
• LEGO
• CtCoq
• Analytica

This page was built for publication: Generation and presentation of formal mathematical documents

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