Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

Lead Research Organisation: Coventry University
Department Name: Ctr for Fluid and Complex Systems

Abstract

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.

Planned Impact

Quantifier Elimination (QE) allows for the removal of quantifiers within logical statements to produce clear unambiguous algebraic descriptions. In this sense QE is the act of simplifying or solving a problem exactly, like pen and paper mathematics. The impact of improved QE procedures is felt not just in mathematics, but throughout engineering and the natural sciences - wherever there is a desire for such solutions.

Impact in such a wide range of fields will be secured via industrial Project Partner Maplesoft, whose European HQ is currently in Cambridge. They produce the Maple Computer Algebra System widely used in science, education and industry (automotive, aerospace, electronics, defence, energy, financial services, consumer products, and entertainment). Maplesoft have committed staff time to transfer project outcomes into their software, and importantly, link them up as sub-routines to the most widely used user commands. Thus our project outcomes will be automatically used by their several million users worldwide. Further, all outcomes will be published in open access to facilitate transfer into other systems.

The project has two objectives on the emerging application of QE to biology and economics. These will in turn have impact outside academia.

- The type of problem we plan to tackle in biology (identifying regions of parameter space for networks in which multistationarity can occur) are ultimately relevant to cancer diagnosis. We will be guided here by project partner, systems biology group SYMBIONT. We will run a workshop on the use of symbolic techniques within computational biology, affiliated with an appropriate systems biology conference, to ensure researchers there are aware of our progress.

- QE applications in economics can be used to improve the quality of economic analysis and models, as performed routinely by governments, central banks, and the civil service. Indeed, project partner Casey Mulligan (U. Chicago) has spent the last two years seconded to the White House where, as confirmed in his letter of support, he has made extensive use of QE technology, "in areas ranging from drug pricing, international trade, environmental quality, telecommunications, labor markets, health insurance, and automobile markets". We plan training sessions at Bath and Coventry for teaching staff on their Economics degree courses to show how QE tools may be used in the economics curriculum.

We note one other application domain of particular importance (and an area of UK strength): Formal Software Verification: the use of computers to check a logical statement beyond all doubt (by successively combining existing results with basic axioms), often used to ensure the correctness of safety-critical systems. The use of QE in such tools is already well known: e.g. KeYmaera combines a theorem prover with real QE procedures for verification in the railway, automotive, and aviation industries, and even for surgical robotics! We do not propose any theoretical research here, but it is important that we disseminate any outcomes to support the EPSRC Resilient Nation outcome. We hence plan to attend industry focused verification events, such as the annual UK Verification Futures conference.

The work is at the intersection of two computer science fields: symbolic computation and satisfiability checking, who have only started working together in the past few years. In order to further encourage this integration and the impact it is having on both fields we will run two workshops, following the successful SC-Square format.

Finally, there will also be some local impacts of the project. It will directly support the UK early career development of two RA's; while the PI will gain the particularly valuable first RCUK standard grant. The project will feed into curriculum development: providing suitable examples, guest lectures and topics for final year projects on the Computer Science degrees at the two sites.

Publications

10 25 50

publication icon
Sadeghimanesh A (2022) An SMT solver for non-linear real arithmetic inside maple in ACM Communications in Computer Algebra

publication icon
Río T (2023) Clustering in the Lazard method for Cylindrical Algebraic Decomposition in ACM Communications in Computer Algebra

publication icon
Davenport J.H. (2023) Iterated Resultants in CAD in CEUR Workshop Proceedings

publication icon
England M. (2022) SC-Square: Overview to 2021 in CEUR Workshop Proceedings

publication icon
Uncu A.K. (2023) SMT-Solving Induction Proofs of Inequalities in CEUR Workshop Proceedings

publication icon
Del Río T. (2023) Data Augmentation for Mathematical Objects in CEUR Workshop Proceedings

publication icon
Röst G (2021) Exotic Bifurcations in Three Connected Populations with Allee Effect in International Journal of Bifurcation and Chaos

 
Title Decomposing Truth 
Description This was an entry into the Art and Creative Works Exhibit of the 2021 Maple Conference: https://www.maplesoft.com/mapleconference/2021/gallery.aspx The entry consisted of both an image: https://matthewengland.coventry.domains/Conferences/Maple21-Art-Image.png and a description https://matthewengland.coventry.domains/Conferences/Maple21-Art-Description.pdf The purpose of the image was to illustrate an application of an algorithm, although the author argued it also held aesthetic value. 
Type Of Art Artwork 
Year Produced 2021 
Impact It received positive comments at the event. 
URL https://www.maplesoft.com/mapleconference/2021/gallery.aspx
 
Title Growing Allee Flowers 
Description The Allee effect is observed in biological systems where species exhib both competitive and cooperative behavior. E.g. the population size need to be above a threshold to not become extinct; but the environment has a limited amount of resources and so the population must also be below a carrying capacity. In exploring systems with this behaviour the author (DEWCAD PDRA Amirhossein SadeghiManesh) discovered that plots of the parameter space resembled flowers and used that to generate this artwork as a tool to attract people to the science. A more detailed description can be found on the document accompanying the artwork on the URL below. 
Type Of Art Artwork 
Year Produced 2022 
Impact Entry into the Maple Conference 2022 Art Gallery 
URL https://www.maplesoft.com/mapleconference/2022/art.aspx
 
Title Singly vs Doubly Exponential 
Description The artwork consists of two photos by PhD student Tereso del Rio who works alongside the DEWCAD project. One photo shows piles of grain growing exponentially, and the next piles growing doubly exponentially. The piece is designed to show the dramatic different between these two large rates of growth. It very well illustrates the "Doubly Exponential Wall" that the DEWCAD project titled references. 
Type Of Art Artwork 
Year Produced 2022 
Impact This was in the Maple Conference 2022 Art Gallery. 
URL https://www.maplesoft.com/mapleconference/2022/art.aspx#maple
 
Description #1 There has been progress on new CAD computation schemes. In particular, an approach that utilises a proof system so separate out the steps neededfor mathematical correctness from those that can be optimised by heuristic decisions. This allows for more structured and documented optimisations and clearer proofs of correctness.

#2 Progress on the use of this technology in biology for identifyign multistationarity in chemical reaction networks: a new hybrid symbolic-numeric scheme offers advantages from both worlds.

#3 The collaboarations between symbolic computation and computer algebra have continued to be deepended through our sponsorshipof the SC-Square initiative. The use of CAD in this context has generated new variants of the set covering problems now being studied independently.
Exploitation Route This remains to be seen. But the project has workpackages to ensure use in biology and economics fields which can be reported on next year.
Sectors Digital/Communication/Information Technologies (including Software)

Education

Pharmaceuticals and Medical Biotechnology

URL https://matthewengland.coventry.domains/dewcad/
 
Description The work on cylindrical algebraic coverings [1] developed as part of this project has found impact. It was reimplemented as a core routine in the widely used SMT solver cvc5 [2]. This implementation is now widely seen as the state-of-the-art SMT solver for non-linear real arithmetic, winning the 2023 SMT competiotion in this track for example. The software is used by many businesses including Amazon, and is a core tool in many scientific endeavours. [1] E. Abraham, J.H. Davenport, M. England and G. Kremer. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings. Journal of Logical and Algebraic Methods in Programming, 119, 100633, Elsevier, 2021. [2] G. Kremer, E. Abraham, M. England and James H. Davenport. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. In Proceedings of the 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2021), pp. 37-39. IEEE, 2021.
First Year Of Impact 2022
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Economic

 
Description Deakin University - Coventry University cotutelle scheme (pair of PhD students)
Amount £180,000 (GBP)
Organisation Deakin University 
Sector Academic/University
Country Australia
Start 04/2025 
End 11/2028
 
Title SMT-Solving Induction Proofs of Inequalities Benchmarking Repository 
Description This repository contains the full list of files and the benchmarking results that were used in the benchmarking processes described in the paper: A.K. Uncu, J.H. Davenport and M. England. "SMT-Solving Induction Proofs of Inequalities". Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2022). The files are split in three branches. The Mathematica and Maple files include the calls that were made to the respective computer algebra systems, and the smt2 files are the ones used by the considered SMT solvers: Z3, CVC5 and Yices. The Benchmarking Results cvc has the results. The columns record the file names, the satisfiability outcome of the calls, then the times (in seconds) of the respective programmes. Any empty box (which the Maple:-RegularChains column has) would mean that the implementation does not accept that sort of input (this is due to rational functions - see the paper for details). Any time over 1200 seconds would mean that the program times out and the outcome of the question was not found in the given time. 
Type Of Material Database/Collection of data 
Year Produced 2023 
Provided To Others? Yes  
URL https://zenodo.org/record/7777296
 
Description Chicago - Economics 2023 
Organisation University of Chicago
Country United States 
Sector Academic/University 
PI Contribution This is a collaboration between the DEWCAD project team and Prof. Casey Mulligan who is an economist at the University of Chicago. The collaboration is on the application of QE procedures to problems in economics. The DEWCAD team contribute the expertise in QE.
Collaborator Contribution Our partner contributes the expertise and example data frome economics: chosen either for economic interest or computational difficulty. We collaboratedbefore in 2017-2019. We have now in 2023 revived the collaboration.
Impact Chapter 10 of the politics book aimed at a general audience published by Prof. Mulligan in 2020 detailed work emitting from our previous collaboration. Casey Mulligan. "You're Hired!: Untold Successes and Failures of a Populist President". Republic Book Publishers, 2020. ISBN 1645720136 In 2023 Prof. Mulligan gave testimony before the US Senate Committee on Commerce, Science and Transportation hearing on "Bringing Transparency and Accountability to Pharmacy Benefit Managers", in which he cited our joint work. https://www.commerce.senate.gov/2023/2/bringing-transparency-and-accountability-to-pharmacy-benefit-managers
Start Year 2023
 
Description Dagstuhl 22072 
Organisation Fondazione Bruno Kessler
Country Italy 
Sector Private 
PI Contribution Both DEWCAD sites, James H. Davenport (Bath) and Matthew England (Coventry) were organisers of Dagstuhl Workshop 22072: New Perspectives in Symbolic Computation and Satisfiability Checking. The seminar was run in hybrid mode with 50% of attendees in person and 50% online. PhD students from Bath (Corin Lee) and Coventry (Tereso del Rio) provided the local technical support to the seminar and the DEWCAD postdoc at Coventry (Amirhossein Sadeghi Manesh) from online technical support for online participants.
Collaborator Contribution The other two organisers of the workshop were Alberto Griggio (FBK) and Erika Abraham (RWTH Aachen). Toegther the 4 organsiers bid for the seminar, attracted the participants, planned the schedule and ensured the smooth running and success.
Impact To be confirmed.
Start Year 2021
 
Description Dagstuhl 22072 
Organisation RWTH Aachen University
Department Department of Computer Science
Country Germany 
Sector Academic/University 
PI Contribution Both DEWCAD sites, James H. Davenport (Bath) and Matthew England (Coventry) were organisers of Dagstuhl Workshop 22072: New Perspectives in Symbolic Computation and Satisfiability Checking. The seminar was run in hybrid mode with 50% of attendees in person and 50% online. PhD students from Bath (Corin Lee) and Coventry (Tereso del Rio) provided the local technical support to the seminar and the DEWCAD postdoc at Coventry (Amirhossein Sadeghi Manesh) from online technical support for online participants.
Collaborator Contribution The other two organisers of the workshop were Alberto Griggio (FBK) and Erika Abraham (RWTH Aachen). Toegther the 4 organsiers bid for the seminar, attracted the participants, planned the schedule and ensured the smooth running and success.
Impact To be confirmed.
Start Year 2021
 
Description FUB: Automating Detection of Bifurcations of Polynomial Ordinary Differential Equations 
Organisation Free University of Berlin
Country Germany 
Sector Academic/University 
PI Contribution This is a new collaborative project between the PDRA on our project, Amirhosein SadeghiManesh, and Nicola Vassena at Free University Berlin. The project is supported by an LMS travel grant.
Collaborator Contribution Nicola Vassena spent a week in Coventry in April 2023 for collaborative research, supported by an LMS grant.
Impact No outputs yet - under preparation.
Start Year 2022
 
Description Macquarie University: Equational Constraint Technology 
Organisation Macquarie University
Country Australia 
Sector Academic/University 
PI Contribution This collaboration between the DEWCAD team and Macquarie University is to develop new theory to take advantage of multiple equational constraints in CAD. The DEWCAD team provided expertise on the QE procedures.
Collaborator Contribution Macquarie University (Prof. Scott McCallum) is a world expert in the mathematics than underpins CAD projection.
Impact J.H. Davenport, M. England, S. McCallum, and A.K. Uncu. Iterated Resultants and Rational Functions in Real Quantifier Elimination. Submitted, 2024. Preprint arXiv:2312.16210
Start Year 2023
 
Description Maplesoft - DEWCAD 
Organisation Maplesoft
Country Canada 
Sector Private 
PI Contribution Coventry University have a multi-stranded and long standing collaboration with the software company Maplesoft, providing fundamental research than improves their software product.
Collaborator Contribution Maplesoft are a partner of the DEWCAD project. They have provided technical advice on programmaing in Maple to the DEWCAD PDRA and feedback from their Senior Director of research. They have provided access to internal company software tools to produce high quality documentation for our software packages.
Impact For example, the code release at the DOI below utilised the internal documentation making tool: 10.5281/zenodo.6646133
Start Year 2021
 
Description RWTH & US Naval: Proof System 
Organisation RWTH Aachen University
Country Germany 
Sector Academic/University 
PI Contribution This collaboration between the DEWCAD team, RWTH Aachen and the US Naval Academy was to produce a new CAD implementation which utilised a proof system approach to separate out the steps neccessary for correctness from those that could be subject to heuristic choices. The DEWCAD team provided expertise on the QE procedures.
Collaborator Contribution RWTH Aachen brought the expertise on the proof system framework.
Impact J. Nalbach, E. Abraham, P. Specht, C.W. Brown, J.H. Davenport, and M. England Levelwise construction of a single cylindrical algebraic cell. Journal of Symbolic Computation, 123, Article Number 102288. Elsevier, 2024. Digital Object Identifier: 10.1016/j.jsc.2023.102288
Start Year 2021
 
Description RWTH & US Naval: Proof System 
Organisation United States Naval Academy
Country United States 
Sector Academic/University 
PI Contribution This collaboration between the DEWCAD team, RWTH Aachen and the US Naval Academy was to produce a new CAD implementation which utilised a proof system approach to separate out the steps neccessary for correctness from those that could be subject to heuristic choices. The DEWCAD team provided expertise on the QE procedures.
Collaborator Contribution RWTH Aachen brought the expertise on the proof system framework.
Impact J. Nalbach, E. Abraham, P. Specht, C.W. Brown, J.H. Davenport, and M. England Levelwise construction of a single cylindrical algebraic cell. Journal of Symbolic Computation, 123, Article Number 102288. Elsevier, 2024. Digital Object Identifier: 10.1016/j.jsc.2023.102288
Start Year 2021
 
Description U. Cincinnati - XAI and CAD 
Organisation University of Cincinnati
Country United States 
Sector Academic/University 
PI Contribution This collaboration seeks to use Explainable AI (XAI) methods on an analysis of Ml models for computer algebra to learn new information on the underlying algebraic algorithm. The collaboration is with PhD student Lynn Pickering at U. Cincinnati. We provided the expertise on the underlying algebraic algorithm and on prior use of ML for its optimisation.
Collaborator Contribution Our collaborators provided the XAI expertise.
Impact L. Pickering, T. Del Rio Almajano, M. England and K. Cohen Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition. Journal of Symbolic Computation, 123, Article Number 102276. Elsevier, 2024. https://doi.org/10.1016/j.jsc.2023.102276
Start Year 2022
 
Title CRNPy 
Description This Python package contains implementation of several algorithms to study Chemical Reaction Networks (CRNs) mathematically. 
Type Of Technology Software 
Year Produced 2021 
URL https://zenodo.org/record/5770251
 
Title CRNPy 
Description This Python package contains implementation of several algorithms to study Chemical Reaction Networks (CRNs) mathematically. 
Type Of Technology Software 
Year Produced 2021 
Open Source License? Yes  
Impact Used in a masters student project at Coventry University which explored data science approaches to problems in CRN classification. 
URL https://zenodo.org/record/5770252
 
Title Computation files of the paper Matrix decomposition by transforming the unit sphere to an Ellipsoid through Dilation, Rotation and Shearing 
Description This Zenodo repository contains the computation files related to the paper "Matrix decomposition by transforming the unit sphere to an Ellipsoid through Dilation, Rotation and Shearing". It also contains a Maple package, Ellipsoids, and a Matlab equivalent of it in a Matlab script file. 
Type Of Technology Software 
Year Produced 2022 
URL https://zenodo.org/record/7021478
 
Title Computation files of the paper Polynomial Superlevel Set Representation of the Multistationarity Region of Chemical Reaction Networks 
Description This Zenodo repository contains the computation files related to the paper "Polynomial Superlevel Set Representation of the Multistationarity Region of Chemical Reaction Networks". It contains several Matlab script and Maple worksheet files and their pdf print outs, it also contains one Julia file and two input files for MCKR app and their outputs. These files cover all the computations and plots of the paper. 
Type Of Technology Software 
Year Produced 2022 
URL https://zenodo.org/record/5911941
 
Title Computation files of the paper Resultant Tools for Parametric Polynomial Systems with Application to Population Models 
Description This zenodo repository contains the computation files related to the paper "Resultant Tools for Parametric Polynomial Systems with Application to Population Models". It contains a Maple package, ResChain, and several Maple worksheets containing all the computations and plots in the paper. 
Type Of Technology Software 
Year Produced 2022 
URL https://zenodo.org/record/5902593
 
Title Computation files of the paper Resultant Tools for Parametric Polynomial Systems with Application to Population Models 
Description This zenodo repository contains the computation files related to the paper "Resultant Tools for Parametric Polynomial Systems with Application to Population Models". It contains a Maple package, ResChain, and several Maple worksheets containing all the computations and plots in the paper. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
Impact Software to use for calculating chains of iterated resultants in the case of computing a discriminant variety. 
URL https://zenodo.org/record/5902594
 
Title Data and code for the paper New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis 
Description This repository contains all the data and code necessary to generate the results and figures presented in the 2022 CASC paper of Tereso del Río and Matthew England. It contains a dataset in a .csv file, a .tex describing the dataset and seven .py files containing the code used to analyse the dataset. To generate the figures in the paper and the dataset used to create the table in the paper run the Python code named 'run_for_paper.py' inside the folder 'Code'. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
URL https://zenodo.org/record/6750306
 
Title Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition 
Description This toolbox supports the results in the following publication: Pickering, L., del Río, T., England, M. and Cohen, K., 2023. Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition. https://doi.org/10.1016/j.jsc.2023.102276.   Abstract: In recent years there has been increased use of machine learning (ML) techniques within mathematics, including symbolic computation where it may be applied safely to optimise or select algorithms.  This paper explores whether using explainable AI (XAI) techniques on such ML models can offer new insight for symbolic computation, inspiring new implementations within computer algebra systems that do not directly call upon AI tools.  We present a case study on the use of ML to select the variable ordering for cylindrical algebraic decomposition.  It has already been demonstrated that ML can make the choice well, but here we show how the SHAP tool for explainability can be used to inform new heuristics of a size and complexity similar to those human-designed heuristics currently commonly used in symbolic computation. 
Type Of Technology Software 
Year Produced 2023 
Open Source License? Yes  
URL https://zenodo.org/doi/10.5281/zenodo.8229297
 
Title SCPPack 
Description This is a Maple package to study Set Covering Problem (SCP) and Set Covering Problems with Reasons (SCPR). It contains a package mla file, a demo worksheet, the source code files with a help file for each function in this package. 
Type Of Technology Software 
Year Produced 2022 
URL https://zenodo.org/record/6609201
 
Title SCPPack 
Description This is a Maple package to study Set Covering Problem (SCP) and Set Covering Problems with Reasons (SCPR). It contains a package mla file, a demo worksheet, the source code files with a help file for each function in this package. 
Type Of Technology Software 
Year Produced 2022 
Impact Supporting research of a new PhD student at Coventry University (Abiola Babatunde) on this new NP problem. 
URL https://zenodo.org/record/6609202
 
Title Supporting files for the mathematical art Growing Allee Flowers 
Description This Zenodo repository contains the Maple worksheet supporting the mathematical art work titled "Growing Allee Flowers". 
Type Of Technology Software 
Year Produced 2022 
URL https://zenodo.org/record/7105453
 
Description 2023 Presentation to British Computer Society (Coventry Branch) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Industry/Business
Results and Impact DEWCAD PI gave an invited talk titled "Real Quantifier Elimination: Recent Algorithmic Progress and Applications".
Year(s) Of Engagement Activity 2023
URL https://coventry.bcs.org/branch-programme-2023-2024/
 
Description Abram Gannibal Project Workshop 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Matthew England (Coventry) was invited to give a talk at the workshop of the Abram Gannibal Project, at Chicheley Hall, Buckinghamshire, in March 2022.

The Abram Gannibal project aims to establish collaborations between UK mathematicians and emerging Sub-Saharan African scientists and their research groups to tackle a range of problems arising in technological challenges relevant to the African development context. Dr England was invited to talk on the DEWCAD project, with a focus on the applications of the work. The audience was mostly postgraduate students from Africa who were having a research visit to the UK.
Year(s) Of Engagement Activity 2022
URL https://people.maths.ox.ac.uk/agp/AG.html
 
Description Invited Talk at Chulalongkorn University, Thailand 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Undergraduate students
Results and Impact DEWCAD Project PDRA, Amirhossein Sadeghi Manesh, gave an invited talk at Chulalongkorn University in Thailand. The talk was open to all in the Department of Mathematics and Computer science. As such, it was tailored to an UG audience with a broad title: "In a Search for Cheaper Computer Algebra Tools to Answer Real World Problems"
Year(s) Of Engagement Activity 2023
URL https://matthewengland.coventry.domains/dewcad/img/Amir-Jan23Talk-Poster.jpg
 
Description Invited Talk at Johannes Kepler University, Linz, Austria 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Postgraduate students
Results and Impact DEWCAD PDRA Matthew England was invited to give a talk at Johannes Kepler University, Linz, in the Institute of Algebra Seminar Series. The presentation was titled, Cylindrical Algebraic Coverings: An SC-Square Success Story.
Year(s) Of Engagement Activity 2022
URL http://www.algebra.uni-linz.ac.at/teaching/seminar/schedule.php?term=ws2022
 
Description SC-Square Workshop 2022 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact As planned in the original proposal, the DEWCAD project sponsored an edition of the SC-Square Workshop. This allowed for feedback on DEWCAD outputs and dissemination of related work from around the world. The event took place in Haifa, Israel as part of the Federated Logic Conference.
Year(s) Of Engagement Activity 2022
 
Description SC-Square Workshop 2023 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact As planned in the original proposal, the DEWCAD project sponsored an edition of the SC-Square Workshop. This allowed for feedback on DEWCAD outputs and dissemination of related work from around the world. The event took place in Tromso, Norway as part of the International Symposium on Symbolic and Algebraic Computation.
Year(s) Of Engagement Activity 2023
URL http://www.sc-square.org/CSA/workshop8.html
 
Description STEM for Britain 2022 Competition 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Policymakers/politicians
Results and Impact STEM for BRITAIN is an annual scientific poster competition, in which finalists are invited to exhibit their poster in the Houses of Parliament, Westminster, London. Its aim is to give members of both Houses an insight into the research undertaken in UK universities by early-career researchers.

DEWCAD postdoctoral researchers, Amirhossein Sadeghi Manesh, was selected for the final of the Mathematics category. His poster was titled, "SAVING RESEARCH BUDGETS BY IMPROVING ALGEBRAIC TOOLS \\FOR THE STUDY OF POPULATION DYNAMICS". He will travel to London on 7th March 2022 for the final.
Year(s) Of Engagement Activity 2022
URL https://stemforbritain.org.uk/stem-for-britain-mathematical-sciences-exhibition-2022/
 
Description STEM for Britain 2024 Competition 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Policymakers/politicians
Results and Impact STEM for BRITAIN is an annual scientific poster competition, in which finalists are invited to exhibit their poster in the Houses of Parliament, Westminster, London. Its aim is to give members of both Houses an insight into the research undertaken in UK universities by early-career researchers. Coventry UNiversity PhD student, Abiola Babatunde, is co-supervised by the DEWCAD PI and PDRA on a topic related to DEWCAD. He was selected for the final of the Mathematics category. His poster was titled, "Using Set Covering Problem Variants for Detecting Genes Responsible for Diseases". He travelled to London on 3rd March 2024 for the final.
Year(s) Of Engagement Activity 2024
URL https://stemforbritain.org.uk/