Scottish Theorem Proving

There will be a meeting of STP in St Andrews on Friday June 12th 2009, in the School of Computer Science, North Haugh, St Andrews, from 1.00 to 5.00 pm.

The meeting is in room 1.33a of the Jack Cole Building. It is building 16 on the map in How to get to the School of Computer Science; or maybe you need How to get to St Andrews first.

Lunch arrangements are yet to be finalised. Please let us know by Saturday 6 June if you want a sandwich lunch beforehand. Dietary restrictions should be divulged.

The meeting will finish by 5pm to allow (a) people to catch the 1729 train from Leuchars back to the real world and (b) (for others) an adequate period for team-building exercises in a local hostelry (Drouthy Neebors).

RD and EK

Programme:

• 1.30 pm Lilia Giorgieva, Heriot-Watt University (Edinburgh)
  
  Verification of agent's communication

We study standard formal models for knowledge management. We propose a multi-agent knowledge management framework. The framework relies on identification of processes which support knowledge management. We express knowledge exchange in epistemic logic. We then translate multi-agent dialogues into a protocol language which is verifiable by model checking.

• 2.00 pm James McKinna, Radboud University of Nijmegen
  (replaces talk by Sripriya G)
  
  Programming with Computational Induction (joint work with Dan Synek and Eelis van der Weegen)
  
  We consider the problem of representing and verifying non-structurally recursive algorithms in the type theory CIC of the Coq proof assistant. We illustrate our ideas in the context of a reachability algorithm on (finite) graphs. Our approach makes use of Sozeau's Program machinery, a relatively recent addition to Coq, which permits a very clean representation of functional programs in CIC. In this talk I will discuss a representation, where the use of Program is confined to proving total correctness, while partial correctness is handled via the graph of the function. This work fulfils some of the promises sketched some years ago in another St Andrews seminar in this series.
  
  
• 2.30 pm Moa Johansson, University of Edinburgh
  
  Conjecture Synthesis for Inductive Theories
  
  Interactive theorem provers, such as Isabelle, often come with large theory libraries of previously proved theorems and lemmas. Automating the formation of these theory libraries is an important challenge. We have developed a program for inductive theory formation, called IsaCoSy, which synthesise conjectures bottom-up from available constants and variables. The synthesis process is made tractable by only generating irreducible terms. Synthesised conjectures are filtered through counter-example checking, and then passed to the automated inductive prover in IsaPlanner. As theorems are discovered, more restrictions on the synthesis process can be generated. IsaCoSy is one of very few theory formation systems that has been applied to inductive theories. We have sucessfully used IsaCoSy to synthesise theories about natural numbers, lists and binary trees. The results were compared to Isabelle's libraries with high recall if lower precision.
  
  
• 3.00 pm Ekaterina Komendantskaya, University of St Andrews
  
  Neurons OR Symbols: Why Does OR Remain Exclusive?
  
  The joint efforts of researchers in many areas have given many insights on how logic and neuroscience can relate: Boolean (binary) networks can compute logical connectives; binary threshold networks can simulate Finite Automata, and (universal) Turing machines can be simulated by neural networks with rational weights. Neural networks in their full potential are as powerful as analog computing. The natural question that arises is how neural networks can cope with logical theories and calculi. The existing Neuro-Symbolic systems have originated from Cognitive Science and Artificial Intelligence, and usually interpret semantics (or model-theoretic aspect) of first-order logic programs using boolean or fuzzy neural networks. Thus, as for today, only truth values are processed by neuro-symbolic networks, while the syntax, the proper "symbolic" part of computations, remains opaque. As a result, the central algorithms and notions of proof theory and automated reasoning (term-rewriting, unification, goal-oriented refutation, higher-order logics and typed languages), have not received any significant implementation in Neural Networks. In this talk, we analyse the reasons for the long-lasting gap between Neurocomputing and Computational Logic, between "Neurons" and "Symbols". We outline five main properties that a successful Neuro-Symbolic System of the future will need to possess in order to achieve a successful integration with the state of the art techniques of automated reasoning.
  
  
• 3.30 pm Tea and coffee
  
  
• 4.00 pm Shamim Ripon, University of Glasgow
  
  A Semantic Embedding of Promela-Lite in PVS
  
  Promela-Lite is a small specification language which captures the core features of Promela. It is defined to prove the correctness of the automatic symmetry detection techniques for Promela. The grammar and semantics of the language have been defined. Properties of the language are proved by hand. In this talk, we present our approach to embed Promela-Lite syntax and semantics into the general purpose theorem prover PVS and use these embeddings to interactively prove both consistency with the syntax/semantics definitions and language properties.
  
  
• 4.30 pm Christoph Hermann, University of St Andrews
  
  Verification of Resource Usage of Hume Programs in Agda
  
  Agda as a language with dependent types can be used for prototyping small embedded programs for verification purposes. Dependent types specify program properties which are to be verified in the design phase. Of particular interest for us are non-functional properties of programs written in Hume, a language for embedded, safety-critical systems. Such properties are e.g. memory requirements, worst-case execution time or power consumption, since for embedded systems these are of equal importance as functional correctness. For pure functional expressions in Hume there is already an automatic analysis available. The verification in Agda deals with the coordination level of Hume, in which components interact in an asynchronous fashion and program execution can involve repetitive execution of components. The aim is to combine the automatic analysis at the Hume expression level and the knowledge about time and energy requirements of peripheral devices with the designer's knowledge about the algorithmic behaviour at the coordination level. Agda is also a proof assistant and provides support for equational reasoning to justify properties specified in the types. To a small extent Agda is also able to carry out automatic reasoning for equality and ordering of values expressed in terms of arithmetic expressions.
  

Organised by R. Dyckhoff and Ekaterina Komendantskaya