The sixteenth meeting of the Wessex Theory Seminar took place at Imperial College London on August 29th 2012. It was a farewell workshop for Dirk Pattinson and Tadeusz Litak.
The talks were held in room 213 (Clore Lecture Theatre), Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2RH.
11:00 - 11:45 Lutz Schroeder (Friedrich-Alexander-Universität Erlangen-Nürnberg), Coalgebraic logic and self-reference
11:45 - 12:30 Alexandra Silva (Radboud University Nijmegen), Brzozowski's algorithm, (co)algebraically
12:30 - 13:45 lunch break
13:45 - 14:30 James Brotherston (University College London), Cyclic abduction of inductive termination preconditions
14:30 - 15:15 Peter Hancock (University of Strathclyde), On stuttering equivalence
15:15 - 16:00 Frank Wolter (University of Liverpool), Ontology-based data access and CSP: towards a link between modal logic and constraint satisfaction
16:00 - 16:30 coffee break
16:30 - 17:15 Rasmus Mogelberg (IT University of Copenhagen), The topos of trees as a model of guarded recursion
17:15 - 18:00 Christian Urban (Kings College London), The Myhill-Nerode Theorem in a Theorem Prover
Decidability of modal logics tends to break down quickly when features for self-reference are added,
such as the down-arrow binder of hybrid logic, or its single-variable version popularized by Marx as the I-me construct.
We have shown in earlier work that decidability (and in fact low complexity) of logics with I-me is regained if the number
of modal operators between between each use of me and its enclosing I is bounded by two. In the case of the description
logic ALCQ, the corresponding extension by depth-2 I-me turns out to be equivalent to the addition of a number of well-known
features: inverses, role hierarchies, safe boolean role combinations, and sROIQ's self-loop construct. Here, we report on
ongoing work aimed at a coalgebraic generalization of the algorithmic principles involved.
We give a new presentation of Brzozowski's algorithm to minimize
using elementary facts from universal algebra and coalgebra,
and building on earlier work by Arbib and Manes on the duality
between reachability and observability.
This leads to a simple proof of its correctness and opens the door to
further generalizations. Notably, we derive algorithms to minimize
Moore, non-deterministic and weighted automata.
Going all the way back to Alan Turing, people have asked the
question "does this program ever terminate?". In this talk, I want
to go further and ask "can we find a reasonable precondition under
which this program terminates?". When one considers
heap-manipulating programs, this problem - which is one of
abduction, or synthesis - typically involves inventing the
inductive definitions of data structures. For example, a program
that traverses a list will terminate given a heap structured as an
acyclic list as input. But given a cyclic list, it will fail to
terminate, and given something that is not a list at all, it will
typically encounter a memory fault and crash.
Here I demonstrate a new method, called cyclic abduction, for
automatically inferring the inductive definitions of termination
preconditions for heap-manipulating programs. That is, given a
program, this method returns the definition of an inductively
defined predicate in separation logic under which the program is
guaranteed to terminate (without crashing). Cyclic abduction
essentially works by searching for a cyclic proof of termination
of the program, abducing definitional clauses of the precondition
as necessary to advance the proof search process.
We have constructed abduction proofs for a range of small programs
both by hand, and automatically, using a custom cyclic theorem
prover. The abduced predicates may define segmented, cyclic,
nested, and/or mutually defined data structures.
This is joint work with Nikos Gorogiannis (also at UCL).
The notion of stuttering equivalence, or at least the name, is due to Leslie Lamport,
and plays an important role in his version of quantified linear-time temporal logic.
Some published definitions of this notion are plain broken. It turns out that a
possible (correct) definition has the form of a nested coinductive-inductive definition, a form
that Dirk may recognise.
In recent years, the use of ontologies (=logical theories) to access instance data has become
increasingly popular. The general idea is that an ontology provides a vocabulary or conceptual
model for the application domain, which can then be used as an interface for querying instance
data and to derive additional facts.
In this presentation, I will introduce ontology-based data access for ontologies given in modal logic
(aka description logic) and investigate the following non-uniform complexity problem: what is the data
complexity of query answering for a fixed ontology? I will present general conditions under which this
problem is in PTime and, respectively, coNP-hard. Then it is shown that query answering
in modal logic is equivalent to solving constraint satisfaction problems (CSPs) with finite templates.
This result provides a very close link between modal logic and CSPs - a very active research area
combining methods from logic, graph theory, algebra, and combinatorics.
This link has numerous consequences for modal logic. For example, a P/coNP dichotomy holds for
with query answering in modal logic if, and only if, Feder and Vardi¿s dichotomy conjecture for CSPs holds.
We show how the topos of trees, i.e., the category of presheaves over the ordered
natural numbers, models guarded recursive terms, predicates and types.
We have two motivations for this work: one is as a model of
computation with coinductive types such as streams, using guards to ensure
well-definedness of recursive definitions. The other is the construction of
models of programming languages with higher-order store, which involves
solving recursive domain equations. But since guarded recursion is commonplace
in computer science we expect many more applications.
In the talk I will give a computational intuition for the topos of trees and
show how the internal logic of this model can be used as an expressive
language combining dependent types and subset types with guarded recursion.
I will also sketch how to construct a model of higher-order store entirely inside
this language, using a combination of set-like constructions and guarded recursion.
Relations to step-indexing and metric space models of guarded recursion will be discussed.
There are numerous textbooks on regular languages. Many of them focus
on finite automata for proving properties. Unfortunately, automata are
not so straightforward to formalise in theorem provers. The reason is
that natural representations for automata are graphs, matrices or
functions, none of which are inductive datatypes. Regular expressions
can be defined straightforwardly as a datatype and a corresponding
reasoning infrastructure comes for free in theorem provers. I will show
in this paper that a central result from formal language theory - the
Myhill-Nerode Theorem - can be recreated using only regular
expressions. From this theorem many closure properties of regular
From King's College London:
From Queen Mary:
From University College London:
See all Wessex sites involved and meetings so far.