Intelligent Computer Mathematics

The use of technology in schools has been one of the most debated topics around mathematics education. In some countries there is a huge investment, in others there is a downscaling. Malaysia decided in 2013 to put its 10 million students to use Google laptops and Google apps, while Australia in the same year decided it would not continue funding their own high school laptop program. Who is right from the educational point of view? The last major curriculum document written in the world to date, the Common Core State Standards-CCSS in the United States, whose mathematics part is coordinated by the well known mathematician William McCallum, sets as one of its standards for mathematical practice: “Mathematically proficient students consider the available tools when solving a mathematical problem. These tools might include pencil and paper, concrete models, a ruler, a protractor, a calculator, a spreadsheet, a computer algebra system, a statistical package, or dynamic geometry software.” Strong moves need substantiation from research, including the analysis of the existing situation in different countries. What does research say about the use of computers in schools in present time and the use of different pieces of software from spreadsheets to computer algebra systems?

As the scholarly communication system evolves to become natively web-based, hyperlinks are increasingly used to refer to web resources that are created or used in the course of the research process. These hyperlinks are subject to reference rot: a link may break or the linked content may drift and eventually no longer be representative of the content intended by the link. The Hiberlink project quantifies the problem and investigates approaches aimed at alleviating it. The presentation will provide an insight in the project’s findings that result from mining a massive body of scholarly literature spanning the period from 1997 to 2012. It will also provide an overview of components of a possible solution: pro-active web archiving, links with added attributes, and the Memento “Time Travel for the Web” protocol.

This talk will focus on the infrastructure developed for representing and accessing data (especially mathematical data) in Wolfram|Alpha, as well as on the technologies and language extensions developed in the most recent version of

Mathematica

for making this data even more computationally accessible. Based on experiences using these technologies to create a prototype semantic digital library for a subset of mathematics, we believe the ambitious dream of creating of a semantic digital library for all of mathematics is now within reach.

It is customary to assess the reliability of underground oil and gas pipelines in the presence of excessive loading and corrosion effects to ensure a leak-free transport of hazardous materials. The main idea behind this reliability analysis is to model the given pipeline system as a Reliability Block Diagram (RBD) of segments such that the reliability of an individual pipeline segment can be represented by a random variable. Traditionally, computer simulation is used to perform this reliability analysis but it provides approximate results and requires an enormous amount of CPU time for attaining reasonable estimates. Due to its approximate nature, simulation is not very suitable for analyzing safety-critical systems like oil and gas pipelines, where even minor analysis flaws may result in catastrophic consequences. As an accurate alternative, we propose to use a higher-order-logic theorem prover (HOL) for the reliability analysis of pipelines. As a first step towards this idea, this paper provides a higher-order-logic formalization of reliability and the series RBD using the HOL theorem prover. For illustration, we present the formal analysis of a simple pipeline that can be modeled as a series RBD of segments with exponentially distributed failure times.

Cylindrical algebraic decompositions (CADs) are a key tool for solving problems in real algebraic geometry and beyond. We recently presented a new CAD algorithm combining two advances: truth-table invariance, making the CAD invariant with respect to the truth of logical formulae rather than the signs of polynomials; and CAD construction by regular chains technology, where first a complex decomposition is constructed by refining a tree incrementally by constraint. We here consider how best to formulate problems for input to this algorithm. We focus on a choice (not relevant for other CAD algorithms) about the order in which constraints are presented. We develop new heuristics to help make this choice and thus allow the best use of the algorithm in practice. We also consider other choices of problem formulation for CAD, as discussed in CICM 2013, revisiting these in the context of the new algorithm.

The class of

regular propositional schemata

, discovered by Aravantinos et al. [4], is a major advancement towards more expressive classes of inductive theorems with a decidable satisfiability problem. Though more expressive than previously known decidable classes outlined by Kapur & Giesl[17], it still requires the burdensome restriction of induction with only one free parameter. In general, unrestricted usage of multiple free parameters in schematic formulae is undecidable for satisfiability [2]. In later work, Aravantinos et al. [6] introduced

normalized clause sets

which have a decision procedure for satisfiability and allow for restricted usage of multiple parameters. In our work, we investigate classes of propositional schemata which allow for multiple free parameters and are more expressive than regular schemata. Specifically, the classes we investigate have a decision procedure for satisfiability testing without requiring the additional theoretical machinery of normalized clause sets. Thus, allowing one to avoid conversion to CNF formulae. Both of the classes we introduce,

linked schemata

and

pure overlap schemata

use the machinery introduced in the earlier works of Aravantinos et al.[4] with only a slight change to the decision procedure.

We explore the application of automated reasoning techniques to unknot detection, a classical problem of computational topology. We adopt a two-pronged experimental approach, using a theorem prover to try to establish a positive result (i.e. that a knot is the unknot), whilst simultaneously using a model finder to try to establish a negative result (i.e. that the knot is not the unknot). The theorem proving approach utilises equational reasoning, whilst the model finder searches for a minimal size counter-model. We present and compare experimental data using the involutary quandle of the knot, as well as comparing with alternative approaches, highlighting instances of interest. Furthermore, we present theoretical connections of the minimal countermodels obtained with existing knot invariants, for all prime knots of up to 10 crossings: this may be useful for developing advanced search strategies.

Cylindrical algebraic decomposition(CAD) is a key tool in computational algebraic geometry, particularly for quantifier elimination over real-closed fields. When using CAD, there is often a choice for the ordering placed on the variables. This can be important, with some problems infeasible with one variable ordering but easy with another. Machine learning is the process of fitting a computer model to a complex function based on properties learned from measured data. In this paper we use machine learning (specifically a support vector machine) to select between heuristics for choosing a variable ordering, outperforming each of the separate heuristics.

This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development. Hipster can be used in two main modes. The first is

exploratory mode

, used for automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. The second is

proof mode

, used in a particular proof attempt, trying to discover the missing lemmas which would allow the current goal to be proved. Hipster’s proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. We show example uses of both modes.

Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting this analysis within the sound core of a theorem prover: HOL Light. Our definition of complex vector builds upon the definitions of complex numbers and real vectors. This extension allows us to extensively benefit from the already verified theorems based on complex analysis and real vector analysis. To show the practical usefulness of our library we adopt it to formalize electromagnetic fields and to prove the law of reflection for the planar waves.

The paper is the first of several ones [14,17] describing a mathematical structure developed in the FSTP project, mathematically modeling Substantive Patent Law (“SPL“) and its US Highest Courts‘ precedents primarily for emerging technologies inventions. Chapter 2 presents this mathematical structure comprising particularly, 3 abstraction levels - each comprising “inventive concepts“, their “subset coverings“, “concept transformations“, “induced concept relations‘, and “refinements“. Chapters 3 and 4 explain its practical application in describing an invention respectively testing it by an Innovation Expert System (IES) for its satisfying SPL.

Using the notion of “inventive concepts“ for precisely describing emerging technologies inventions has been introduced into SPL precedents by the US Supreme Court during its ongoing “SPL initiative“ - marked by its KSR/Bilski/ Mayo/ Myriad decisions. It induced, into the FSTP project, a rigorous mathematical analysis of allegedly new problems caused by these Highest Courts‘ SPL decisions about emerging technologies inventions. This analysis proved extremely fertile by enabling not only clarifying/removing obscurities in such problems but also developing powerful “patent technology“ in the FSTP project.

Access to mathematical knowledge has changed dramatically in recent years, therefore changing mathematical search practices. Our aim with this study is to scrutinize professional mathematicians’ search behavior. With this understanding we want to be able to reason why mathematicians use which tool for what search problem in what phase of the search process. To gain these insights we conducted 24 repertory grid interviews with mathematically inclined people (ranging from senior professional mathematicians to non-mathematicians). From the interview data we elicited patterns for the user group “mathematicians” that can be applied when understanding design issues or creating new designs for mathematical search interfaces.

To understand mathematical language we have to understand the words of mathematics. In particular, for machine-supported knowledge management and digital libraries, we need machine-actionable terminology databases (termbases). However, terminologies for Mathematics and related subjects differ from vocabularies for general natural languages in many ways. In this paper we analyze these and develop a data model for

SMGloM

the Semantic, Multilingual Glossary of Mathematics and show how it can be encoded in the

OMDoc

/

MMT

theory graph model. This structured representation naturally accounts for many of the terminological and ontological relations of a semantic terminology (aka. glossary). We also demonstrate how we can account for multilinguality in this setting.

Including

source of mathematical expressions, within the PDF document of a text-book or research paper, has definite benefits regarding ‘Accessibility’ considerations. Here we describe three ways in which this can be done, fully compatibly with international standards ISO 32000, ISO 19005-3, and the forthcoming ISO 32000-2 (PDF 2.0). Two methods use embedded files, also known as ‘attachments’, holding information in either

or

formats, but use different PDF structures to relate these attachments to regions of the document window. One uses structure, so is applicable to a fully ‘Tagged PDF’ context, while the other uses

tagging of the relevant content. The third method requires no tagging at all, instead including the source coding as the

relacement of a so-called ‘fake space’. Information provided this way is extracted via simple

/

/

actions, and is available to existing screen-reading software and assistive technologies.

Mathematical content is a valuable information source and retrieving this content has become an important issue. This paper compares two searching strategies for math expressions: presentation-based and content-based approaches. Presentation-based search uses state-of-the-art math search system while content-based search uses semantic enrichment of math expressions to convert math expressions into their content forms and searching is done using these content-based expressions. By considering the meaning of math expressions, the quality of search system is improved over presentation-based systems.

Content analysis of scientific publications is a nontrivial task, but a useful and important one for scientific information services. In the Gutenberg era it was a domain of human experts; in the digital age many machine-based methods, e.g., graph analysis tools and machine-learning techniques, have been developed for it. Natural Language Processing (NLP) is a powerful machine-learning approach to semiautomatic speech and language processing, which is also applicable to mathematics. The well established methods of NLP have to be adjusted for the special needs of mathematics, in particular for handling mathematical formulae. We demonstrate a mathematics-aware part of speech tagger and give a short overview about our adaptation of NLP methods for mathematical publications. We show the use of the tools developed for key phrase extraction and classification in the database zbMATH.

Wikipedia is the first address for scientists who want to recap basic mathematical and physical laws and concepts. Today, formulae in those pages are displayed as Portable Network Graphics images. Those images do not integrate well into the text, can not be edited after copying, are inaccessible to screen readers for people with special needs, do not support line breaks for small screens and do not scale for high resolution devices. Mathoid improves this situation and converts formulae specified by Wikipedia editors in a

like input format to MathML, with Scalable Vector Graphics images as a fallback solution.

When faced with the question of how to represent properties in a formal proof system any user has to make design decisions. We have proved three of the theorems from Maskin’s 2004 survey article on Auction Theory using the Isabelle/HOL system, and we have verified software code that implements combinatorial Vickrey auctions. A fundamental question in this was how to represent some basic concepts: since set theory is available inside Isabelle/HOL, when introducing new definitions there is often the issue of balancing the amount of set-theoretical objects and of objects expressed using entities which are more typical of higher order logic such as functions or lists. Likewise, a user has often to answer the question whether to use a constructive or a non-constructive definition. Such decisions have consequences for the proof development and the usability of the formalization. For instance, sets are usually closer to the representation that economists would use and recognize, while the other objects are closer to the extraction of computational content. We have studied the advantages and disadvantages of these approaches, and their relationship, in the concrete application setting of auction theory. In addition, we present the corresponding Isabelle library of definitions and theorems, most prominently those dealing with relations and quotients.

Since there are different ways of axiomatizing and developing a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We introduce the notion of a

realm

as a structure for consolidating knowledge about a mathematical theory. A realm contains several axiomatizations of a theory that are separately developed. Views interconnect these developments and establish that the axiomatizations are equivalent in the sense of being mutually interpretable. A realm also contains an external interface that is convenient for users of the library who want to apply the concepts and facts of the theory without delving into the details of how the concepts and facts were developed. We illustrate the utility of realms through a series of examples. We also give an outline of the mechanisms that are needed to create and maintain realms.

Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they have, and are in turn formalized, are the same. For the basic concepts, like natural numbers, matching them between libraries is often straightforward, because of mathematical naming conventions. However, for more advanced concepts, finding similar formalizations in different libraries is a non-trivial task even for an expert.

In this paper we investigate automatic discovery of similar concepts across libraries of proof assistants. We propose an approach for normalizing properties of concepts in formal libraries and a number of similarity measures. We evaluate the approach on HOL based proof assistants

HOL4

,

HOL Light

and

Isabelle/HOL

, discovering 398 pairs of isomorphic constants and types.

Interactive theorem provers have been used extensively to reason about various software/hardware systems and mathematical theorems. The key challenge when using an interactive prover is finding a suitable sequence of proof steps that will lead to a successful proof requires a significant amount of human intervention. This paper presents an automated technique that takes as input examples of successful proofs and infers an Extended Finite State Machine as output. This can in turn be used to generate proofs of new conjectures. Our preliminary experiments show that the inferred models are generally accurate (contain few false-positive sequences) and that representing existing proofs in such a way can be very useful when guiding new ones.

Dynamic geometry systems (DGS) have become basic tools in many areas of geometry as, for example, in education. Geometry Automated Theorem Provers (GATP) are an active area of research and are considered as being basic tools in future enhanced educational software as well as in a next generation of mechanized mathematics assistants. Recently emerged Web repositories of geometric knowledge, like TGTP and Intergeo, are an attempt to make the already vast data set of geometric knowledge widely available. Considering the large amount of geometric information already available, we face the need of a query mechanism for descriptions of geometric constructions.

In this paper we discuss two approaches for describing geometric figures (declarative and procedural), and present algorithms for querying geometric figures in declaratively and procedurally described corpora, by using a DGS or a dedicated controlled natural language for queries.

We study representation formats that allow formally defining what we call

flexary

operators: functions that take arbitrarily many arguments, like

$\sum_{k=1}^n a_k$

or binders that bind arbitrarily many variables, like ∀ 

x

1

,…

x

n

.

F

. Concretely, we define a flexary logical framework based on LF, and use it as a meta-language to define flexary first-order logic and flexary simple type theory. We use these to formalize several flexary mathematical concepts including arithmetical and logical operators, matrices, and polynomials.

The Isabelle proof assistant comes equipped with a very powerful tactic for term simplification. While tremendously useful, the results of simplifying a term do not always match the user’s expectation: sometimes, the resulting term is not in the form the user expected, or the simplifier fails to apply a rule. We describe a new, interactive tracing facility which offers insight into the hierarchical structure of the simplification with user-defined filtering, memoization and search. The new simplifier trace is integrated into the Isabelle/jEdit Prover IDE.

The Semantic Alliance (SAlly) Framework, first presented at MKM 2012, allows integration of Mathematical Knowledge Management services into typical applications and end-user workflows. From an architecture allowing invasion of spreadsheet programs, it grew into a middle-ware connecting spreadsheet, CAD, text and image processing environments with MKM services. The architecture presented in the original paper proved to be quite resilient as it is still used today with only minor changes.

This paper explores extensibility challenges we have encountered in the process of developing new services and maintaining the plugins invading end-user applications. After an analysis of the underlying problems, I present an augmented version of the SAlly architecture that addresses these issues and opens new opportunities for document type agnostic MKM services.

The libraries of deduction systems are growing constantly, so much that knowledge management concerns are becoming increasingly urgent to address. However, due to time constraints and legacy design choices, there is barely any deduction system that can keep up with the MKM state of the art. HOL Light in particular was designed as a lightweight deduction system that systematically relegates most MKM aspects to external solutions — not even the list of theorems is stored by the HOL Light kernel.

We make the first and hardest step towards knowledge management for HOL Light: We provide a representation of the HOL Light library in a standard MKM format that preserves the logical semantics and notations but is independent of the system itself. This provides an interface layer at which independent MKM applications can be developed. Moreover, we develop two such applications as examples. We employ the MMT system and its interactive web browser to view and navigate the library. And we use the MathWebSearch system to obtain a search engine for it.

Both easily readable and obscure proof scripts can be found in the bodies of formalisations around formal proof checking environments such as Mizar. The communities that use this system try to encourage writing legible texts by making available various solutions, e.g., by introduction of phrases and constructs that make formal deductions look closer to the informal ones. Still, many authors do not want to invest additional efforts in enhancing readability of their scripts and assume this can be handled automatically for them. Therefore, it is desirable to create a tool that can automatically improve legibility of proofs. It turns out that this goal is non-trivial since improving features of text that enhance legibility is in general NP-complete.

The successful application of SMT technology to solving computationally difficult problems suggests that available SMT solvers can give progress in legibility enhancement. In this paper we present the first experimental results obtained with automated legibility improving tools for the Mizar system that use Z3 solver in the backend.

We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rules and is based on a fragment of first-order logic called coherent logic. Coherent logic has been recognized by a number of researchers as a suitable logic for many everyday mathematical developments. The proposed proof representation is accompanied by a corresponding XML format and by a suite of XSL transformations for generating formal proofs for Isabelle/Isar and Coq, as well as proofs expressed in a natural language form (formatted in

or in HTML). Also, our automated theorem prover for coherent logic exports proofs in the proposed XML format. All tools are publicly available, along with a set of sample theorems.

The unique structural syntax and the variety of semantic equivalences of mathematic expressions make it a challenge for a keyword-based text search engine to effectively meet the users’ search needs. Many existing math search solutions focus on exact search where the notational matching determines the relevance rank, while the structural similarity and mathematical semantics are often missed out or not addressed adequately. One important research question is how to effectively and efficiently find math expressions that are similar to a user’s query, and how to do relevance ranking of hits by similarity. This paper focuses on (1) conceptualizing similarity between mathematical expressions, (2) defining metrics to measure math similarity, (3) utilizing those metrics for math similarity search, and (4) evaluating performance to validate advantage of the proposed math similarity search. Our results show that the performance of math-similarity search is superior to that of keyword-based math search.

The purpose of the NIST Digital Repository of Mathematical Formulae (DRMF) is to create a digital compendium of mathematical formulae for orthogonal polynomials and special functions (OPSF) and of associated mathematical data. The DRMF addresses needs of working mathematicians, physicists and engineers: providing a platform for publication and interaction with OPSF formulae on the web. Using MediaWiki extensions and other existing technology (such as software and macro collections developed for the NIST Digital Library of Mathematical Functions), the DRMF acts as an interactive web domain for OPSF formulae. Whereas Wikipedia and other web authoring tools manifest notions or descriptions as first class objects, the DRMF does that with mathematical formulae. See

http://gw32.iu.xsede.org/index.php/Main_Page

.

Interlinking knowledge is one of the cornerstones of online collaboration. While wiki systems typically rely on links supplied by authors, in the early 2000s the mathematics encyclopedia at PlanetMath.org introduced a feature that provides automatic linking for previously defined concepts. The NNexus software suite was developed to support the necessary subtasks of concept indexing, concept discovery and link-annotation. In this paper, we describe our recent reimplementation and revisioning of the NNexus system.

Marked by the highlights of native generation of

epub

E-books and

TikZ

support for creating

svg

images, we present an annual report of

development in 2013.

provides a reimplementation of the

parser, geared towards preserving macro semantics; it supports an array of output formats, notably

5,

epub

,

and its own

near

. Other highlights include enhancing performance when used inside high-throughput build-systems, via incorporating a native

zip

archive workflow, as well as a simplified installation procedure that now allows to deploy LaTeXML as a cloud service. To this end, we also introduce an official plugin-based scheme for publishing new features that go beyond the core scope of LaTeXML, such as web services or unconventional post-processors. The software suite has now migrated to GitHub and we welcome forks and patches from the wider FLOSS community.

We present the

MathHub.info

system, a development environment for active mathematical documents and an archive for flexiformal mathematics. It offers a rich interface for reading, writing, and interacting with mathematical documents and knowledge. The core of the

MathHub.info

system is an archive for flexiformal mathematical documents and libraries in the

OMDoc

/

MMT

format. Content can be authored or archived in the source format of the respective system, is versioned in GIT repositories, and transformed into

OMDoc

/

MMT

for machine-support and further into HTML5 for reading and interaction.

The goal of this project is to (i) accumulate annotated informal/formal mathematical corpora suitable for training semi-automated translation between informal and formal mathematics by statistical machine-translation methods, (ii) to develop such methods oriented at the formalization task, and in particular (iii) to combine such methods with learning-assisted automated reasoning that will serve as a strong semantic component. We describe these ideas, the initial set of corpora, and some initial experiments done over them.

We present a

to-Office conversion plugin for

ML that can bridge the divide between publication practices in the theoretical disciplines (

) and the applied ones (predominantly Office). The advantage of this plugin over other converters is that

ML conserves enough of the document- and formula structure, that the transformed structures can be edited and processed further.

We are designing and developing a web user interface for digital mathematics libraries called WebMIaS. It allows queries to be expressed by mathematicians through a faceted search interface. Users can combine standard textual autocompleted keywords with keywords in the form of mathematical formulae in

or MathML formats. Formulae are shown rendered by the web browser on-the-fly for users’ feedback. We describe WebMIaS design principles and our experiences deploying in the European Digital Mathematics Library (EuDML). We further describe the issues addressed by formulae canonicalization and by extending the MIaS indexing engine with Content MathML support.

In this paper we present an experimental extension of the

Mizar

system employing an external SAT solver to strengthen the notion of obviousness of the

Mizar

proof checker. The presented extension is based on a version of MiniSAT, called Logic2CNF. The SAT-enhanced

Mizar

checker is programmed to automatically spawn a new Logc2CNF process whenever it needs to justify any goal that involves equalities based on Boolean operations.

Recently, optics technology has emerged as a promising solution by resolving critical bottlenecks in conventional electronic systems. Its application domain spans over diverse fields ranging from laser surgeries to space telescopes. In this paper, we describe an ongoing project which aims at building a theorem proving based framework for the formal reasoning about geometrical optics, an essential theory required in the design and analysis of optical systems. Mainly, we present the motivation of our work, a road-map to achieve our goals, current status of the project and future milestones.

Erratum to: Chapter “Towards the Formal Reliability Analysis of Oil and Gas Pipelines” in: S.M. Watt et al. (Eds.): Intelligent Computer Mathematics, LNAI, DOI: 10.1007/978-3-319-08434-3_4The original version of this chapter contained an error. The name of the author Waqar Ahmad was spelled incorrectly as Waqar Ahmed in the original publication. The original chapter was corrected.