Scottish Theorem Proving Seminar

Date/Time

23rd November 2016

12.30 pm: lunch provided by SICSA

2.00 - 5.00 pm: talks

Location

**Lunch:** Chapterhouse

**Talks:** Newhaven lecture theatre

International Centre for Mathematical Sciences (ICMS)

15 South College Street

Edinburgh EH8 9AA

Registration

Programme

12.30 - 1.45 pm Lunch

1.45 - 2.00 pm
Recent developments in SICSA

Katya Komendantskaya and Neil Ghani

* SICSA Theme Leaders for Theory, Modelling and Computation*

2.00 - 2.40 pm
Machine Learning Problems in Interactive Theorem Proving

Cezary Kaliszyk

* University of Innsbruck *

2.40 - 3.20 pm
Functional Inferences over Heterogeneous Data

Kwabena Nuamah

* University of Edinburgh*

3.20 - 3.40 pm Coffee Break

3.40 - 4.20 pm
Decision diagrams for graph search problems

Craig Reilly

* University of Glasgow *

4.20 - 5.00 pm
Representations of mathematical dialogue

Joe Corneli

* Goldsmiths University of London *

5.00 - 5.15 pm
Business meeting

Gudmund Grov

* Heriot-Watt University *

5.15 pm Close

Adjourn to a local hostelry

Abstract

Machine Learning Problems in Interactive Theorem Proving

Cezary Kaliszyk

As formalization is becoming a more accepted means of establishing correctness of computer programs and mathematical theories, the
usability of proof assistants and the automation level which they provide becomes more important. In this talk I will discuss various proof assistant tasks that give rise to machine learning problems. First, I will present heuristic lemma filtering, whose task is to predict the premises available in the large libraries which are useful for a user given conjecture. Next, we will look at the choice of the optimal strategies for automation. We will continue with internal guidance, the prediction of the actual inference rules to apply at a given proof step. Finally we will look at conjecture and intermediate lemma generation.

Functional Inferences over Heterogeneous Data

Kwabena Nuamah

The increasing availability of knowledge bases (KBs) on the web has opened up the possibility of improved inference in automated query answering (QyA) systems. We have developed a rich inference framework (RIF) that responds to queries where no suitable answer is readily contained in any available data source, by applying functional inferences over heterogeneous data from the web. Our technique combines heuristics, logic and statistical methods to infer novel answers to queries. It also determines what facts are needed for inference, searches for them, and then integrates these diverse facts and their formalisms into a local query-specific inference tree. We explain the internal representation of RIF, the grammar and inference methods for expressing queries and the algorithm for inference. We also show how RIF estimates confidence in its answers, given the various forms of uncertainty faced by the framework.

Decision diagrams for graph search problems

Craig Reilly

Many combinatorial problems can be expressed in terms of graph search or enumeration problems, where the goal is to find a graph (or class of graphs) which satisfies certain constraints. Such problems can be modelled using standard optimisation technologies such as SAT, Integer Programming and Constraint Programming. The size of the search space for many graph search problems is prohibitively large, so it is common for symmetry breaking techniques to be used to minimise the number of isomorphic assignments made during search. One such technique is to search for a canonical copy of each isomorphic graph found during search. However, searching over non-isomorphic graphs is often still prohibitive, so we extend an approach which uses decision diagrams as an optimisation technology to graph search problems, avoiding exhaustive search. These decision diagrams are built from dynamic programming models of graph search problems, which are easily understood and assume no knowledge of optimisation technologies on the part of the programmer. When the problem is prohibitively difficult, our approach provides bounds on the objective (for example, if we are searching for an extremal graph this will correspond to bounds on the number of edges present in a solution).

Representations of mathematical dialogue

Joe Corneli

The first half of the talk will provide a high-level overview of
"Lakatos-style Collaborative Mathematics through Dialectical, Structured
and Abstract Argumentation", a paper (currently under review) that was
written with members of the Centre for Argumentation Technology at the
University of Dundee. This work aims to represent the informal aspects
of proof in a formal way; in other words, to expose high-level
structures of reasoning to computational analysis. The second half of
the talk will consider an extension of this work that digs deeper into
the mathematical content of collaboratively-created proofs.

This seminar was organised by Alan Bundy and
Francisco José Quesada Real.

For further information please contact: A.Bundy@ed.ac.uk

Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB,
Scotland

Tel: +44 (0)131 650 2733 Fax: +44 (0)131 650 6899

Tel: +44 (0)131 650 2733 Fax: +44 (0)131 650 6899

Please send corrections and suggestions for this page to the
DReaM Support Team

Unless explicitly stated otherwise all material on this web site is
copyright © The University of Edinburgh.