ICMS 2018 Session: Software for Mathematical Reasoning and Applications

ICMS 2018: Home, Sessions

Organizers

Aim & 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

Important Dates

Short abstract submission:
April 14, 2018 (extended)
Extended abstract submission:
April 21, 2018
Organizers decision:
April 30, 2018

Submission & Publication

Level 1:
Submit a short abstract at latest by April 14, 2018.
Level 2:
Submit an extended abstract at latest by April 21, 2018.
Level 3:
A special issue in some journal (e.g. the Journal of Symbolic Computation) might be organized after the conference depending on the number and the quality of Level 2 submissions.

Accepted Talks

  1. Automated reasoning in (semi-) groups with power-maps

    R. Padmanabhan (Dept. of Mathematics, University of Manitoba, Canada)
    Y. Zhang (Dept. of Mathematics, University of Manitoba, Canada)

    Abstract: In groups, semigroups, and cancellative semigroups, various theorems for commutativity have been explored. For example, n-abelian groups by Baer, Alperin, Kaluzhnin and others; some power-map based theorems by B.H. Neumann. Most of these results were proved by using some pure algebraic techniques. The methods are often unique and it is difficult to apply for other similar questions.

    Recently, we have developed a new concept of "power-like function" generalizing the standard notion of power-maps in a group or a semigroup. This idea can be applied for a large of class of commutativity theorems. Our proof belongs to first-order logic and uses a first-order theorem-prover "Prover9". Normally, first-order theorem provers cannot handle sentences involving arbitrary integer variables, This is the first time that Prover9 has been augmented by power-like functions to enable the software to prove new theorems in this area.

    In this paper, using Prover9 and power-like functions, we prove and extend a well-known theorem by Neumann (2001). In these automated proofs, the integer variable never explicitly appears and hence the lengths of the proofs as well as the lengths of the longest clause in these proofs remain the same irrespective of the value of n. It is also possible to use similar automated proofs in equational theory of rings.

  2. A Topos Model for Syntax

    L. Schoenbaum (University of South Alabama, USA)

    Abstract: We describe a Grothendieck topos that may be viewed as the object architecture of a software application, or as a general model of computation. The base category is a system of syntax trees, which is made into a site by adding a Grothendieck topology in which syntax trees are covered by valid chains of inference that end at the tree. Arrows between syntax trees (and syntax forests, in our approach) correspond to sound rewrite rules, which we present in a uniform, computer-implementable format, as certain forms having a well-defined boundary. Certain sheaves of the topos generated by the site correspond to formal systems. An extension of one formal system to another, or the discharge of an assumption, defines a sheaf morphism. The verification of a theorem corresponds topos-theoretically to the amalgamation of a section. The topos-theoretic structure is therefore simple, but important, as it permits an easy-to-use implementation and offers semantics for a natural-deduction style of reasoning. In practice all machine-based computation would occur in the finite part of the topos's structure. We describe the finite part of the topos precisely, including all details, using a set theoretic formalism. We then develop a rule system, called the SETTL (set-theoretic logic) system, to serve as a foundation for mathematical reasoning and computation. The SETTL system is convenient for having a reduced, RISC-like set of basic connectives and axioms. Using it, we develop an intuitionistic formalism (that can of course easily be made classical), including quantifiers, classes, and functions (up to first order, or to some higher order). We develop a form of Peano arithmetic, and provide a small handful of examples applying the system in two contrasting ways: to mathematical proofs, and to algorithms from computer science. The topos provides supporting semantics for a computer application whose implementation details are outlined. The computer application includes both sound and unsound rules, and the latter are called creative. We describe a set of these which is complete, in the sense that it provides at least one (possibly unsound) transformation between every syntax tree. This lays the foundations of an application user interface. We discuss this layer of the software, particularly in connection with a distinction between representation and syntax that is important to the application's architecture. Intended uses are for mathematics education, verification, for research/investigation, or in the pure study of the underlying system and its mechanics, or other logical frameworks.

  3. Inferring Safe Maude Programs with ATAME

    Maria Alpuente (DSIC, Technical University of Valencia, Spain)
    Demis Ballis (DMIF, University of Udine, Italy)
    Julia Sapina (DSIC, Technical University of Valencia, Spain)

    Abstract: We present ATAME, an assertion-based program specialization tool for the multi-paradigm language Maude. The program specializer ATAME takes as input a set A of system assertions that model the expected program behavior plus a Maude program R to be specialized that might violate some of the assertions in A. The outcome of the tool is a safe program refinement R' of R in which every computation is a good run, i.e., it satisfies the assertions in A. The specialization technique encoded in ATAME is fully automatic and ensures that no good run of R is removed from R', while the number of bad runs is reduced to zero. We demonstrate the tool capabilities by specializing an overly general nondeterministic dam controller to fulfill a safety policy given by a set of system assertions.

  4. Finding a Middle Ground for Computer-Aided Cryptography

    Bryan Williams (SPAWAR Systems Center Atlantic, USA)
    Evan Austin (SPAWAR Systems Center Atlantic, USA)
    Scott Batson (SPAWAR Systems Center Atlantic, USA)
    Peter Curry (SPAWAR Systems Center Atlantic, USA)


    Abstract: Motivated by the ever increasing difficulty of proofs of security and correctness, cryp- tographers have drawn inspiration from the more general software and hardware verification communities and integrated a number of formal methods tools and techniques into their work- flows. Even though this practice of computer-aided cryptography is still comparatively young, it has spawned a number of automated cryptographic analysis tools. These tools may typi- cally be categorized in one of two ways: tools focused on theoretical, or ”provable”, aspects of security; and tools focused on verifying more practical implementation details. In 2014, Barthe et. al. introduced EasyCrypt, a tool that claims to support game-based verification of security for cryptographic constructions in a generic group model. We have developed novel libraries in EasyCrypt to support functionality over elliptic curve cryptographic schemes for the purpose of verifying tool support in the generic group model setting. This paper discusses our motivation for, and early work towards, ending an approachable middle ground of the current cryptographic tool spectrum. In addition, we present the automated verification of CPA security for an elliptic curve ElGamal variant in EasyCrypt, and discuss how one may adapt these ideas to additional elliptic curve schemes.

  5. Towards a Unified Ordering for Superposition Calculus Automated Theorem Proving

    Jan Jakubův (Czech Technical University in Prague, Czech Republic)
    Cezary Kaliszyk (University of Innsbruck, Austria)


    Abstract: In this paper we propose an extension of the automated theorem prover E by the weighted path ordering. Weighted path ordering is theoretically stronger than all the orderings used in E-prover, however its parametrization is more involved than those normally used in automated reasoning. In particular, it depends on a term algebra. We discuss how the parameters for the ordering can be proposed automatically for particular theorem proving problem strategies. We integrate the ordering in E-prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the ones used in E prover so far.