The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
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 Management.
The paper describes an innovative technique for efficient retrieval of mathematical statements from large repositories, developing and substantially improving the metadata-based approach introduced in [10].
We present a formalization of the axiomatic set theory ZF which reflects real mathematical practice, and is easy for mechanical manipulation and interactive theorem proving. Unlike the standard first-order formalizations, our version provides a rich class of abstraction terms denoting sets on the one hand, and is based on purely syntactical (rather than semantic) considerations on the other hand.
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 efficient authoring of new Mizar articles it is necessary to have good tools for searching and browsing this library. It would be ideal if such tools were simple, intuitive and easy to access. Particularly, they should provide interactive...
Finding required information in a library of mathematics can be problematic, just as in any other library. However, so far, there are no strong search methods based on the semantics of formal mathematics. This paper describes a new approach based on latent semantic indexing (LSI). Using this, the semantics of terms need not be explicitly defined but is indirectly inferred from a body of documents...
Web Service technology is increasingly being used to develop distributed applications, however the convention is to describe individual services in terms of the interfaces that they expose, rather in terms of the function that they perform. In this paper we describe a mechanism for encoding information about mathematical web services which is rich enough to allow a potential client to identify automatically...
We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a mathematical library of constructive algebra and analysis formalized in the theorem prover Coq. We explain the structure and the contents of the library and we discuss the motivation and some (possible) applications of such a library. The development of C-CoRN is part of a larger goal to design a computer system...
In this paper we describe the semantic analysis of differential equations given in the ubiquitous formats MathML and OpenMath. The analysis is integrated in a deployed Web indexing framework. Starting from basic classifications for differential equations the proposed system architecture is amenable to extensions for further reconstruction of mathematical content on the Web. The syntactic analysis...
The problem of the integrity of a computer managed mathematical knowledge repository is in the heart of MKM since mathematical vernacular is a language permitting plenty of ways in expressing the same meaning. The users of the library are naturally forced to choose certain way among many similar ones, unless different approaches are provided by developers. Mizar is a system for formalizing mathematical...
Theories play an important role in building mathematical knowledge repositories. Organizing knowledge in theories is an obvious approach to cope with the growing number of definitions, theorems, and proofs. However, they are also a matter of subject on their own: developing a new piece of mathematics often relies on extending or combining already developed theories in this way reusing definitions...
In this paper we are interested in the process of formalizing a mathematical text written in Common Mathematical Language (CML) into type theory using intermediate representations in Weak Type Theory [8] and in type theory with open terms. We demonstrate that this method can be reliable not only in the sense that eventually we get formally verified mathematical texts, but also in the sense that we...
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 multiple views of mathematical texts, including natural language views using the exact text that the mathematician wants to use. Thus, MathLang now supports the ability to capture the essential mathematical structure of mathematics...
Automated knowledge management techniques critically depend on the availability of semantically enhanced documents which are hard to come by in practice. Starting from a detailed look at the motivations of users to produce semantic data, we argue that the authoring problem experienced by MKM is actually an author’s dilemma. An analysis of the content authoring process suggests that the dilemma can...
The more extensive use of diagrammatic representations as a tool for managing complexity and communication problems of mathematical knowledge is advocated in the paper. The specifics of this representation tool are introduced, including the problems with using diagrams in mathematics, issues of proper design of diagrams, specification of main usage types of mathematical diagrams and ways of their...
We extend first-order logic with sequence variables and sequence functions. We describe syntax, semantics and inference system for the extension, define an inductive theory with sequence variables and formulate induction rules. The calculus forms a basis for the top-down systematic theory exploration paradigm.
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, it becomes increasingly valuable to find automated means to manage this data and capture semantics such as relatedness and significance. We apply graph-based approaches, such as HITS, or Hyperlink Induced Topic Search, [11]...
In this paper, the current state of the System for Automated Deduction, SAD, is described briefly. The system may be considered as the modern vision of the Evidence Algorithm programme advanced by Academician V. Glushkov in early 1970s. V. Glushkov proposed to make investigation simultaneously into formalized languages for presenting mathematical texts in the form most appropriate for a user, formalization...
Mathematical tools such as computer algebra systems and interactive and automated theorem provers are complex systems and can perform difficult computations. Typically, such tools are used by a (small) group of particularly trained and skilled users to assist in mathematical problem solving. They can also be used as back-engines for interactive exercises in learning environments. This, however, suggests...
In this paper we present a mechanism for adding interactivity to static mathematical documents, which become interactive programs that allow students to practice the resolution of problems that involve symbolic computations. The designers that use this mechanism can work in the same environment used by students when solving the problems, and they don’t need to know any programming language. The original...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.