Intelligent Computer Mathematics

Table of Contents

1. Frontmatter

2. System Description: XSL-Based Translator of Mizar to LaTeX

   Grzegorz Bancerek, Adam Naumowicz, Josef Urban

   Abstract

   We describe a new version of the Mizar-to- translator. The system has been re-implemented as XSL stylesheets instead of as Pascal programs, allowing greater flexibility. It can now be used to generate both /PDF and HTML with MathJax code. We also experimentally support generation of full proofs. Finally, the system is now available online and through the Mizar Emacs interface.

3. Translating the IMPS Theory Library to MMT/OMDoc

   Jonas Betzendahl, Michael Kohlhase

   Abstract

   The IMPS system by Farmer, Guttman and Thayer was an influential automated reasoning system, pioneering mechanisations of features like theory morphisms, partial functions with subsorts, and the little theories approach to the axiomatic method. It comes with a large library of formalised mathematical knowledge covering a broad spectrum of different fields. Since IMPS is no longer under development, this library is in danger of being lost. In its present form, it is also not compatible for use with any other mathematical system.

   To remedy that, we formalise the logic of IMPS (LUTINS), and draw on both the original theory library source files as well as the internal data structures of the system to generate a representation in a modern knowledge management format. Using this approach, we translate the library to OMDoc/MMT and verify the result using type-checking in the MMT system against our implementation of LUTINS .

4. Using the Isabelle Ontology Framework

   Linking the Formal with the Informal Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, Burkhart Wolff

   Abstract

   While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a framework for developing a wide spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation.

   Up to now, Isabelle’s document preparation system lacks a mechanism for ensuring the structure of different document types (as, e.g., required in certification processes) in general and, in particular, mechanism for linking informal and formal parts of a document.

   In this paper, we present Isabelle/DOF, a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for conventional typesetting as well as formal development. We show how to model document ontologies inside Isabelle/DOF, how to use the resulting meta-information for enforcing a certain document structure, and discuss ontology-specific IDE support.

5. Automated Symbolic and Numerical Testing of DLMF Formulae Using Computer Algebra Systems

   Howard S. Cohl, André Greiner-Petter, Moritz Schubotz

   Abstract

   We have developed an automated procedure for symbolic and numerical testing of formulae extracted from the National Institute of Standards and Technology (NIST) Digital Library of Mathematical Functions (DLMF). For the NIST Digital Repository of Mathematical Formulae, we have developed conversion tools from semantic to the Computer Algebra System (CAS) MAPLE which relies on Youssef’s part-of-math tagger. We convert a test data subset of 4,078 semantic DLMF formulae extracted from the DLMF to the native CAS representation and then apply an automated scheme for symbolic and numerical testing and verification. Our framework is implemented using Java and MAPLE. We describe in detail the conversion process which is required so that the CAS is able to correctly interpret the mathematical representation of the formulae. We describe the improvement of the effectiveness of our automated scheme through incremental enhancement (making more precise) of the mathematical semantic markup for the formulae.

6. Concrete Semantics with Coq and CoqHammer

   Łukasz Czajka, Burak Ekici, Cezary Kaliszyk

   Abstract

   The “Concrete Semantics” book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant (version 8.7.2). In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness, and the readability of the proof scripts originating from a Coq re-formalization of two chapters from the book.

7. Automated Determination of Isoptics with Dynamic Geometry

   Thierry Dana-Picard, Zoltán Kovács

   Abstract

   We present two approaches to symbolically obtain isoptic curves in the dynamic geometry software GeoGebra in an automated, interactive process. Both methods are based on computing implicit locus equations, by using algebraization of the geometric setup and elimination of the intermediate variables. These methods can be considered as automatic discovery.

   Our first approach uses pure computer algebra support of GeoGebra, utilizing symbolic differentiation of the input formula. Due to computational challenges we limit here our observations to quartic curves. The second approach hides all details in computer algebra from the user, that is, the input problem can be defined by a purely geometric way, considering a conic, a circle being given by its center and radius, and a parabola by the pair focus-directrix, for instance. The results are, however, not new, the novelty being is the way we obtain them, as a handy method for a new kind of man and machine communication. Both approaches deliver an algebraic output, namely, a polynomial and its graphical representation. The output is dynamically changed when using a slider bar. In this sense, dynamic study of isoptics can be introduced in a new way.

   The internal GeoGebra computations, partly programmed by the authors, is an on-going work with various challenges in properly formulating systems of equations, in particular, to optimize computations and to avoid unnecessary extra curves in the output. Our paper highlights some of these challenges as well.

8. Biform Theories: Project Description

   Jacques Carette, William M. Farmer, Yasmine Sharoda

   Abstract

   A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for specifying and reasoning about algorithms that manipulate mathematical expressions. However, formalizing biform theories is challenging as it requires the means to express statements about the interplay of what these algorithms do and what their actions mean mathematically. This paper describes a project to develop a methodology for expressing, manipulating, managing, and generating mathematical knowledge as a network of biform theories. It is a subproject of MathScheme, a long-term project at McMaster University to produce a framework for integrating formal deduction and symbolic computation.

9. A Coq Formalization of Digital Filters

   Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire

   Abstract

   Digital filters are small iterative algorithms, used as basic bricks in signal processing (filters) and control theory (controllers). They receive as input a stream of values, and output another stream of values, computed from their internal state and from the previous inputs. These systems can be found in communication, aeronautics, automotive, robotics, etc. As the application domain may be critical, we aim at providing a formal guarantee of the good behavior of these algorithms in time-domain. In particular, we formally proved in Coq some error analysis theorems about digital filters, namely the Worst-Case Peak Gain theorem and the existence of a filter characterizing the difference between the exact filter and the implemented one. Moreover, the digital signal processing literature provides us with many equivalent algorithms, called realizations. We formally defined and proved the equivalence of several realizations (Direct Forms and State-Space).

10. MathTools: An Open API for Convenient MathML Handling

    André Greiner-Petter, Moritz Schubotz, Howard S. Cohl, Bela Gipp

    Abstract

    Mathematical formulae carry complex and essential semantic information in a variety of formats. Accessing this information with different systems requires a standardized machine-readable format that is capable of encoding presentational and semantic information. Even though MathML is an official recommendation by W3C and an ISO standard for representing mathematical expressions, we could identify only very few systems which use the full descriptiveness of MathML. MathML’s high complexity results in a steep learning curve for novice users. We hypothesize that this complexity is the reason why many community-driven projects refrain from using MathML, and instead develop problem-specific data formats for their purposes. We provide a user-friendly, open-source application programming interface for controlling MathML data. Our API allows one to create, manipulate, and efficiently access commonly needed information in presentation and content MathML. Our interface also provides tools for calculating differences and similarities between MathML expressions. The API also allows one to determine the distance between expressions using different similarity measures. In addition, we provide adapters for numerous conversion tools and the canonicalization project. Our toolkit facilitates processing of mathematics for digital libraries without the need to obtain XML expertise.

11. Aligator.jl – A Julia Package for Loop Invariant Generation

    Andreas Humenberger, Maximilian Jaroschek, Laura Kovács

    Abstract

    We describe the Aligator.jl software package for automatically generating all polynomial invariants of the rich class of extended P-solvable loops with nested conditionals. Aligator.jl is written in the programming language Julia and is open-source. Aligator.jl transforms program loops into a system of algebraic recurrences and implements techniques from symbolic computation to solve recurrences, derive closed form solutions of loop variables and infer the ideal of polynomial invariants by variable elimination based on Gröbner basis computation.

12. Enhancing ENIGMA Given Clause Guidance

    Jan Jakubův, Josef Urban

    Abstract

    ENIGMA is an efficient implementation of learning-based guidance for given clause selection in saturation-based automated theorem provers. In this work, we describe several additions to this method. This includes better clause features, adding conjecture features as the proof state characterization, better data pre-processing, and repeated model learning. The enhanced ENIGMA is evaluated on the MPTP2078 dataset, showing significant improvements.

13. Formalized Mathematical Content in Lecture Notes on Modelling and Analysis

    Michael Junk, Stefan Hölle, Sebastian Sahli

    Abstract

    We introduce an approach to include formalized mathematics in regular undergraduate mathematics courses. In order to enable automatic parsing and checking, the code of our lecture notes systematically uses strict syntax conventions for all definitions and theorems, including in particular an unambiguous grammar for all formulas. Resulting from several years of experience, we present a body of about 1000 pages of notes for a course on modelling and a sequence of three courses on analysis and calculus which are a regular part in the undergraduate mathematics curriculum at the University of Constance. We explain the basic structure of the formalization and its syntax and discuss the practicability of the approach.

14. Isabelle Import Infrastructure for the Mizar Mathematical Library

    Cezary Kaliszyk, Karol Pąk

    Abstract

    We present an infrastructure that allows importing an initial part of the Mizar Mathematical Library into the Isabelle/Mizar object logic. For this, we first combine the syntactic information provided by the Mizar parser with the syntactic one originating from the Mizar verifier. The proof outlines are then imported by an Isabelle package, that translates particular Mizar directives to appropriate Isabelle meta-logic constructions. This includes processing of definitions, notations, typing information, and the actual theorem statements, so far without proofs. To show that the imported 100 articles give rise to a usable Isabelle environment, we use the environment to formalize proofs in the Isabelle/Mizar environment using the imported types and their properties.

15. Discourse Phenomena in Mathematical Documents

    Andrea Kohlhase, Michael Kohlhase, Taweechai Ouypornkochagorn

    Abstract

    Much of the wealth of industrialized societies is based on knowledge that is laid down and communicated in scientific/technical/engineering/mathematical documents: highly structured documents that contain diagrams, images, and – most daunting to many readers – mathematical formulae. It seems clear that digital, interactive documents have the potential to improve reading these kind of documents, and thus learning and applying this kind of knowledge.

    To understand how such improvements could be designed, we explore how formula understanding interacts with the surrounding text in mathematical documents. We report on an eye-tracking experiment with 23 engineering students reading a “solved problem” based on a simple differential equation. We observe for instance that – triggered by formulae – readers backjump to previously identified semantic loci and that this behavior is independent of depth of understanding in mathematically trained readers. Based on our observations, we propose novel in-document interactions that could potentially enhance reading efficiency.

16. Finding and Proving New Geometry Theorems in Regular Polygons with Dynamic Geometry and Automated Reasoning Tools

    Zoltán Kovács

    Abstract

    In 1993 Watkins and Zeitlin published a method [1] to simply compute the minimal polynomial of \(\cos (2\pi /n)\), based on the Chebyshev polynomials of the first kind. For the work presented in this paper we have implemented a small augmentation, based on Watkins an Zeitlin’s work, to the dynamic mathematics tool GeoGebra. We show that this improves GeoGebra’s capability to discover and automatically prove various non-trivial properties of regular n-gons.

    Discovering and proving, in this context, means that the user can sketch a conjecture by drawing the geometric figure with the tools provided by GeoGebra. Then, even if the construction is just approximate, in the background a rigorous proof is computed, ensuring that the conjecture can be confirmed, or must be rejected.

    In this paper the potential interest of automated reasoning tools will be illustrated, by describing such new results in detail, obtained by some recently implemented features in GeoGebra.

    Besides confirming well known results, many interesting new theorems can be found, including statements on a regular 11-gon that are impossible to represent with classical means, for example, with a compass and a straightedge, or with origami.

17. Gröbner Bases of Modules and Faugère’s Algorithm in Isabelle/HOL

    Alexander Maletzky, Fabian Immler

    Abstract

    We present an elegant, generic and extensive formalization of Gröbner bases, an important mathematical theory in the field of computer algebra, in Isabelle/HOL. The formalization covers all of the essentials of the theory (polynomial reduction, S-polynomials, Buchberger’s algorithm, Buchberger’s criteria for avoiding useless pairs), but also includes more advanced features like reduced Gröbner bases. Particular highlights are the first-time formalization of Faugère’s matrix-based \(F_4\) algorithm and the fact that the entire theory is formulated for modules and submodules rather than rings and ideals. All formalized algorithms can be translated into executable code operating on concrete data structures, enabling the certified computation of (reduced) Gröbner bases and syzygy modules.

18. MathChat: Computational Mathematics via a Social Machine

    Manfred Minimair

    Abstract

    The main question of this research is: How does a social machine discover algorithmic mathematical knowledge? A social machine is a system of humans and computers engaged in some purposeful activity. To address the main question, an empiric and theoretical framework for algorithmic mathematical knowledge discovered by the social machine is proposed. The framework is derived from findings in Distributed Cognition documenting how collaborators evolve a mathematical algorithm. By combining Distributed Cognition with the standard Message Passing Model of Distributed Computing, a formalism is introduced to specify the activities of the social machine and its algorithmic knowledge. Furthermore, the software system MathChat is introduced which provides an online environment for social machines engaged in mathematical computations. An application of MathChat in network analysis education is described which outlines a social machine covered by the proposed framework.

19. Automatically Finding Theory Morphisms for Knowledge Management

    Dennis Müller, Michael Kohlhase, Florian Rabe

    Abstract

    We present a method for finding morphisms between formal theories, both within as well as across libraries based on different logical foundations. As they induce new theorems in the target theory for any of the source theory, theory morphisms are high-value elements of a modular formal library. Usually, theory morphisms are manually encoded, but this practice requires authors who are familiar with source and target theories at the same time, which limits the scalability of the manual approach.

    To remedy this problem, we have developed a morphism finder algorithm that automates theory morphism discovery. In this paper we present an implementation in the MMT system and show specific use cases. We focus on an application of theory discovery, where a user can check whether a (part of a) formal theory already exists in some library, potentially avoiding duplication of work or suggesting an opportunity for refactoring.

20. Goal-Oriented Conjecturing for Isabelle/HOL

    Yutaka Nagashima, Julian Parsert

    Abstract

    We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to identify and prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isabelle’s strong automation to identify and prove such conjectures.

21. Knowledge Amalgamation for Computational Science and Engineering

    Theresa Pollinger, Michael Kohlhase, Harald Köstler

    Abstract

    This paper addresses a knowledge gap that is commonly encountered in computational science and engineering: To set up a simulation, we need to combine domain knowledge (usually in terms of physical principles), model knowledge (e.g. about suitable partial differential equations) with simulation (i.e. numerics/computing) knowledge. In current practice, this is resolved by intense collaboration between experts, which incurs non-trivial translation and communication overheads. We propose an alternate solution, based on mathematical knowledge management (MKM) techniques, specifically theory graphs and active documents: Given a theory graph representation of the domain, model, and background mathematics, we can derive a targeted knowledge acquisition dialogue that supports the formalization of domain knowledge, combines it with simulation knowledge and – in the end – drives a simulation run – a process we call MoSIS (“Models-to-Simulations Interface System”). We present the MoSIS prototype that implements this process based on a custom Jupyter kernel for the user interface and the theory-graph-based Mmt knowledge management system as an MKM backend.

22. Validating Mathematical Theorems and Algorithms with RISCAL

    Wolfgang Schreiner

    Abstract

    RISCAL is a language for describing mathematical algorithms and formally specifying their behavior with respect to user-defined theories in first-order logic. This language is based on a type system that constrains the size of all types by formal parameters; thus a RISCAL specification denotes an infinite class of models of which every instance has finite size. This allows the RISCAL software to fully automatically check in small instances the validity of theorems and the correctness of algorithms. Our goal is to quickly detect errors respectively inadequacies in the formalization by falsification in small model instances before attempting actual correctness proofs for the whole model class.

23. First Experiments with Neural Translation of Informal to Formal Mathematics

    Qingxiang Wang, Cezary Kaliszyk, Josef Urban

    Abstract

    We report on our experiments to train deep neural networks that automatically translate informalized -written Mizar texts into the formal Mizar language. To the best of our knowledge, this is the first time when neural networks have been adopted in the formalization of mathematics. Using Luong et al.’s neural machine translation model (NMT), we tested our aligned informal-formal corpora against various hyperparameters and evaluated their results. Our experiments show that our best performing model configurations are able to generate correct Mizar statements on 65.73% of the inference data, with the union of all models covering 79.17%. These results indicate that formalization through artificial neural network is a promising approach for automated formalization of mathematics. We present several case studies to illustrate our results.

24. Deep Learning for Math Knowledge Processing

    Abdou Youssef, Bruce R. Miller

    Abstract

    The vast and fast-growing STEM literature makes it imperative to develop systems for automated math-semantics extraction from technical content, and for semantically-enabled processing of such content. Grammar-based techniques alone are inadequate for the task. We present a new project for using deep learning (DL) for that purpose. It will explore a number of DL and representation-learning models, which have shown superior performance in applications that involve sequences of data. As math and science involve sequences of text, symbols and equations, such as deep learning models are expected to deliver good performance in math-semantics extraction and processing.

    The project has several goals: (1) to apply different DL models to math-semantics extraction and processing, designing more suitable models as needed, for such foundational tasks as accurate tagging and automated translation from to semantically-resolved machine understandable forms such as cMathML; (2) to create and make available to the public labeled math-content datasets for model training and testing, and Word2Vec/Math2Vec representations derived from large math datasets; and (3) to conduct extensive comparative performance evaluations gaining insights into which DL models, data representations, and traditional machine learning models, are best for the above-stated goals.

25. Backmatter