Search

Formal concept analysis (FCA) comprises a set of powerful algorithms which can be used for data analysis and manipulation, and a set of visualisation tools which enable the discovery of meaningful relationships between attributes of the data. We explore the potential of combining FCA and mathematical discovery tools in order to better facilitate discovery tasks. In particular, we propose a novel lookup method for the Encyclopedia of Integer Sequences, and we show how conjectures from the Graffiti discovery program can be better understood using FCA visualisation tools. We argue that, not only can FCA tools greatly enhance the management and visualisation of mathematical knowledge, but they can also be used to drive exploratory processes. [ABSTRACT FROM AUTHOR]

In order to foster the use of proof assistance systems, we integrated the proof assistance system Ωmega with the standard scientific text-editor $_{\rm {\sc MACS}}$. We aim at a document-centric approach to formalizing and verifying mathematics and software. Assisted by the proof assistance system, the author writes her document entirely inside the text-editor in a language she is used to, that is a mixture of natural language and formulas in style. We present a basic mechanism that allows the author to define her own notation inside a document in a natural way, and use it to parse the formulas written by the author as well as to render the formulas generated by the proof assistance system. To make this mechanism effectively usable in an interactive and dynamic authoring environment, we extend it to efficiently accommodate modifications of notations, to track dependencies to ensure the right order of notations and formulas, to use the hierarchical structure of theories to prevent ambiguities, and to reuse concepts together with their notation from other documents. [ABSTRACT FROM AUTHOR]

To be effective and useful, math search systems must not only maximize precision and recall, but also present the query hits in a form that makes it easy for the user to identify quickly the truly relevant hits. To meet that requirement, the search system must sort the hits according to domain-appropriate relevance criteria, and provide with each hit a query-relevant summary of the hit target. The standard relevance measures in text search, which rely mostly on keyword frequencies and document sizes, turned out to be inadequate in math search. Therefore, alternative relevance measures must be defined, which give more weight to certain types of information than to others and take into account cross-reference statistics. In this paper, new, multidimensional relevance metrics are defined for math search, methods for computing and implementing them are discussed, and comparative performance evaluation results are presented. Query-relevant hit-summary generation is another factor that enables users to quickly determine the relevance of the presented hits. Although the hit title accompanied by a few leading sentences from the target document is simple to produce, this often fails to convey to the user the document's relevant excerpts. This shifts the burden onto the user to pursue many of the hits, and read significant portions of their target documents, to finally locate the wanted documents. Clearly, this task is too time-consuming and should be largely automated. This paper presents query-relevant hit-summary generation methods, outlines implementation strategies, and presents performance evaluation results. [ABSTRACT FROM AUTHOR]

The disambiguation approach to the input of formulae enables the user to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae we want to present only errors related to the interpretation meant by the user, hiding errors related to other interpretations (spurious errors). We propose a heuristic to recognize spurious errors, which has been integrated with the disambiguation algorithm of [6]. [ABSTRACT FROM AUTHOR]

We explore mathematical knowledge in the field of electrical engineering and claim that electrical engineering is a suitable area of application for mathematical knowledge management: We show that mathematical knowledge arising in electrical engineering can be successfully handled by existing MKM systems, namely by the Mizar system. To this end we consider in this paper network theory and in particular stability of networks. As an example for mathematical knowledge in electrical engineering we present a Mizar formalization of Schur's theorem. Schur's theorem provides a recursive, easy method to check for BIBO-stability of networks. [ABSTRACT FROM AUTHOR]

Even though only a tiny fraction of mathematical knowledge is available digitally (e.g in theorem prover or computer algebra libraries, in documents with content-markup), our current retrieval methods are already inadequate. With further increase in digitalization of mathematics the situation will get worse without significant advances. When searching a formula, we often want to find not only structurally identical occurrences, but also all (logically) equivalent ones. Furthermore, we want to retrieve whole mathematical theories (i.e. objects with prescribed properties), and we want to find them irrespective of the nomenclature chosen in the respective formalization. In this paper, we propose a normalization-based approach to mathematical formula and theory retrieval modulo an equivalence theory and concept renaming, and apply the proposed algorithm to end-user querying and knowledge sharing. We test the implementation by applying it to a first-order translation of the Mizar library. [ABSTRACT FROM AUTHOR]

This article describes an approach to searching for mathematical notation. The approach aims at a search system that can be effectively and economically deployed, and that produces good results with a large portion of the mathematical content freely available on the World Wide Web today. The basic concept is to linearize mathematical notation as a sequence of text tokens, which are then indexed by a traditional text search engine. However, naive generalization of the "phrase query" of text search to mathematical expressions performs poorly. For adequate precision and recall in the mathematical context, more complex combinations of atomic queries are required. Our approach is to query for a weighted collection of significant subexpressions, where weights depend on expression complexity, nesting depth, expression length, and special boosting of well-known expressions. To make this approach perform well with the technical content that is readily obtainable on the World Wide Web, either directly or through conversion, it is necessary to extensively normalize mathematical expression data to eliminate accidently or irrelevant encoding differences. To do this, a multi-pass normalization process is applied. In successive stages, MathML and XML errors are corrected, character data is canonicalized, white space and other insignificant data is removed, and heuristics are applied to disambiguated expressions. Following these preliminary stages, the MathML tree structure is canonicalized via an augmented precedence parsing step. Finally, mathematical synonyms and some variable names are canonicalized. [ABSTRACT FROM AUTHOR]

Mizar provides built-in support for defining structures (aggregates) like the familiar algebraic systems of groups or vector spaces. When trying to employ these structures for formalizing graph algorithms we ran into substantial problems stemming from the fact that fields in Mizar structures are not first class objects. We decided that a different approach would be more suitable for the task at hand. Starting from scratch, we modeled structures as functions. In our approach, fields in structures are first class objects and just this one factor made working with graph algorithms much more convenient. We report on our experience and argue that our approach to aggregates is more suitable for a proof assistant like Mizar. [ABSTRACT FROM AUTHOR]

The interest of the field of Mathematical Knowledge Management is predicated on the assumption that by investing into markup or formalization of mathematical knowledge, we can reap benefits in managing (creating, classifying, reusing, verifying, and finding) mathematical theories, statements, and objects. This global value proposition has been used to motivate the pursuit of technologies that can add machine support to these knowledge management tasks. But this (rather naive) technology-centered motivation takes a view merely from the global (macro) perspective, and almost totally disregards the user's point of view and motivations for using it, the local (micro) perspective. In this paper we go a first step into a more principled analysis of the MKM value proposition by focusing on motivations for mathematical search engines from the micro perspective. We will use a table-based method called the "Added-Value Analysis" (AVA) developed by one of the authors. Even though we apply the AVA only to mathematical search engines, the method quickly leads to value considerations that are relevant for the whole field of MKM. [ABSTRACT FROM AUTHOR]

There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts (e.g., chapter, section, theorem or proof ) and identifying statements according to their logical importance (e.g., theorem is more important than lemma). Such narrative/structuring labels guide the reader's navigation of the text and form the key components in the reasoning structure of the theory reflected in the text. We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a "proof" justifies a "theorem" but cannot justify an "axiom") and (2) checking that the logical precedences in the document are self-consistent. The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle. [ABSTRACT FROM AUTHOR]

Methods for computerised mathematics have found little appeal among mathematicians because they call for additional skills which are not available to the typical mathematician. We herein propose to reconcile computerised mathematics to mathematicians by restoring natural language as the primary medium for mathematical authoring. Our method associates portions of text with grammatical argumentation roles and computerises the informal mathematical style of the mathematician. Typical abbreviations like the aggregation of equations a = b > c, are not usually accepted as input to computerised languages. We propose specific annotations to explicate the morphology of such natural language style, to accept input in this style, and to expand this input in the computer to obtain the intended representation (i.e., a = b and b > c). We have named this method syntax souring in contrast to the usual syntax sugaring. All results have been implemented in a prototype editor developed on top of $_{{\rm {\sc MACS}}}$ as a GUI for the core grammatical aspect of MathLang, a framework developed by the ULTRA group to computerise and formalise mathematics. [ABSTRACT FROM AUTHOR]

We have formalized material from an introductory real analysis textbook in the proof assistant Scunak. Scunak is a system based on set theory encoded in a dependent type theory. We use the formalized material to illustrate some interesting aspects of the relationship between informal presentations of mathematics and their formal representation. We focus especially on a representative example proved using the system. [ABSTRACT FROM AUTHOR]

Logiweb is an open source, distributed system for publication of machine checked mathematics. It covers all aspects of electronic publishing: high typographical quality, archival, handling of references to previously published results, and publication of refereed volumes. The present paper is itself produced using Logiweb; and the paper is formally correct in the sense that it has been verified by Logiweb. The paper describes the implementation layers of the Logiweb system as seen by the user: the programming layer, the metalogic layer, the tactic layer, and the object proof layer. [ABSTRACT FROM AUTHOR]

One major goal of Mathematical Knowledge Management is building extensive repositories, in which the mathematical knowledge has been verified. It appears, however, that maintaining such a repository is as hard as building it - especially for an open collection with a large number of contributors. In this paper we argue that even careful reviewing of contributions cannot cope with the task of keeping a mathematical repository efficient and clearly arranged in the long term. We discuss reasons for revisions of mathematical repositories accomplished by the "core implementors" and illustrate our experiences with revisions of MML, the Mizar Mathematical Library. [ABSTRACT FROM AUTHOR]

We present a new framework for the online development of formalized mathematics. This framework allows wiki-style collaboration while providing users with a rendered and browsable version of their work. We describe a prototype based on Coq, its web interface as implemented by the second author, and a modified version of the MediaWiki code-base. We discuss open issues such as dependencies and repository consistency. We explain limitations of the current prototype and we give a perspective towards a more robust solution. [ABSTRACT FROM AUTHOR]

From the very beginning of the development of the Mizar system experiments with using Mizar as a tool for teaching mathematics have been conducted. Numerous organized courses were based on different versions of the system: starting from the first implementation of its processor, through Mizar-MSE, Mizar-4 and PC-Mizar up till its present version. Now Mizar with its mathematical library gives us quite new didactic possibilities. The purpose of this paper is to present a certain course on logic and set theory offered by our Institute for freshman students. The course employs Mizar as the main tool of instruction. In the paper we discuss the organization of this course and describe some examples of students' tasks. Finally, some conclusions and remarks are given. [ABSTRACT FROM AUTHOR]

This paper introduces Proof General Kit, a framework for software components tailored to interactive proof development. The goal of the framework is to enable flexible environments for managing formal proofs across their life-cycle: creation, maintenance and exploitation. The framework connects together different kinds of component, exchanging messages using a common communication infrastructure and protocol called PGIP. The main channel connects provers to displays. Provers are the back-end interactive proof engines and displays are components for interacting with the user, allowing browsing or editing of proofs. At the core of the framework is a broker middleware component which manages proof-in-progress and mediates between components. [ABSTRACT FROM AUTHOR]

In this paper we address the problem of reconstructing a higher order, checkable proof object starting from a proof trace left by a first order automatic proof searching procedure, in a restricted equational framework. The automatic procedure is based on superposition rules for the unit equality case. Proof transformation techniques aimed to improve the readability of the final proof are discussed. [ABSTRACT FROM AUTHOR]

A prototype for a web application designed to symbolically process locus, proof and discovery tasks on geometric diagrams created with the commercial dynamic geometry systems Cabri, The Geometer's Sketchpad and Cinderella is presented. The application, named LAD (acronym for Locus-Assertion-Discovery) and thought of as a remote add-on for the considered DGS, follows the Groebner basis method relying on CoCoA and a Mathematica kernel for the involved symbolic computations. From the DGS internal textual representation of a geometric diagram, an OpenMath (i.e. semantic based) description of the requested task is created using the elements in the plangeo OpenMath content dictionaries. A review of the elements included in these CDs is given and two new elements proposed, namely locus and discovery. Everything is finally thoroughly illustrated with examples. LAD is freely accessible at http://nash.sip.ucm.es/LAD/LAD.html. [ABSTRACT FROM AUTHOR]

We address the problem of automatic synthesis of decision procedures. Our synthesis mechanism consists of several stages and sub-mechanisms and is well-suited to the proof-planning paradigm. The system (adeptus), that we present in this paper, synthesised a decision procedure for ground arithmetic completely automatically and it used some specific method generators in generating a decision procedure for linear arithmetic, in only a few seconds of cpu time. We believe that this approach can lead to automated assistance in constructing decision procedures and to more reliable implementations of decision procedures. [ABSTRACT FROM AUTHOR]

A vector-product space is a component-free representation of the common three-dimensional Cartesian vector space. The components of the vectors are invisible and formally inaccessible, although expressions for the components could be constructed. Expressions that have been built from the scalar and vector products can be simplified using a rule-based system. In order to develop and specify the system, an axiomatic system for a vector-product space is given. In addition, a brief description is given of an implementation in Aldor. The present work provides simplification functionality which overcomes difficulties encountered in earlier packages. [ABSTRACT FROM AUTHOR]

This paper looks at the feasibility of applying the quantifier elimination program QEPCAD-B to obtain quantifier-free conditions for the approximate factorization of a simple hyperbolic linear partial differential operator (LPDO) of order 2 over some given bounded rectangular domain in the plane. A condition for approximate factorization of such an operator to within some given tolerance over some given bounded rectangular domain is first stated as a quantified formula of elementary real algebra. Then QEPCAD-B is applied to try to eliminate the quantifiers from the formula. While QEPCAD-B required too much space and time to finish its task, it was able to find a partial solution to the problem. That is, it was able to find a nontrivial quantifier-free sufficient condition for the original quantified formula. [ABSTRACT FROM AUTHOR]

We present a prototype of a computer algebra system that is built on top of a proof assistant, HOL Light. This architecture guarantees that one can be certain that the system will make no mistakes. All expressions in the system will have precise semantics, and the proof assistant will check the correctness of all simplifications according to this semantics. The system actually proves each simplification performed by the computer algebra system. Although our system is built on top of a proof assistant, we designed the user interface to be very close in spirit to the interface of systems like Maple and Mathematica. The system, therefore, allows the user to easily probe the underlying automation of the proof assistant for strengths and weaknesses with respect to the automation of mainstream computer algebra systems. The system that we present is a prototype, but can be straightforwardly scaled up to a practical computer algebra system. [ABSTRACT FROM AUTHOR]

An axiomatic theory represents mathematical knowledge declaratively as a set of axioms. An algorithmic theory represents mathematical knowledge procedurally as a set of algorithms. A biform theory is simultaneously an axiomatic theory and an algorithmic theory. It represents mathematical knowledge both declaratively and procedurally. Since the algorithms of algorithmic theories manipulate the syntax of expressions, biform theories—as well as algorithmic theories—are difficult to formalize in a traditional logic without the means to reason about syntax. Chiron is a derivative of von-Neumann-Bernays-Gödel (nbg) set theory that is intended to be a practical, general-purpose logic for mechanizing mathematics. It includes elements of type theory, a scheme for handling undefinedness, and a facility for reasoning about the syntax of expressions. It is an exceptionally well-suited logic for formalizing biform theories. This paper defines the notion of a biform theory, gives an overview of Chiron, and illustrates how biform theories can be formalized in Chiron. [ABSTRACT FROM AUTHOR]

This paper reports on ongoing work on the project of representing the Kenzo system [15] in type theory [11]. [ABSTRACT FROM AUTHOR]

Many functions in classical mathematics are largely defined in terms of their derivatives, so Bessel's function is "the" solution of Bessel's equation, etc. For definiteness, we need to add other properties, such as initial values, branch cuts, etc. What actually makes up "the definition" of a function in computer algebra? The answer turns out to be a combination of arithmetic and analytic properties. [ABSTRACT FROM AUTHOR]

We address some aspects of a system architecture for mathematical assistants that integrates calculations and deductions by common infrastructure within the Isabelle theorem proving environment. Here calculations may refer to arbitrary extra-logical mechanisms, operating on the syntactic structure of logical statements. Deductions are devoid of any computational content, but driven by procedures external to the logic, following to the traditional "LCF system approach". The latter is extended towards explicit dependency on abstract theory contexts, with separate mechanisms to interpret both logical and extra-logical content uniformly. Thus we are able to implement proof methods that operate on abstract theories and a range of particular theory interpretations. Our approach is demonstrated in Isabelle/HOL by a proof-procedure for generic ring equalities via Gröbner Bases. [ABSTRACT FROM AUTHOR]

In previous papers we described the implementation of a system which combines mathematical object generation, transformation and filtering, conjecture generation, proving and disproving for mathematical discovery in non-associative algebra. While the system has generated novel, fully verified theorems, their construction involved a lot of ad hoc communication between disparate systems. In this paper we carefully reconstruct a specification of a sub-process of the original system in a framework for trustable communication between mathematics systems put forth by us. It employs the concept of biform theories that enables the combined formalisation of the axiomatic and algorithmic theories behind the generation process. This allows us to gain a much better understanding of the original system, and exposes clear generalisation opportunities. [ABSTRACT FROM AUTHOR]

In this paper, an approach to integrate an already-written Common Lisp program for algebraic manipulation with ACL2 proofs of properties of that program is presented. We report on a particular property called "cancellation theorem", which has been proved in ACL2, and could be applied to several problems in the field of Computational Algebraic Topology. [ABSTRACT FROM AUTHOR]

The development of e-Science (cyberScience, Grid, etc.) is starting to become a reality with formalised data resources, services on demand, domain-specific search engines, digital repositories, etc. Increasingly STM information will be contained in compound XML documents, representing scientific communication (articles, theses, repository entries, etc.). In physical sciences such as chemistry, materials science, engineering, physics, earth sciences, these "datuments" [1] normally contain hypertext, graphics, tables, graphs and numerical data, mathematical objects and relationships. In addition they may also contain domain-specific content such as chemical formula and reactions, thermodynamic and mechanical properties, electric, magnetic and optical properties. Among the domain-specific languages, CML (Chemical Markup Language) is the oldest and broadest, and is now being actively used for publishing by the Royal Society of Chemistry (Project Prospect [2]) which gives an idea of what chemistry in datuments can look like. CML has had to develop the domain-specific objects (molecules, atoms, bonds, spectra, crystallography, etc.) and the relationships between them. However, due to the text-based nature of early XML, it has also had to design an implement domain-independent infrastructure which can support much of physical science. Originally called STMML [3] it supports data types (float, integer, complex, etc.), data structures (arrays, lists, matrices, etc.), geometrical concepts (points, planes, lines, etc.) and scientific units of measurement. In addition CML bases much of its flexibility one usercreated dictionaries (ontologies) which are hyperlinked from objects in the datuments. [ABSTRACT FROM AUTHOR]

The On-Line Encyclopedia of Integer Sequences (or OEIS) is a database of some 130000 number sequences. It is freely available on the Web (http://www.research.att.com/~njas/sequences/) and is widely used. There are several ways in which it benefits research: 1It serves as a dictionary, to tell the user what is known about a particular sequence. There are hundreds of papers which thank the OEIS for assistance in this way.1The associated Sequence Fans mailing list is a worldwide network which has evolved into a powerful machine for tackling new problems.1As a direct source of new theorems, when a sequence arises in two different contexts.1As a source of new research, when one sees a sequence in the OEIS that cries out to be analyzed. The 40-year history of the OEIS recapitulates the story of modern computing, from punched cards to the internet. The talk will be illustrated with numerous examples, emphasizing new sequences that have arrived in the past few months. Many open problems will be mentioned. Because of the profusion of books and journals, volunteers play an important role in maintaining the database. If you come across an interesting number sequence in a book, journal or web site, please send it and the reference to the OEIS. (You do not need to be the author of the sequence to do this.) There is a web site for sending in "Comments" or "New sequences". Several new features have been added to the OEIS in the past year. Thanks to the work of Russ Cox, searches are now performed at high speed, and thanks to the work of Debby Swayne, there is a button which displays plots of each sequence. Finally, a "listen" button enables one to hear the sequence played on a musical instrument (try Recamáan's sequence A005132!). [ABSTRACT FROM AUTHOR]