Watt
2012
Program
Abstracts
Travel Information
Fotos
Watt 2012
The Watt Workshop on Symbolic Computation
Saturday 22 September 2012

Edinburgh, Scotland


Speakers


Tetsuo Ida (Japan)
Fairouz Kamareddine (UK)
Alexander Konovalov (UK)
Hans-Wolfgang Loidl (UK)
Ursula Martin (UK)
Stephen Watt (Canada)

Title and Abstract of Talks

Tetsuo Ida

Interactive vs. automated proofs in computational origami

Geometrical theorem proving is challenging in many ways. One that comes to our mind is to face directly the formalizations of basic geometrical objects together with of methods for construction and formalization of subsequent construction of the geometrical objects of study. The other is to face proving geometrical theorems formally, i.e., to follow the reasoning steps in greater details using only the given rules of deductions possibly with the help of computer assisted formal verification tools.

Sometimes, geometrical theorems are stated without degenerate considerations, or tacitly assumed. Problem of degeneracy cases may pop up in formal theorem proving. Also appealing to institution may not be allowed in the formal proofs. There have been significant developments of sophisticated tools to meet these challenges. The tools may be classified into ATP (Automated Theorem Provers) and PA (Proof Assistance (whose basic mode of communication with human provers are interactive).

There are advantages and disadvantages in both ATPs and PAs, and geometrical theorem proving do need both.

In developing origami theories, we certainly need both of them. Algebraic ATPs such as those grown from Groebner basis computations, CAD and powerful algebraic manipulations of the computer algebra systems such as Mathematica are proven to be very useful. However, certain theorems are best proved by interactive theorem provers, such as Isabelle/HOL or Coq.

In this talk I report our experiences of the uses of Mathematica-based theorem prover specifically designed for origami theories, and of the uses of Isabelle/HOL for proving certain kinds of origami theorems. We give small examples of origami theorems with demos, and show that algebraic ATP and PA are indeed helpful, and furthermore need to be integrated. We discuss future views of geometrical theorem provers in the context of origami theory developments.

This is an abridged version of the presentation which will be given at SYNASC 2012, to be held on September 25 - 29, 2012 in Timisoara.


Fairouz Kamareddine

On the Computerisation of Mathematics

The twentieth century saw the invention of computation machines and languages. Then, information engines, the world wide web and electronic search tools have changed the way we store, use and manipulate all aspects of knowledge. The 21st century will continue the search for the best computerisation tools and methods. However, we need to pose first and look at the challenges and pitfalls of the 20th century. In this talk, as a working example throughout, I concentrate on the computerisation of mathematical texts in the MathLang project. However, one can follow the same techniques to computer any other aspect of knowledge. The MathLang project aims at computerizing mathematical texts according to various degrees of formalisations, and without any prior commitment to a particular logical framework (e.g., having to choose either set theory or category theory or type theory, etc.) or to a particular proof checker (e.g., having to choose Mizar or Isabelle or Coq, etc.). Instead, MathLang keeps the choices of the logical framework and proof checker open depending on the taste and expertise of the user. Furthermore, MathLang allows useful computerizations of mathematical texts at much lower levels where the emphasis is not on full formalization as is done in the foundations of mathematics (e.g., as initiated by Frege and Russell) or on proof checking (e.g., as initiated by de Bruijn's Automath).

During computerization, first, the mathematical text is input into the computer exactly as it was written and then one or more MathLang aspects are applied to the text to provide extended versions of the text that can be checked for different levels of correctness. One basic aspect is to extend the text with categorical information (term, noun, adjective, statement, etc) and to automatically check the correctness of the text at this categorical level. This guarantees coherence of the text (e.g., variables are declared before being used and the text constitutes a well structured book). Another aspect is to divide the text into parts annotated with relations (e.g., Corollary A uses Theorem B) and to automatically derive from these relations a number of structures that represent some dependencies in the text which help explain the logical structure of the text. These dependencies are used in a further aspect where a version of the text is transformed into another which shows the holes in the proofs. Other aspects will transform this version into a fully formalized version (say in Mizar or Isabelle).

MathLang was created in 2000 by Fairouz Kamareddine and J.B. Wells as an experience driven project where the computerisation of different texts taken from various branches of mathematics, is the basis for the design and implementation of the MathLang aspects. So far, a number of mathematical texts have been computerised, some of which have been gradually transformed through MathLang aspects into full Mizar. Other proof checkers (e.g., Isabelle and Coq) are envisioned for the near future.

In this talk, the MathLang framework, its developments and its current and future aspects, as well as examples of computerization from original mathematical texts to the fully formalised Mizar versions are given. For each aspect, emphasis will be on its design, formalisation, implementation, the automation available for this aspect and the correctness or trustworthiness of these processes. Then, we discuss how the computerisation path from the original mathematical text to full Mizar will look if Isabelle was the checker chosen instead of Mizar and show that a number of aspects and computerised versions of the original text are common between both path. We also discuss at which stage a commitment to a certain logical framework and a certain proof checker can be made on the path from the original mathematical text to the version fully formalised in that proof checker.

The MathLang project started in 2000 by Fairouz Kamareddine and Joe Wells and has had since 2002 four PhD students (Manuel Maarek, Krzysztof Retel, Robert Lamar and Christoph Zengler) and a number of MSc and BSc students all collaborating and contributing to the design and implementation of the various aspects and to the computerization of mathematical texts.


Alexander Konovalov

Symbolic Computation Software Composability Protocol and Its Implementation

Symbolic Computation Software Composability Protocol (SCSCP) is a lightweight XML-based remote procedure call protocol, in which both data and instructions are represented as OpenMath objects. SCSCP was developed in the SCIEnce project (http://www.symbolic-computing.org/) as a common standard interface that may be used for combining computer algebra systems (and any other compatible software). I will demonstrate how communication via SCSCP goes, using examples which will involve GAP, Macaulay2 and Maple systems.


Hans-Wolfgang Loidl

SymGrid-Par: a System for Parallel Symbolic Computation on Large-scale Distributed Systems

The SymGrid-Par system has been designed as a high-performance symbolic computation platform, exploiting massive parallelism on Grid-style systems. It features a high-level coordination language, based on parallel Haskell, a set of domain specific skeletons for symbolic computation, and a standardised interface, SCSCP, to a range symbolic computation systems. In this talk, we will discuss the design and some performance results of this system, that has been developed as part of the EU-funded SCIEnce project.


Ursula Martin

Online/off line - mathematical culture in the age of the internet

Online blogs, question answering systems and distributed proofs provide a rich new resource for understanding what mathematicians really do, and hence devising better tools for supporting mathematical advance.

In this talk we discuss the first steps in such a research programme, looking at two examples through a sociological lens, to see what we can learn about mathematical practice, and whether the reality of mathematical practice supports the theories of researchers such as Polya and Lakatos, or the expectations of computer scientists devising software to do maths.

Polymath provides structured way for a number of people to work on a proof simultaneously: we analyse a polymath proof of a math olympiad problem to see what kinds of techniques the participants use. Mathoverflow supports asking and answering research level mathematical questions: we look at a sample of questions about algebra, and provide a typology of the kinds of questions asked, and consider the features of the discussions and answers they generate.

Finally we outline a programme of further work, and consider what our results tell us about mathematical practice, mathematical advance, and opportunities for further computational support for proof and question answering.


Stephen Watt

A Cluster of Languages for Mathematical Computing

The modern computing landscape features a galaxy of programming and data description languages, with new ones introduced continually. New ideas, introduced in one language, find their way into subsequent languages as the landscape evolves. Many important ideas first expressed in mathematical software have found their way into the most widely used general purpose languages. Perhaps one reason for this is that mathematical programming provides a rich domain of challenging, but precisely defined problems. This contrasts with the hard problems in other areas where abstractions are simpler and it is harder to evaluate different approaches. We therefore see mathematical software as a canary in the coal mine of programming languages, providing an advance testing ground for ideas.

We presents our experiences in the design and implementation of several special purpose languages applied to mathematical computing: Maple, Axiom, Aldor, OpenMath, MathML and InkML. These languages have addressed a breadth of problems, ranging from efficient compilation of higher order mathematical abstractions to flexible motion capture of two dimensional handwriting. In terms of adoption, they range from tens to millions of users with widely differing needs. This talk outlines some of the problems these languages were intended to solve, the new ideas they introduced, and the pragmatic compromises taken along the way.


Last Updated: 2012-04-21