Verification Series

Tight width minimisation of self-join-free quantified conjunctive queries

29th October 2026, 11:00 add to calenderAshton 208
Sam Thompson
University of Liverpool

Abstract

Query minimisation is a classical problem in database theory and the width of a formula, defined as the maximum number of free variables over all subformulae, is a central measure for query evaluation. This talk will consider width minimisation for a subclass of quantified conjunctive queries (QCQs), namely self-join-free QCQs. I'll present a result that, for this class, rewriting optimality coincides with semantic optimality: given a query φ, the minimum-width query obtainable from φ by applying natural and established rewriting rules has minimum width among all first-order formulae logically equivalent to φ. As a consequence, the width of a self-join-free QCQ can be optimised by a logical-equivalence-preserving rewriting algorithm.

(This is based on joint work with Hubie Chen and Fabio Mogavero, to appear at PODS 2027.)
add to calender (including abstract)