ICMS 2016 Session: Software for Mathematical Reasoning and Applications

ICMS 2016: Home, Sessions


Aim and Scope

In addition to traditional software for numerics and symbolics (in algebra, analysis, combinatorics, etc.), more and more software for automated reasoning based on sophisticated general and special reasoning techniques with nice user interfaces enriches the possibilities of working mathematicians, computer scientists and engineers. For this session we welcome reports on


Submission Guidelines


  1. Agent-Based HOL Reasoning [pdf slides]

    Alexander Steen (Freie Universität Berlin, Institute of Computer Science),
    Max Wisniewski (Freie Universität Berlin, Institute of Computer Science),
    Christoph Benzmüller (Stanford University, CSLI/Freie Universität Berlin, Institute of Computer Science)

    Abstract: We present the automated theorem prover Leo-III and its associated system platform. In the DFG funded project a novel agent-based deduction system for classical higher-order logic (HOL) is developed which aims at exploiting massive parallelism at various levels in the reasoning process. The system allows ad-hoc inclusion of independent specialist agents that add advanced functionality to the proof search such as consistency checks of the input axiomatization using model finders or augmented deduction rules for non-classical logics. The latter, very powerful, capability is enabled by semantical embedding of the desired goal logic in HOL. Several of such embeddings will be included in Leo-III, yielding an out-of-the-box automation tool for a great number of (quantified) non-classical logics relevant in mathematics (e.g. inclusive/free logic as used in projective geometry), philosophy (e.g. modal logics) and computer science (e.g many-valued logics, paraconsistent logics).

    In its current state, Leo-III is based on an ordered paramodulation calculus for typed lambda-terms, augmented with special means of extensionality treatment. The employment of agents allows parallelism on the search level by introducing and/or splits of the search space. The scheduling of the agents' actions is realized as optimization procedure using combinatorical auction games.

  2. Automating Free Logic in HOL [pdf slides] [paper source] [further experiments]

    Christoph Benzmüller (Stanford University/Freie Universität Berlin)
    Dana Scott (Visiting Scholar, University of California, Berkeley)

    Abstract: Terms in classical logic denote, without exceptions, entities in a non-empty domain of (existing) objects D, and it are these objects of D the universal and existential quantifiers do range over. Unfortunately, however, these conditions may render classical logic unsuited for handling mathematically relevant issues such as undefinedness and partiality. For example in category theory composition of maps is not always defined.

    Free logic (and inclusive logic) has been proposed as an alternative to remedy these shortcomings. It distinguishes between a raw domain of possibly non-existing objects D and a particular subdomain E of D, containing only the "existing" entities. Free variables range over D and quantified variables only over E. Each term denotes in D but not necessarily in E. Unfortunately, as far as we know no theorem provers have been developed so far for free logic.

    In this talk we will present a semantic embedding of free logic in classical higher-order logic (HOL). This embedding enables state-of-art theorem provers and model finders for HOL, such as the first author's Leo provers, the proof assistant Isabelle/HOL and the model finder Nitpick, to reason within and about free logic in practical applications.

    To illustrate the approach we report on first experiments in which we have analysed axioms systems in category theory. In our experiments theorem provers were able to detect a (presumably unknown) redundancy in the foundational axiom system of the category theory textbook by Freyd and Scedrov.

  3. Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0

    Alexander Maletzky (RISC, JKU Linz)

    Abstract: In this talk we will report on three useful tools recently implemented in the frame of the Theorema project: a graphical user interface for interactive proof development, a higher-order rewriting mechanism, and a tool for automatically analyzing the logical dependencies of formulas and theories. Each of these three tools already proved extremely helpful in the extensive formal exploration of a non-trivial mathematical theory, namely the theory of Gröbner bases in reduction rings, in Theorema.

    Interactive proving proceeds in a dialog-oriented manner, where in each step a dialog window pops up, displaying the current proof situation (characterized by the current proof goal and list of assumptions) and containing buttons and menus for enabling the user to specify how to continue, e. g. which inference rule to apply next. The higher-order rewriting mechanism is capable of first turning Theorema formulas into rewrite-rules, and then translating these (possibly higher-order) rewrite-rules into Mathematica transformation rules that can be used for rewriting expressions efficiently. Analyzing Theorema theories, finally, works by first constructing a “dependency graph” reflecting the logical structure of the formulas part of the theory and then employing well-known functions from graph theory, e. g. to search for cycles, collect all successors of a node, and many more.

  4. An automated deduction and its implementation for solving problem of sequence at university entrance examination

    Yumi Wada (University of Tsukuba, Japan)
    Takuya Matsuzaki (Nagoya University, Japan)
    Akira Terui (University of Tsukuba, Japan)
    Noriko H. Arai (National Institute of Informatics, Japan)

    Abstract: "Todai Robot Project" is a project of artificial intelligence launched by National Institute of Informatics for re-unifying the artificial intelligence field subdivided in 1980’s and afterwards. We focus towards attaining a high score in National Center Test for University Admissions, and use Quantifier Elimination (QE) over the real closed fields as a main tool for solving problems in mathematics. However, it is not applicable for several kinds of problems such as one with sequence.

    In this talk, we propose an algorithm for solving problems of sequence at the National Center Test for University Admissions. For solving the most problems of sequence in National Center Test, we need to solve recurrence relations and algebraic equations which are given as constraints for the sequence. Although functions for solving recurrence relations and algebraic equations are available in popular computer algebra systems, it is not easy to find an answer because we need to use these functions back and forth for solving the given recurrence relations and equations in appropriate order.

    We have tackled this problem by implementing the algorithm on programing language Haskell and computer algebra system Maple, and present evaluation results for past and mock examinations, including a successful result in an open mock examination in 2015.

  5. Automated Deduction in Ring Theory

    Ranganathan Padmanabhan (Department of Mathematics, The University of Manitoba, Canada)
    Yang Zhang (Department of Mathematics, The University of Manitoba, Canada)

    Abstract: It is well-known that automated reasoning tools have been widely used in many areas such as lattice theory, loop algebra, group theory and ring theory, which provide powerful methods to check or simplify the proofs, prove or construct counter-examples for conjectures, and discover the new theorems, see, for example, McCune and Padmanabhan (Lecture Notes in Artificial Intelligence 1095, Springer), and Phillips and Stanovsky (ESARM 2008).

    Pover9/Mace4 or its predecessor Otter is one of powerful automated theorem provers for the first-order logic with equality. Since 1990's, this kind of questions attracted more and more people's attentions in automated reasoning area.

    The purpose of this paper is to explore various possibilities of using Prover9 in ring theory and semiring theory, in particular, associative rings, rings with involutions, semirings with cancellation laws and Near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, for example, Jacobson and Herstein's commutativity theorems, give some new proofs, and also discuss some new applications.

  6. Automated discovery of elementary geometry theorems: First steps

    Miguel A. Abánades (Rey Juan Carlos University, Spain)
    Francisco Botana (Vigo University, Spain)
    Zoltán Kovács (Private University College of Education of the Diocese of Linz, Austria)
    Tomas Recio (Cantabria University, Spain)
    Csilla Sólyom-Gecse (Babeş-Bolyai University, Romania)

    Abstract: Considerable attention and efforts have been given to the implementation of automated reasoning tools in interactive geometric environments. Nevertheless, the main goal in such works focused on theorem proving, cf. Java Geometry Expert or GeoGebra. A related issue, automatic discovery, remains almost unexplored in the field of dynamic geometry software.

    The talk describes our initial results towards the incorporation into GeoGebra, a worldwide spread software with tenths of millions of users, of automated discovery abilities. As a first result, currently available in the official version, we report on a new command allowing the automatic discovery of loci of points in diagrams. Besides the standard mover-tracer locus finding, the approach also deals with loci constrained by implicit conditions. Hence, our proposal successfully automates a kind of bound dragging in dynamic geometry, the 'dummy locus dragging'. In this way, the cycle of conjecturing-checking-proving will be accessible for general learners in elementary geometry.

  7. Certifying efficient polynomial implementations using the FoCaLize system

    Catherine Dubois (Ecole Nationale Superieure d’Informatique pour l’Industrie et l’Entreprise, Laboratoire SAMOVAR)
    Therese Hardin (Universite Pierre et Marie Curie)
    Francois Pessaux (ENSTA Paristech)
    Renaud Rioboo (Ecole Nationale Superieure d’Informatique pour l’Industrie et l’Entreprise, Laboratoire SAMOVAR)

    Abstract: Polynomials are of major concern in mathematical software since they form the base of any system. A computer algebra system is mainly a polynomial manipulator thus correctness and efficiency of their implementation is important for any system manipulating mathematical values. In related publications, we presented a framework for a polynomial library implementation, which was structured in an object oriented way and was both efficient and certifiable. This work started the FoCaL project which is now FoCaLize, a general framework for program certification but polynomials remain a challenging subject for program certification.
  8. Parameter space analysis for algebraic Python programs in SageMath

    Matthias Köppe (Department of Mathematics, University of California, Davis)
    Yuan Zhou (Department of Mathematics, University of California, Davis)

    Abstract: A metaprogramming trick transforms algebraic programs for testing a property for a given input parameter into programs that compute simplified semialgebraic descriptions of the input parameters for which the property holds. Our implementation of this trick is for Python programs (within the Python-based computer algebra system SageMath and using Mathematica for semialgebraic computations). We illustrate it with an application in the theory of integer linear optimization, the automatic discovery and proof of certain cutting plane theorems in integer programming.
  9. Efficient knot discrimination via quandle colouring with SAT and #-SAT

    Andrew Fish (University of Brighton)
    Alexei Lisitsa (University of Liverpool)
    David Stanovsky (Charles University, Prague)
    Sarah Swartwood (University of Brighton)

    Abstract: We apply SAT and #-SAT to problems of computational topology: knot detection and recognition. Quandle coloring can be viewed as associations of elements of algebraic structures, called quandles, to arcs of knot diagrams such that certain algebraic relations hold at each crossing. The existence of a coloring (called colorability) and the number of colorings of a knot by a quandle are knot invariants that can be used to distinguish knots. We realise coloring instances as SAT and #-SAT instances, and produce experimental data demonstrating that a SAT-based approach to colorability is a practically efficient method for knot detection and #-SAT can be utilised for knot recognition.

    We find a minimal set of 15 simple quandles (drawn from the set of all 354 simple quandles of size at most 47) that distinguish all prime knots (up to reverse and mirror image) of up to 10 crossings. We present a minimal set of 17 quandles (of size up to 182) that distinguish all prime knots (up to reverse and mirror image) of up to 12 crossings and compare the efficiency of computing all colorings with that of the set of 26 previously discovered distinguishing quandles from Clark et al (of size up to 182), both using #-SAT.