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.
SACERDOTI COEN, C. (2004). Mathematical Libraries as Proof Assistant Environments. s.l : Springer.
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.