Thirteenth Meeting of the Southern Logic Seminar, University of Bath

The thirteenth meeting of the Southern and Midlands Logic Seminar will be held on the afternoon Wednesday 11 February 2026 at the University of Bath. Talks will take place in 3 East 2.1 on the main Claverton Down campus.

Participants are encouraged to join the Southern and Midlands Logic Seminar community on Slack, which is used for announcements and coordination. Please contact one of the organisers to be added.

The meeting is supported by a London Mathematical Society Joint Research Groups grant, with additional funding from the Mathematical Foundations of Computation group at Bath.

Programme

Abstracts for the talks are available below.

Venue

The main campus of the University of Bath is located on a hilltop just outside the city centre. It is within walking distance from Bath Spa train station in principle, but you should allow 30–40 minutes and be wary that the route involves a steep uphill climb. A more comfortable alternative is to take one of the regular bus connections from the city centre to the campus. Further information on how to get to the university can be found here, with details of bus routes here.

Talks will take place in 3 East 2.1. Anyone arriving before lunchtime can find the local participants in the Department of Computer Science, on the fourth floor of 1 West. The campus map might be helpful if you get lost.

Travel bursaries

Each meeting has a small budget to cover travel costs for speakers and participants. Priority will be given to young researchers, particularly PhD students. We are also able to provide some support for participants with caring or parenting responsibilities. Anyone who requires support should contact Thomas Powell in advance of the meeting.

Abstracts

"To contract, or to delete, that is the questio" Gecia Bravo-Hermsdorff, Bath
The analogy between graphs and electrical circuits has played a fundamental role in the development of graph theory, and its myriad connections to other branches of mathematics and science. The discrete graph Laplacian, an operator related to diffusion on graphs, and the effective resistance are two major players in this story. I will introduce you to these characters by describing how we used them to make a graph reduction algorithm that preserves global structure while reducing it via the dual operations of edge deletion and contraction. This will lead us to a surprising connection with the Tutte polynomial, a fundamental combinatorial invariant with deep connections to a wide range of other topics.

"TBC" Till Rampe, Birmingham

"A Logic for Fresh Labelled Transition Systems" Hamza Bandukara, Queen Mary
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.

"Double negation elimination and the multiple succedent structure of LK" Nox Cowie, Sussex
The classical natural deduction system NK can be obtained from the intuitionistic system NJ by adding a double negation elimination inference rule. On the other hand, the intuitionistic and classical sequent calculi LJ and LK are differentiated not by the addition of a rule, but by the number of formulae that can be contained in the right-hand side of a sequent. In an LJ-derivation, the right-hand side of a sequent can contain at most one formula; the classical LK is obtained by lifting this restriction. This distinction between LJ and LK is of a notably different nature than that between NJ and NK: the first being purely structural, and the second involving the explicit addition of a classical inference pattern. We demonstrate how the classical strength of double negation elimination emerges from the structural feature of right multiplicity by examining the relationship between derivations in natural deduction and sequent calculus and, in particular, applications of their respective implication and negation inference rules. As a result, we clarify how right multiplicity constitutes a counterpart to the principle of double negation elimination.

"Tropical homotopies two ways" Yue Ren, Durham
This talk revolves around the efficient computation of the solutions to systems of polynomial equations. We will recap methods from the current state of the art, the maths behind them and their limitations. We will then give an introduction to tropical geometry, outline how it can help us push beyond it, and which theoretical and practical challenges need to be overcome.

Organisers