Previous CISA Seminars

Abstract:
TBC

Abstract:
TBC

Abstract:
TBC

Abstract:
Conversational Agents (CAs) have their origins in Chatbots designed to pass the Turing Test for machine intelligence. However, chatbot technology is limited to the production of convincing social chit-chat for a period of around 10 minutes. The Goal-Oriented Conversational Agent (GOCA) provides a conversational interface to conventional computer applications such as selling and end-user support. It can replace a human in a specific domain-oriented task but is not expected to be a convincing partner for social conversation. This seminar will review the original pattern matching CA technology developed by the MMU Intelligent Systems Group (in particular its drawbacks and some challenging applications for CAs) before presenting a new approach invented by the group for a new generation of CAs. This technique, Short Text Semantic Similarity (STSS) has been adopted by a number of research groups, internationally, and elements of the seminal algorithm, STASIS, appear in virtually all new work. The seminar will also cover benchmarking techniques for new STSS algorithms, our work to develop variants of STASIS for new languages (Arabic and Thai) and the extension of STSS algorithms to take account of Dialogue Acts. The final proposal is that CAs can benefit the Agents community as a whole, by allowing non-technical humans to instruct machine agents on their beliefs, desires and intentions –leading to Mandated Intelligent Agents which can represent their human clients in the wider world. Biographical notes: James O’Shea received his BSc (Hons) degree in Chemistry from Imperial College in 1976 and his PhD from Manchester Metropolitan University (MMU) in 2011. He is a senior lecturer in the School of Computing, Mathematics and Digital Technology at MMU. He spent five years in industry at International Computers (ICL) working on simulation models of Large Scale Integrated circuits and Microprogramming. He also has extensive consultancy experience under UK DTI schemes including the Microelectronics Applications Project, the Microelectronics Awareness Programme and Knowledge Transfer Partnerships. After joining MMU in 1989, he developed a research interest in AI and co-founded the Intelligent Systems Group (ISG). His current research interests include Conversational Agents and Intelligent Text Processing as well as the Adaptive Psychological Processing involved in Silent Talker technology. He is currently a member of several MMU spinout companies and is a named inventor on the patent of the Silent Talker lie detector system.

Abstract:
TBC

Abstract:
TBC

Abstract:
Thirty five years ago computers made a dramatic debut in mathematics with the famous proof of the Four Color Theorem by Appel and Haken. Their role has been expanding recently, from computational devices to tools that can tackle deduction and proofs too complex for (most) human minds, such as the Kepler conjecture or the Classification of Finite Simple Groups. These new "machine" proofs entail fundamental changes in the practice of mathematics: a shift from craftsmanship, where each argument is a tribute to the ingenuity of the mathematician that perfected it, to a form of engineering where proofs are created more systematically. In addition to formal definitions and theorems, mathematical theories also contain clever, context-sensitive notations, usage conventions, and proof methods. To mechanize advanced mathematical results it is essential to capture these more informal elements, replacing informal and flexible usage conventions with rigorous interfaces, and exercise apprenticeship with precise algorithms. This can be difficult, requiring an array of techniques closer to software engineering than formal logic, but it is essential to obtaining formal proofs of graduate-level mathematics, and can give new insight as well. In this talk we will give several examples of such empirical formal mathematics that we have encountered in the process of mechanizing a large corpus of Combinatorics and Algebra required by the proofs of the Four Colour and Odd Order Theorem. Bio: Georges Gonthier is a Principal Researcher at Microsoft Research Cambridge. Dr. Gonthier has worked on the Esterel reactive programming language, techniques for the optimal computation of functional programs, the design and formal verification of a concurrent garbage collector, the join calculus model of concurrency, concurrency analysis of the Ariane 5 flight software, using full abstraction in the analysis of security properties, and a fully computer-checked proof of the famous Four Colour Theorem. He now heads the Mathematical Components project at the MSR Inria Joint Center, following up on the latter work with the development of a comprehensive library of formalized abstract algebra.

Abstract:
Herry Herry: "Automated Planning for Configuration Changes"

In this talk, we will present a prototype implementation of a configuration system which uses automated planning techniques to compute the workflows between declarative states. The resulting workflows are executed using the popular combination of ControlTier and Puppet. This allows the prototype to be used in unattended "autonomic" situations where manual workflow specification is not feasible. It also ensures that critical operational constraints are maintained throughout the execution of the workflow. We will show how the system solves the Cloud-Burst problem i.e. migrating a web application services from private to public cloud.

Phil Scott: "What Hilbert means by Infinity"

In his "Foundations of Geometry", Hilbert develops an axiomatic foundation for Euclidean geometry and geometric interpretations of arithmetic. However, there are explicit references to "infinity" and "natural number" in his axioms and some of his theorems seem to assume the existence of a structure as rich as the natural numbers. We discuss the issues and explain how the problematic theorems can be formalised without prior commitment to the existence of the natural numbers or of the infinite.

Abstract:

Roy McCasland: "Automated Discovery in Mathematics"
A long-held goal of the Automated Mathematical Reasoning community has been to provide computer systems capable of making a significant contribution to mathematics research. True enough, there have been some notable achievements by theorem-provers, including computer-generated proofs of Robinson's Conjecture and the Four-Colour Theorem, for example. However, these successes have not proved sufficient to entice more than a relatively few mathematicians to take up the usage of such systems.
This talk will focus on recent developments in automated 'discovery' (as compared to, say, 'theorem-proving') which will hopefully lead to computer systems, in the not-too-distant future, that will be truly appreciated -- and used -- by many mathematicians.

Petros Papapanagiotou: "Formal verification of Web Services composition using Linear Logic and the pi-calculus"
We give an overview of a rigorous approach to Web Services composition based on theorem proving in the proof assistant HOL Light. In this, we exploit the proofs-as-processes paradigm to compose multiple Web Services specified in Classical Linear Logic, while using the expressive nature of our theorem-proving framework to provide a systematic and rigorous treatment of properties such as exceptions. The end result is not only a formally verified proof of the composition, with an associated guarantee of correctness, but also an `executable' pi-calculus statement describing the composition in process-algebraic terms. We illustrate our approach by analyzing a non-trivial example involving numerous Web Services in a real-estate domain.
This talk is based on a paper presented at ECOWS 2011 in September.

Abstract:
Brain perfusion imaging using Computed Tomography (CT) or Magnetic Resonance (MR) imaging has become more and more popular nowadays, it is a very powerful clinical tool for stroke diagnosis.

As time is virtually important in the case of stroke, our method using parallelization in the perfusion imaging processing can dramatically reduce analysis time (by the speedup factor of 5.56) and therefore the number of brain cells damaged will be reduced and the possibility of cure will be increased.

Besides, CT images suffer from low contrast-to-noise ratios (CNR) since there is always a tradeoff between CNR and the amount of radiation exposure to the patient. Therefore, the reduction of noise level becomes important. Our method using Gaussian process regression can significantly reduce noise, improve CNRs and therefore deliver a more accurate perfusion result.