Mathematical libraries as proof assistant environments
In: MKM 2004 : mathematical knowledge management (Bialowieza, 19-21 September 2004)Lecture notes in computer science :332-346
Konferenz
- print, 11 ref
Zugriff:
In this paper we analyse the modifications on logical operations - as proof checking, type inference, reduction and convertibility - that are required for the identification of a proof assistant environment with a distributed mathematical library, focusing on proof assistants based on the Curry-Howard isomorphism. This identification is aimed at the integration of Mathematical Knowledge Management tools with interactive theorem provers: once the distinction between the proof assistant environment and a mathematical library is blurred, it is possible to exploit Mathematical Knowledge Management rendering, indexing and searching services inside an interactive theorem prover, a first step towards effective loosely-coupled collaborative mathematical environments.
Titel: |
Mathematical libraries as proof assistant environments
|
---|---|
Autor/in / Beteiligte Person: | SACERDOTI COEN, Claudio |
Link: | |
Quelle: | MKM 2004 : mathematical knowledge management (Bialowieza, 19-21 September 2004)Lecture notes in computer science :332-346 |
Veröffentlichung: | Berlin: Springer, 2004 |
Medientyp: | Konferenz |
Umfang: | print, 11 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|