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.

Mathematical Libraries as Proof Assistant Environments

SACERDOTI COEN, CLAUDIO
2004

Abstract

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.
Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings
332
346
SACERDOTI COEN, Claudio
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/9004
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact