On arrival, all participants should go to Level 3 Reception at 15 South College Street to sign in.
The meeting will take place in the Cramond Room on Level 2.
Abstract: Ontology evolution involves repairing ontologies in order to resolve logical conflicts that arise from the merge of multiple, locally consistent ontologies. We design a collection of 'ontology repair plans', which are mechanisms for automating ontology evolution. In this talk, I will present our effort in implementing ontology repair plans in Isabelle -- a higher-order theorem prover. Our use of Isabelle is rather unusual as we are mostly interested in automatically creating new locales and manipulating terms within the theorem prover.
14.10-14.50: Teresa Llano (Heriot-Watt University)
Abstract: Formal methods have been successfully used for the development of safety-critical systems; however, the need for skilled knowledge when writing formal models and reasoning about them represents a major barrier in the adoption of formal methodologies for the development of non-critical applications. A key aspect in the verification of formal models and in the development of reliable systems is the identification of invariants. However, finding correct and meaningful invariants for a model represents a significant challenge. We have used automated theory formation (ATF) techniques to automatically discover invariants of Event-B models. In particular, we use Colton's HR system to explore the domain of Event-B models and suggest potential invariants.
14.50-15.20: Coffee and Tea
15.20-16.00: Robert Rothenberg (University of St Andrews)
Abstract: Gentzen-style sequent calculi have been extended in several ways so as to obtain cut-free calculi for various non-classical logics. These extensions are based on changing particular syntactic features of sequent calculi. However, these new calculi may contain structures which do not translate directly into formulae of the logics that these calculi are intended for. This makes translation between formalisms problematic. We discuss these issues, and include results from work on translating between two kinds of extension, hypersequent and labelled calculi, for intermediate logics with geometric Kripke semantics.
16.00-16.40: Chris Power (University of Glasgow)
Abstract: Symmetry reduction techniques have been successful in combating the state-space explosion problem for temporal logic model checking. Recently, there has been interest in using model checkers to verify properties of probabilistic systems. Therefore, we describe a method of applying symmetry reduction to discrete time Markov chains and Markov decision process. The method includes the automated detection of data symmetries from a probabilistic specification language and the efficient application of reduction to models that posses certain structural properties.
16.40-18.30: Drinks Reception with Light Supper.
Previous
STP seminars
For further information please
contact: Andrew Ireland (a.ireland@hw.ac.uk)