These lectures will take place in Lower College Hall, North Street. The lectures will discuss the close relationship between how knowledge and problems may be represented and how people and computers use these representations to guide their reasoning about the problems.

10.00 1. Title: The Interaction of Representation and Reasoning

Abstract: Successful reasoning is dependent on appropriate representation of both knowledge and of successful methods of reasoning. A change of representation can change an intractable problem into an easy one. Failures of reasoning can suggest changes of representation. Reasoning failures can, for instance, take the form of proofs of false conjectures, failures to prove true conjectures or inefficient inference. I will illustrate these interactions by drawing on work in my research group.

11.30 2. Title: Theory Evolution in Physics

Abstract: We investigate the problem of automatically repairing a faulty Physics theory when it conflicts with experimental evidence. We introduce novel strategies for fault diagnosis and for representation repair. Diagnosis and repair are composed into general-purpose repair plans. We will illustrate this with two such plans, where theory and experiment conflict over (a) the value and (b) the dependence of a function, respectively. We represent both physical concepts and the repair plans using higher-order logic. This is because many physical concepts are most naturally represented as higher-order functions and because polymorphic higher-order functions are required to enable the repair plans to be applied to diverse situations.

14.00 3. Title: Reformation: A Domain-Independent Algorithm for Theory Repair

Abstract: We describe and invite discussion on work in progress on reformation, a new algorithm for the automated repair of faulty logical theories. A fault is revealed by a reasoning failure: either the proof of a false theorem or the failure to prove a true conjecture. Repair suggestions are systematically extracted via analysis of the attempted unification of two formulae. These suggestions will either block an unwanted but successful unification or unblock a wanted but failed unification attempt. In contrast to traditional belief revision and abduction mechanisms, the repairs are to the language of the theory as well as to the deletion or addition of axioms.

Professor Alan Bundy

Professor Alan Bundy is Professor of Automated Reasoning in the School of Informatics at the University of Edinburgh. Professor Bundy is a world-leader in the area of artificial intelligence called Mathematical Reasoning and has held more than 50 research grants in this area since the 1970s , has published more than 200 research papers and has been awarded the 2007 IJCAI Award for Research Excellence and Herbrand Award for Distinguished Contributions to Automated Deduction. He is a Fellow of the Royal Society, A Fellow of the Royal Society of Edinburgh, a Fellow of the Royal Academy of Engineers and, in 2012, was awarded a CBE for services to computing science. As well as his research work, Professor Bundy has played an active role in the British Computer Society and has been instrumental in supporting changes to the computer science curriculum in schools.

Slides:

• Lecture 1
• Lecture 2
• Lecture 3

Title
Formal Modelling and Analysis of Deployed Systems

Abstract
Formal methods are traditionally used for specification and implementation in a waterfall model. In contrast, I am interested in formal models of concurrent, interactive systems that may/may not be in software, and   may already be deployed, i.e. they are systems to be observed.  Can formal models and reasoning expose how a system actually works?  Can formal models and reasoning suggest improvements based on how a system is actually used?

In these talks I will investigate these questions through case studies, from biochemical signalling pathways, to wireless home networks and (shock horror) mobile app games.

Biography
I have been at the Department of Computing Science, University of Glasgow since January 1988. Until 2012 I was Dean of Research in the College of Science and Engineering and Senate Assessor on Court and before that I was Head of Department of Computing Science for four years, from 2003 to 2007. I currently work for the Scottish Government 60% of the time, as the Chief Scientific Adviser. Continue reading