• Canada
• UK Research and Innovation close
• UKRI|EPSRC close
• 2021 close
• 2025 close

A statement is quantified if it has a qualification such as "for all" or "there exists". Let us consider an example commonly encountered in high school mathematics when studying quadratics: "there exists x such that ax^2 + bx + c = 0 has two different solutions for x". The statement is mathematically precise but the implications are unclear: what restrictions does this statement of existence force upon us? Quantifier Elimination (QE) replaces such a statement by an equivalent unquantified one, in this case by "either a is not zero and b^2 - 4ac is greater than 0, or all of a=b=c=0". The quantifier "there exists" and the variable x have been eliminated. The key points are: (a) the result may be derived automatically by a computer from the original statement using QE; (b) QE uncovers the special case when a=0 which humans often miss! Solutions to QE problems are not numbers but algebraic descriptions which offer insight. In the example above QE did not provide solutions to a particular equation - it told us in general how the number of solutions depends on (a,b,c). QE makes explicit the mathematical structure that was hidden: it is a way to "simplify" or even "solve" mathematical problems. For statements in polynomials over real numbers there will always exist an equivalent formula without the quantification. However, actually obtaining the answer can be very costly in terms of computation, and those costs rise with the size of the problem. We call this the "doubly exponential wall" in reference to how fast they rise. Doubly exponential means rising in line with the power of a power, e.g. a problem of size n costs roughly 2^(2^n). When applying QE in practice, results may be found easily for small problems, but as sizes increase you inevitably hit the wall where a computation will never finish. The doubly exponential wall cannot be broken completely: this rise in costs is inevitable. However, the aim of this project is to "push back the wall" so that lots more practical problems may be tackled by QE. The scale here means that pushing the wall even a small way offers enormous potential: e.g. 2^(2^4) is less than 66,000 while 2^(2^5) is over 4 billion! We will achieve this through the development of new algorithms, inspired by an existing process (cylindrical algebraic decomposition) but with substantial innovations. The first innovation is a new computation path inspired by another area of computer science (satisfiability checking) which has pushed back the wall of another famously hard problem (Boolean satisfiability). The team are founding members of a new community for knowledge exchange here. The second innovation is the development of a new mathematical formalisms of the underlying algebraic theory so that it can exploit structure in the logic. The team has prior experience of such developments and is joined by a project partner who is the world expert on the topic (McCallum). The third innovation is the relaxation of conditions on the underlying algebraic object that have been in place for 40+ years. The team are the authors of one such relaxation (cylindrical algebraic coverings) together with project partner Abraham. QE has numerous applications, perhaps most crucially in the verification of critical software. Also in artificial intelligence: an AI recently passed the U. Tokyo Mathematics entry exam using QE technology. This project will focus on two emerging application domains: (1) Biology, where QE can be used to determine the medically important values of parameters in a system; (2) Economics where QE can be used to validate findings, identify flaws and explore possibilities. In both cases, although QE has been shown by the authors to be applicable in theory, currently procedures run out of computer time/memory when applied to many problem instances. We are joined by project partners from these disciplines: SYMBIONT from systems biology and economist Mulligan.

The Committee on Climate Change suggests that we need to decarbonise all heat in buildings by 2050 to achieve the Net Zero emissions targets. The electrification of heat supply, through either direct electric heating or heat pumps, seems more likely to be realised in practice. However, the complete electrification of heat will result in much higher electricity demand in winter than in summer. Furthermore, due to the consistency of ambient temperature, it will also lead to electricity demand spikiness which is a big challenge for the grid. The HARVEST project will develop a new solution that can absorb and accumulate the curtailed/waste renewable electricity all around the year using thermochemical heat storage technology and then convert and magnify the heat output in winter and cooling output in summer using heat pump technology. The unique features of the proposed solution are: (1) the microwave-assisted process to flexibly absorb renewable electricity; and (2) the compact and efficient regeneration process by direct contact reaction between thermochemical heat storage materials and ammonia solution. We have established a strong multidisciplinary consortium, consisting of leading researchers from the University of Birmingham, the University of Edinburgh, and the University College London, to address the key challenges in both the scientific/technological aspects and social aspects. Our research will significantly contribute to several identified approaches in the 'Decarbonising Heating and Cooling 2' call document, in particular, the 'new technologies of heating and/or cooling' and 'new methods or significant developments for heat storage or cold storage'. Our research is also further supported by the UK and international partners to maximise knowledge exchange and impact delivery.