MRG home page · Research · Publications · Projects · Software · People
 
 


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.




Previous STP seminars



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
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.