Scottish Theorem Proving Seminar

About STP

Theorem proving research is notably strong in Scottish universities, with active groups and researchers in at least six departments. The Scottish Theorem Proving Seminar Series provide a common venue for communication and sharing of ideas by all these researchers. At least once a year, one of the departments hosts an informal seminar for the whole Scottish theorem proving community. As well as theorem proving, other related fields are also represented, e.g. model checking and other forms of formal reasoning, verification and synthesis. This is a friendly venue for PhD students and RAs to discuss their work in progress and get feedback.

Over the last few years there were many discussions about changing the title and broadening the scope of the seminar to explicitly address other forms of formal reasoning, verification and synthesis, thus the seminar is to be rebranded and the new name announced on 12 December 2019.

Invited speaker:

• Prof Radu Mardare (Department of Computer & Information Sciences, University of Strathclyde): Quantitative formal reasoning

Call for contributions:
We invite contributions on automatic reasoning, theorem proving, model checking, verification and synthesis. Speakers are invited to present research results in any of the themes of interest for the seminar as well as application experiences, tools, and promising preliminary ideas. We are planning this event as a friendly venue for PhD students and RAs to discuss their work in progress and get feedback.
If you would like to give a talk, please send your proposed title and abstract (up to 500 words) by email to Rob Stewart via email by (UPDATED!) 5 December 2019.

Attending:
Attending the seminar, the lunch and the coffee break are free (thanks to our sponsors!). In order to help with catering arrangements, please register at our Eventbrite page.

Abstracts

• Radu Mardare, Department of Computer & Information Sciences, University of Strathclyde
  Quantitative formal reasoning For more than 2000 years mathematics is done axiomatically: we establish a set of axioms and using a logical apparatus, we prove theorems. And always we axiomatize an equivalence (congruence) relation among the mathematical objects. The recent focus of theoretical computer science on probabilistic and stochastic systems, requested by the developments in machine learning, robotics or cyber physical systems, puts us a new challenge. We need more than understanding if two systems/automata/algorithms are (behaviourally) equivalent or not; we need to understand when systems that are not equivalent have “sufficiently” similar behaviours, or when can we claim that a system is a “sufficiently good” approximation of another system. If we want to approach this problem axiomatically, one needs to axiomatize not a congruence, but rather a (pseudo-) metric – and this is a novel challenge in mathematics. This work summarizes a series of results I obtained, in collaboration with Prakash Panangaden and Gordon Plotkin, in an attempt of extending the classic equational theory to obtain a new, quantitative version of equational theory and its metatheory. I will present a couple of axiomatizations of some classic behavioural distances and present some general variety and quasivariety theorems, which generalize the classic Birkhoff theorems.
• Petros Papapanagiotou, AIAI, School of Informatics, University of Edinburgh
  Logic-based workflow management and optimisation
  In the past few years we have developed the process modelling framework WorkflowFM. It relies on the proofs-as-processes paradigm, implemented in HOL Light, to provide correct-by-construction workflow synthesis. More recently, we have applied such workflow models for the monitoring and optimisation of production flows in manufacturing within the DigiFlow project. This effort has introduced interesting challenges, such as persistent distributed enactment, integration with IoT data, and job-shop scheduling. I will give an overview of our journey from theory to practice and discuss some research ideas for our next steps.
• Ciaran Dunne, Department of Computer Science, Heriot-Watt University
  Mathematical Foundations More Suitable for Education and Verification
  Zermelo-Fraenkel (ZF) set theory is an axiomatic system, widely recognised as a tried and tested mathematical foundation. However, there still remains a wide disparity between the use of set theory in such foundational systems, and standard mathematical practice.
  In practice, mathematicians use a combination of natural language, set-theoretic notation, and first order logic. Such texts are labourious to formalise in theories like ZF, due to the fact that must reduce everything to statements about sets. ZF is also a bad candidate for computer verification of mathematical text, since the search space for valid proof steps is so large. Even famous type theoretic proof assistants such as Coq and Agda fail to gain the attraction of ordinary mathematicians.
  In this talk, I will discuss my current work with Joe Wells in creating a variant of set theory that is suitable for both humans and computers. I will give a presentation of an extension of ZF that admits ordered pairs as non-set objects (urelements), and discuss the relation between these objects and inductive datatypes. I will also highlight other features which are desirable in this context, such as exceptions and definite descriptions.
• Oana Andrei, School of Computing Science, University of Glasgow
  Interpreting Probabilistic Models of Social Group Interactions in Meetings
  A major challenge in Computational Social Science consists in modelling and explaining the temporal dynamics of human communications. Understanding small group interactions can help shed light on sociological and social psychological questions relating to human communications. Which interactions lead to more successful communication or productive meetings? How can we infer temporal models of interactions? How can we explain what these temporal interaction really mean? Current statistical analysis techniques do not explore the full temporal aspect of time-series data generated by interactive systems, and certainly they do not address complex queries involving temporal dependencies. We investigated discrete-time Markov chains with rewards for human-human interactions in social group meetings on a dataset taken from a standard corpus of scenario and non-scenario meetings, the Augmented Multimodal Interaction (AMI) meeting corpus. We identified various queries predicating over the temporal interactions between different roles, the impact of different sentiments in interactions or in decision making, causality between particular states, etc.. We demonstrated the expressiveness of probabilistic temporal logic properties for formalising various queries about group interactions in meetings, we analysed the properties with the probabilistic model checker PRISM, which them helped us interpret the temporal interaction models. One subset of the queries validated our behavioural model as their results confirmed expected interactions, while another subset highlighted novel insight into the AMI dataset we analysed.
• Juan Casanova, School of Informatics, University of Edinburgh
  CESQ Logic: A formalism for expressing queries in restricted second-order logic
  CESQ Logic stands for Computational Existential Second-order Query Logic (This name may still change as we proceed forward). Its name is pretty descriptive of its nature (which I will present in further detail during the talk), and the reasons for our developing and using it are many and of different nature, but a summary would be as follows.
  In our work developing methods for automatically detecting faults in ontologies using meta-level patterns, our approach has lead us to a comfortable spot of doing queries on first-order logic ontologies (theories), using restricted second-order variables in the queries: mainly, they cannot be universally quantified. These second-order variables are in practice the interrogative pronouns (the "whats") of our queries: we wish to find instantiations of them that make our query body provable or satisfiable in our theories. This level of expressivity offers us what we need to run the kind of searches that we wish on our ontologies, using the algorithm that we have developed for that purpose, while remaining still far from full second-order or even higher-order logic expressivity ranges. The reason for avoiding these is the "query" part of our logic: we do not prove theorems, we look for potentially infinite sets of instantiations of variable theorems. This dramatically increases the search space (and the solution space) of our problem and makes it (arguably, but not yet provably) infeasible for larger expressivity ranges like the ones mentioned.
  CESQ Logic formalizes these queries, expressing not only their truth semantics, but also partial computation semantics: different queries may have the same solutions but force a certain approach for their computation. This is what gives CESQ Logic its "Computational" adjective, and it is important to emphasize its partial nature: While queries restrict the range of valid computation strategies, they do not fully determine the exact one to be carried out. This may seem odd at first but it is well defined within the logic, has an intuitive reason for it and, most importantly, a fundamental pragmatic motivation: automatically deciding the best computation procedure for each query from nothing (through heuristics) is ineffective, but a general strategy for the query solving can and has been described and (almost) implemented.
  In the talk, I will try to explain these notions a bit better, present the overall nature of the logic and give a few hints as to why we have deemed it the best option for our purposes.