Mathematical libraries as proof assistant environments
From MaRDI portal
Recommendations
- A proof-centric approach to mathematical assistants
- From proof-assistants to distributed libraries of mathematics: Tips and pitfalls
- Toward sharing libraries of mathematics between theorem provers
- Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
- Mathematical Knowledge Management
- Designing mathematical libraries based on requirements for theorems
- The role of the Mizar mathematical library for interactive proof development in Mizar
Cited in
(17)- A compact kernel for the calculus of inductive constructions
- Aligning concepts across proof assistant libraries
- Maintaining a library of formal mathematics
- User interaction with the Matita proof assistant
- Designing mathematical libraries based on minimal requirements for theorems
- Toward sharing libraries of mathematics between theorem provers
- Reduction and conversion strategies for the calculus of (co)inductive constructions. I
- From proof-assistants to distributed libraries of mathematics: Tips and pitfalls
- An Interactive Driver for Goal-directed Proof Strategies
- Mtac: a monad for typed tactic programming in Coq
- Information-intensive proof technology
- Mathematical Knowledge Management
- Formal Reasoning Using Distributed Assertions
- Interacting safely with an unsafe environment
- Pure type systems without explicit contexts
- Organization, transformation, and propagation of mathematical knowledge in mega
- A proof-centric approach to mathematical assistants
This page was built for publication: Mathematical libraries as proof assistant environments
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5313072)
