MKM
2004
Springer
14 years 5 months ago
2004
Springer
A major obstacle for bridging the gap between textbook mathematics and formalising it on a computer is the problem how to adequately capture the intuition inherent in the mathemati...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
We propose a mathematical knowledge browser which helps people to read mathematical documents. By the browser printed mathematical documents can be scanned and recognized by OCR (O...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
As the amount of online formal mathematical content grows, for example through active efforts such as the Mathweb [21], MOWGLI [4], Formal Digital Library, or FDL [1], and others, ...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
We describe an extension of first-order logic with sequence variables and sequence functions. We define syntax, semantics and inference system for the extension so that Completen...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. Automated knowledge management techniques critically depend on the availability of semantically enhanced documents which are hard to come by in practice. Starting from a ...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
This paper reports on refinements and extensions to the MathLang framework that add substantial support for natural language text. We show how the extended framework supports mult...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. We present an overview of the current situation and recent and expected future developments in areas of copyright law and economics relevant to Mathematical Knowledge Man...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper w...
MKM
2004
Springer
14 years 5 months ago
2004
Springer
MKM
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. The Mizar system is equipped with a very large library containing tens of thousands of theorems and thousands of definitions, which often use overloaded notation. For e...