Scottish Theorem Proving Meeting @ ICMS
|
On Friday December 14, a
Scottish Theorem Proving
meeting will take place at the
International Centre for Mathematical Sciences (ICMS) in Edinburgh - Lecture Theatre, 5th floor of the Bayes Centre (47 Potterow, EH8 9AB).
The meeting is being organized by School of Mathematical and Computer
Sciences at Heriot-Watt University.
For all organizational issues, please contact Andrew Ireland.
Programme
12.30-13.25: Lunch (Area 5.03 - Note that lunch optional, BUT booking is essential - contact Andrew Ireland BEFORE November 30 to book lunch)
13:25-13:30 Andrew Ireland – Welcome & Overview
13:30-14:00 William Kavanagh (University of Glasgow) -
Model Checking for Interesting Stochastic Turn-Based Games
Abstract: Game design is difficult enough without having to consider ensuring a game fun to play. As part of my PhD.
I am attempting to use probabilistic model checking techniques to verify defined properties of "interesting" games.
By examining a simple case study I intend to show the approach employed so far as well as outline the difficulty of the task.
We use state-of-the-art model checking software in Prism-Games to verify properties of stochastic multiplayer games and introduce novel
techniques to analyse simulated high-level play. Hopefully, I can demonstrate that this is a promising area for further research.
14:00-14:30 Kirsty Duncan (Heriot-Watt University)
- Existing landscape in verification of neural networks
Abstract: Deep neural networks have achieved impressive results in areas such as image classification and speech recognition.
Unfortunately they are unstable with respect to adversarial perturbations, minimal changes to network inputs which cause it to misclassify.
This limits the potential of deep learning in safety- and security-critical applications. In recent years, several techniques for verifying
properties of deep neural network have been proposed. This talk will give an overview of the current literature.
14:30-15:00 Juan Casanova (University of Edinburgh)-
Meta-resolution: A Least Commitment Algorithm for Enumerating Provable Instantiations of Formulas Containing Meta-variables
Abstract: Given a formula containing meta-variables, we show how to enumerate instantiations which are provable in a given theory.
Meta-resolution is an abstraction of resolution that uses least commitment principles to deal with meta-variable instantiation in the
formula to be proven, delaying instantiation and using the available information to re-duce unproductive search as much as possible.
We inductively instantiate meta-variables in maximal CNF formulas, develop sets of declarative unification constraints, and use
dependency graphs to solve these efficiently. Our study of the problem is motivated by automated detection and repair of faults in
ontologies; we found naive approaches were not efficient enough. However, our solution applies whenever there is a need to find
theorems, within a theory or ontology, that conform to given patterns.
15:00-16:00 Coffee/tea break and posters/demos (Area 5.03)
16:00-17:00 Re-Branding STP – Discussion Session
17:00 Retire to a local hostelry for Festive Drinks!