This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
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...
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...
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, ...
Lori Lorigo, Jon M. Kleinberg, Richard Eaton, Robe...
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...
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 ...
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...
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...
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...
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�...