# Real Geometry and Connectedness via Triangular Description

Lead Research Organisation:
University of Bath

Department Name: Computer Science

### Abstract

Connectedness, as in "can we get there from here", is a fundamental concept, both in actual space and in various abstract spaces. Consider a long ladder in a right-angled corridor: can it get round the corner? Calling it a corridor implies that it is connected in actual three-dimensional space. But if we consider the space of configurations of the ladder, this is determined by the position and orientation of the ladder, and the `corridor' is now the requirement that no part of the ladder run into the walls - it is not sufficient that the ends of the ladder be clear of the walls. If the ladder is too long, it may have two feasible positions, one in each arm of the corridor, but there may be no possible way to get from one to the other. In this case we say that the configuration space of the ladder is not connected: we can't get the ladder there from here, even though we can get each end (taken separately, which is physically impossible) from here to there. Connectedness in configuration space is therefore the key to motion planning. These are problems human beings (especially furniture movers, or people trying to park cars in confined spaces) solve intuitively, but find very hard to explain. Note that the ladder is rigid and three-dimensional, hence its position is determined by the coordinates of three points on it, so configuration space is nine-dimensional.

Connectedness in mathematical spaces is also important. The square root of 4 can be either 2 or -2: we have to decide which. Similarly, the square root of 9 can be 3 or -3. But, if 4 is connected to 9 in our problem space (whatever that is), we can't make these choices independently: our choice has to be consistent along the path from 4 to 9. When it is impossible to make such decisions totally consistently, we have what mathematicians call a `branch cut' - the classic example being the International Date Line, because it is impossible to assign `day' consistently round a globe. In previous work, we have shown that several mathematical paradoxes reduce to connectedness questions in an appropriate space divided by the relevant branch cuts. This is an area of mathematics which is notoriously difficult to get right by hand, and mathematicians, and software packages, often have internal inconsistencies when it comes to branch cuts.

The standard computational approach to connectedness, which has been suggested in motion planning since the early 1980s, is via a technique called cylindrical algebraic decomposition. This has historically been computed via a "bottom-up" approach: we first analyse one direction, say the x-axis, decomposing it into all the critical points and intermediate regions necessary, then we take each (x,y)-cylinder above each critical point or region, and decompose it, then each (x,y,z) above each of these regions, and so on. Not only does this sound tedious, but it is inevitably tedious - the investigators and others have shown that the problem is extremely difficult (doubly exponential in the number of dimensions).

Much of the time, notably in motion planning, we are not actually interested in the lower-dimensional components, since they would correspond to a motion with no degrees of freedom, rather like tightrope-walking. Recent Canadian developments have shown an alternative way of computing such decompositions via so-called triangular decompositions, and a 2010 paper (Moreno Maza in Canada + Davenport) has shown that the highest-dimensional components of a triangular decomposition can be computed in singly-exponential time. This therefore opens up the prospect, which we propose to investigate, of computing the highest-dimensional components of a cylindrical decomposition in singly-exponential time, which would be a major breakthrough in computational geometry.

Connectedness in mathematical spaces is also important. The square root of 4 can be either 2 or -2: we have to decide which. Similarly, the square root of 9 can be 3 or -3. But, if 4 is connected to 9 in our problem space (whatever that is), we can't make these choices independently: our choice has to be consistent along the path from 4 to 9. When it is impossible to make such decisions totally consistently, we have what mathematicians call a `branch cut' - the classic example being the International Date Line, because it is impossible to assign `day' consistently round a globe. In previous work, we have shown that several mathematical paradoxes reduce to connectedness questions in an appropriate space divided by the relevant branch cuts. This is an area of mathematics which is notoriously difficult to get right by hand, and mathematicians, and software packages, often have internal inconsistencies when it comes to branch cuts.

The standard computational approach to connectedness, which has been suggested in motion planning since the early 1980s, is via a technique called cylindrical algebraic decomposition. This has historically been computed via a "bottom-up" approach: we first analyse one direction, say the x-axis, decomposing it into all the critical points and intermediate regions necessary, then we take each (x,y)-cylinder above each critical point or region, and decompose it, then each (x,y,z) above each of these regions, and so on. Not only does this sound tedious, but it is inevitably tedious - the investigators and others have shown that the problem is extremely difficult (doubly exponential in the number of dimensions).

Much of the time, notably in motion planning, we are not actually interested in the lower-dimensional components, since they would correspond to a motion with no degrees of freedom, rather like tightrope-walking. Recent Canadian developments have shown an alternative way of computing such decompositions via so-called triangular decompositions, and a 2010 paper (Moreno Maza in Canada + Davenport) has shown that the highest-dimensional components of a triangular decomposition can be computed in singly-exponential time. This therefore opens up the prospect, which we propose to investigate, of computing the highest-dimensional components of a cylindrical decomposition in singly-exponential time, which would be a major breakthrough in computational geometry.

### Planned Impact

Real geometry, i.e. the geometry of space as we perceive it without complex numbers, is vital to much of mathematics and many applications despite being less studied/taught (because it is harder?) than complex geometry. Solving problems in real geometry tends to lead to a lot of special cases (see (2) in the case for support), and is tricky to do by hand. Hence there are potentially many application areas for better algorithmic methods for real geometry and connectedness. In particular the question of interest is "connectedness within the reals": it is no good telling a robot to turn through an imaginary angle.

A) The theory of cylindrical algebraic decomposition was originally invented to solve the quantifier elimination problem: given a sentence containing "for all " or "there exists" clauses, produce an equivalent sentence without such clauses. Note that many sentences which appear not to contain such clauses in fact do: the [false over the reals] statement "sin is an invertible function" is really "for all y there exists an x such that y = sin(x)". Hence there are numerous applications in logic and computational mathematics which can benefit from better cylindrical algebraic decomposition: both in the U.K. and world-wide.

B) Motion planning for robots and similar devices such as automatically-steered cars, can be seen, as in [32], as "connectedness in configuration space", i.e. "can we get there from here", where "here" and "there" are configurations of the robot, rather than simply spatial points. This "configuration space" is typically of much higher dimension than one might expect: a rigid body in three-dimensional space is defined by three points, i.e. nine dimensions in all. Hence it is very important to have algorithms which behave efficiently as the number of dimensions grows, and this project should produce such algorithms. Motion planning is one of the areas we have worked on in the past [17], and we intend to pursue exemplar case studies ourselves, as well as disseminating our work via the IMRCs and appropriate conferences.The benefits of better motion planning are incalculable, ranging from better housework robots to the "Factory of the Future". Reconfiguring a "Factory of the Future" requires off-line motion planning, a "motion compiler", which would be a major gain: achievable via the use of the Maple software we will deliver. Further down the line one might envisage on-line motion planning, where our improvements in algorithmic performance would be even more significant.

C) Many mathematicians, and users of mathematics, have problems with apparently-simple function definitions. It is impossible to define 'square root' as a continuous function on the whole complex plane, since the argument of the square root of x is half the argument of x, and therefore the square root of 1 could be either 1 or -1, and neither choice is consistent with continuity. Hence one has to introduce 'branch cuts', and say that the definition is discontinuous as one crosses this cut. These cuts mean that many formulae are not in fact correct, either for special values ("log(1/x)=-log(x)" is not true when x=-1), or in much of the complex plane ("sqrt(x**2-1)=sqrt(x-1)sqrt(x+1)" is only 50% true). The Bath team [1-8] have realised that this is a question of connectivity of the complement of the branch cuts. This has been implemented, and provides a much better (guaranteed never to state that an incorrect identity is true) simplification algorithm than previous ones. However, it is limited by the connectivity question, and the breakthrough envisaged in this project will make the connectivity approach to simplification much more feasible. Maplesoft (see letter of support) would be very interested in this, and where one leading vendor goes, others will follow.

All categories of users will benefit from our twin-track approach of scientific publication and software dissemination via the world-wide Maple computer algebra system.

A) The theory of cylindrical algebraic decomposition was originally invented to solve the quantifier elimination problem: given a sentence containing "for all " or "there exists" clauses, produce an equivalent sentence without such clauses. Note that many sentences which appear not to contain such clauses in fact do: the [false over the reals] statement "sin is an invertible function" is really "for all y there exists an x such that y = sin(x)". Hence there are numerous applications in logic and computational mathematics which can benefit from better cylindrical algebraic decomposition: both in the U.K. and world-wide.

B) Motion planning for robots and similar devices such as automatically-steered cars, can be seen, as in [32], as "connectedness in configuration space", i.e. "can we get there from here", where "here" and "there" are configurations of the robot, rather than simply spatial points. This "configuration space" is typically of much higher dimension than one might expect: a rigid body in three-dimensional space is defined by three points, i.e. nine dimensions in all. Hence it is very important to have algorithms which behave efficiently as the number of dimensions grows, and this project should produce such algorithms. Motion planning is one of the areas we have worked on in the past [17], and we intend to pursue exemplar case studies ourselves, as well as disseminating our work via the IMRCs and appropriate conferences.The benefits of better motion planning are incalculable, ranging from better housework robots to the "Factory of the Future". Reconfiguring a "Factory of the Future" requires off-line motion planning, a "motion compiler", which would be a major gain: achievable via the use of the Maple software we will deliver. Further down the line one might envisage on-line motion planning, where our improvements in algorithmic performance would be even more significant.

C) Many mathematicians, and users of mathematics, have problems with apparently-simple function definitions. It is impossible to define 'square root' as a continuous function on the whole complex plane, since the argument of the square root of x is half the argument of x, and therefore the square root of 1 could be either 1 or -1, and neither choice is consistent with continuity. Hence one has to introduce 'branch cuts', and say that the definition is discontinuous as one crosses this cut. These cuts mean that many formulae are not in fact correct, either for special values ("log(1/x)=-log(x)" is not true when x=-1), or in much of the complex plane ("sqrt(x**2-1)=sqrt(x-1)sqrt(x+1)" is only 50% true). The Bath team [1-8] have realised that this is a question of connectivity of the complement of the branch cuts. This has been implemented, and provides a much better (guaranteed never to state that an incorrect identity is true) simplification algorithm than previous ones. However, it is limited by the connectivity question, and the breakthrough envisaged in this project will make the connectivity approach to simplification much more feasible. Maplesoft (see letter of support) would be very interested in this, and where one leading vendor goes, others will follow.

All categories of users will benefit from our twin-track approach of scientific publication and software dissemination via the world-wide Maple computer algebra system.

### Organisations

- University of Bath, United Kingdom (Lead Research Organisation)
- Western University (Collaboration)
- Coventry University, United Kingdom (Collaboration)
- University of Oxford, United Kingdom (Collaboration)
- University of Edinburgh, United Kingdom (Collaboration)
- Johannes Kepler University, Austria (Collaboration)
- Max Planck Society (Collaboration)
- Fondazione Bruno Kessler (Collaboration)
- RWTH Aachen University, Germany (Collaboration)
- Maplesoft, Canada (Collaboration, Project Partner)
- University of Cambridge, United Kingdom (Collaboration)
- Chinese Academy of Sciences (Collaboration)
- University of Genoa, Italy (Collaboration)
- Macquarie University, Australia (Collaboration)
- University of Cantabria, Spain (Collaboration)
- National Center for Scientific Research (Centre National de la Recherche Scientifique CNRS) (Collaboration)
- University of Kassel, Germany (Collaboration)
- University of Coimbra, Portugal (Collaboration)
- Beihang University (Collaboration)

### Publications

Bradford R
(2014)

*Computer Algebra in Scientific Computing*
Bradford R
(2013)

*Intelligent Computer Mathematics*
Bradford R
(2016)

*Truth table invariant cylindrical algebraic decomposition*in Journal of Symbolic Computation
Bradford R
(2020)

*Identifying the parametric occurrence of multiple steady states for some biological networks*in Journal of Symbolic Computation
Campbell J.A. Et Al (eds)
(2012)

*Speeding Up Cylindrical Algebraic Decomposition by Gröbner Bases*
Carette, J., Aspinall, D., Lange, C., Sojka, P. And Windsteiger, W. (eds)
(2013)

*Understanding Branch Cuts of Expressions*
Davenport J
(2019)

*Regular cylindrical algebraic decomposition*in Journal of the London Mathematical Society
Davenport J
(2016)

*Mathematical Software - ICMS 2016*
Davenport J
(2019)

*Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements Intelligent Geometry Tools*in Electronic Proceedings in Theoretical Computer Science
Davenport J
(2019)

*Symbolic computation and satisfiability checking*in Journal of Symbolic ComputationDescription | Cylindrical Algebraic Decomposition is a powerful tool for solving problems involving (polynomial) equalities and inequalities, e.g. x^2+y^2- 1=0 and x^2+(y-1)^2-1=0. But the standard technique for Cylindrical Algebraic Decomposition just considers the polynomials, x^2+y^2-1 and x^2+(y-1)^2-1, builds a data structure that can answer all questions about these polynomials, and then looks at the precise question. We have made a variety of improvements which say that considering the logical structure of the problem, in this case an AND of two EQUATIONS, allows for much simpler solution methods. |

Exploitation Route | Cylindrical Algebraic Decomposition is used in various areas of software, and, theoretically, in robot motion planning. These speedups should enable the solution of previously intractable problems. Indeed, we have subsequently applied these insights to problems in systems biology, and in economics. |

Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software) |

URL | http://staff.bath.ac.uk/masjhd/Triangular |

Description | Some of the technology developed in this project has been taken up by Maplesoft (a partner on the project) in Maple 17 and later releases, and formed a REF 2014 Impact Case study. This research is also used in the Japanese Todai robot project. Maplesoft have subsequenctly funded a CASE studentship at Bath to continue the partnership & further developments. This research also led to the Davenport/England/Mulligan collaboration on economic uses of CAD. |

First Year Of Impact | 2015 |

Sector | Digital/Communication/Information Technologies (including Software),Education |

Impact Types | Societal,Economic |

Description | CASE studentship |

Amount | £50,000 (GBP) |

Organisation | Engineering and Physical Sciences Research Council (EPSRC) |

Sector | Public |

Country | United Kingdom |

Start | 10/2017 |

End | 09/2021 |

Description | Impact Acceleration Account |

Amount | £5,000 (GBP) |

Organisation | Engineering and Physical Sciences Research Council (EPSRC) |

Sector | Public |

Country | United Kingdom |

Start | 07/2013 |

End | 09/2015 |

Description | Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition |

Amount | £497,465 (GBP) |

Funding ID | EP/T015748/1 |

Organisation | Engineering and Physical Sciences Research Council (EPSRC) |

Sector | Public |

Country | United Kingdom |

Start | 07/2020 |

End | 10/2024 |

Description | SC-square - Satisfiability Checking and Symbolic Computation: uniting two communities to solve real problems |

Amount | € 500,000 (EUR) |

Funding ID | 712689 |

Organisation | European Commission |

Sector | Public |

Country | European Union (EU) |

Start | 07/2016 |

End | 08/2018 |

Title | CAD Example Bank |

Description | A collection of machine-readable examples for cylindrical algebraic decomposition |

Type Of Material | Database/Collection of data |

Year Produced | 2012 |

Provided To Others? | Yes |

Impact | Citations by other users |

URL | http://opus.bath.ac.uk/29503 |

Title | Dataset supporting the paper: Improving the use of equational constraints in cylindrical algebraic decomposition |

Description | The files in this dataset support the following paper: ########################################################################################## Improving the use of equational constraints in cylindrical algebraic decomposition Matthew England, Russell Bradford and James H. Davenport. University of Bath http://opus.bath.ac.uk/42451/ ########################################################################################## Please find included the following: ############################## 1a) A Maple worksheet: EBD15-Section2Example-Maple.mw 1b) A pdf printout of the worksheet: EBD15-Section2Example-Maple.pdf 1c) A Maple Library file: ProjectionCAD.mpl These files detail the examples in Section 2 of the paper run in Maple. To run the Maple worksheet you will need a copy of the commercial computer algebra software Maple. This is currently available from: http://www.maplesoft.com/products/maple/ The examples were run in Maple 18 (released Spring 2014). It is likely that the same results would be obtained in Maple 17 and 16 as well as future versions of Maple, but this cannot be guaranteed. An additional code package, developed at the University of Bath, is required. To use it we need to read the Maple Library file as follows: > read("ProjectionCAD.mpl") > with(ProjectionCAD) More details on this Maple package are available in the technical report at http://opus.bath.ac.uk/43911/ and in the following publication: M. England, D. Wilson, R. Bradford and J.H. Davenport. Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting. Proc ICMS 2014 (LNCS 8593). DOI: 10.1007/978-3-662-44199-2_69 If you do not have a copy of Maple you can still read the pdf printout of the worksheet. ############################## 2) A zipped directory EBD15-Section2Example-Qepcad.zip Within this directory are files concerning those examples from Section 2 of the paper run in Qepcad-B. Qepcad-B is a free piece of software for Linux which can be obtained from: http://www.usna.edu/CS/qepcadweb/B/QEPCAD.html All the files in the zipped directory end in either "-in.txt" or "-out.txt". The former give input for Qepcad and the latter record output. Hence readers without access to Qepcad (e.g. on a Windows system) can still observe the output in the latter files. To verify the output readers should use the following bash command to run a Qepcad input file "Ex-in.txt" and record the output in "Ex-out.txt". qepcad +N500000000 +L200000 < Ex-in.txt > Ex-out.txt ############################## 3a) A Maple worksheet: EBD15-Section4Example-NewApproach.mw 3b) A pdf printout of the worksheet: EBD15-Section4Example-NewApproach.pdf Concerns the example in Section 4 solved using the new ideas of this paper. See notes for files (1) above. ############################## 4) A zipped directory EBD15-Section4Example-Qepcad.zip Concerns the example in Section 4 when solved with Qepcad. See notes for files (2) above. To run all tests at once use the bash script "RunAll.sh". ############################## 5) A zipped directory EBD15-Section4Example-OtherMaple.zip These files concern the other CAD implementations in Maple for the example in Section 4. These are: - Sign-invariant CAD by our own package ProjectionCAD. - Sign-invariant CAD by the RegularChains package (two variants) - CAD using single EC (four variants) in our own package. - CAD using multiple ECs in Regular Chains. The folder contains text files for running the maple code for each of these. An individual one can be executed in command line via > maple < FileName.txt > output.txt To run all tests at once use the bash script "RunTests.sh". ############################## The very last experiment detailed in (5) was also run in the Development Version of Maple giving a different result, as we reported in the paper. The Development Version of Maple is not publicly available. However, it is likely the new algorithm within will be available in the next public Maple release. |

Type Of Material | Database/Collection of data |

Year Produced | 2015 |

Provided To Others? | Yes |

Title | Dataset supporting the paper: Truth table invariant cylindrical algebraic decomposition |

Description | The files in this data set support the following paper: ########################################################################################## Truth table invariant cylindrical algebraic decomposition. Russel Bradford, James H. Davenport, Matthew England, Scott McCallum and David Wilson. http://opus.bath.ac.uk/38146/ ########################################################################################## Please find included the following: ############################## 1a) A Maple worksheet: Section1to7-Maple.mw 1b) A pdf printout of the worksheet: Section1to7-Maple.pdf 1c) A Maple Library file: ProjectionCAD.mpl These files concern the Maple results for the worked examples throughout Sections 1-7 of the paper. To run the Maple worksheet you will need a copy of the commercial computer algebra software Maple. This is currently available from: http://www.maplesoft.com/products/maple/ The examples were run in Maple 16 (released Spring 2012). It is likely that the same results would be obtained in Maple 17, 18, 2015 and future versions, but this cannot be guaranteed. An additional code package, developed at the University of Bath, is required. To use it we need to read the Maple Library file within Maple as follows: >>> read("ProjectionCAD.mpl"): >>> with(ProjectionCAD): More details on this Maple package are available in the technical report at http://opus.bath.ac.uk/43911/ and in the following publication: M. England, D. Wilson, R. Bradford and J.H. Davenport. Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting. Proc ICMS 2014 (LNCS 8593). DOI: 10.1007/978-3-662-44199-2_69 If you do not have a copy of Maple you can still read the pdf printout of the worksheet. ############################## 2) A zipped directory WorkedExamples-Qepcad.zip This directory also concerns the worked examples from Sections 1-7 of the paper, this time when studied with Qepcad-B. Qepcad-B is a free piece of software for Linux which can be obtained from: http://www.usna.edu/CS/qepcadweb/B/QEPCAD.html All the files in the zipped directory end in either "-in.txt" or "-out.txt". The former give input for Qepcad and the latter record output. Hence readers without access to Qepcad (e.g. on a Windows system) can still observe the output in the latter files. To verify the output readers should use the following bash command to run a Qepcad input file "Ex-in.txt" and record the output in "Ex-out.txt". >>> qepcad +N500000000 +L200000 < Ex-in.txt > Ex-out.txt Windows users without Linux access can still read the existing output files in the folder. ############################## 3a) The text file: Section82-ExampleSet.txt 3b) A Maple worksheet: Section82-ExampleSet.mw 3b) A pdf printout of the worksheet: Section82-ExampleSet.pdf The textfile defines the example set which is the subject of the experiments in Section 8.2, whose results were summarised in Table 2. Within the file the 29 examples are defined in the following syntax: (a) First a line starting with "#" giving the full example name followed in brackets by the shortened name used in Table 2. (b) Then a second line in which the example is defined as a list of two sublists: i) The first sublist defines the polynomials used. They are sorted into further lists, one for each formulae in the example. Each of these has two entries: --- The first is either a polynomial defining an equational constraint (EC); a list of polynomials defining multiple ECs; or an empty list (signalling no ECs). --- The second is a list of any non ECs. ii) The second sublist is the variable ordering from highest (eliminate first in projection) to lowest. Note that Maple algorithms use this order by Qepcad the reverse. This is the syntax used by the TTICAD algorithm that is the subject of the paper. The text file doubles as a Maple function definition. When read into Maple the command GenerateInput is defined which can provide the input in formats suitable for the three Maple algorithms tested. An example is given in the Maple worksheet / pdf. We note that the timings reported in the paper were from running Maple in command line mode. See also the notes for files (1) above. The same example set was tested in Qepcad. Here explicit ECs for a parent formula were entered in dynamically as products of the individual sub-formulae ECs, in cases where an explicit EC exists. See also Qepcad notes for file (2) above. Finally, the example set was also tested in Mathematica. Mathematica's CAD command does not return cell counts - these were obtained upon request to a Mathematica developer. Hence they are not recreatable using the information here (something outside the control of the present authors). ############################## 4a) A Maple worksheet: Section83-Maple.mw 4b) A pdf printout of the worksheet: Section83-Maple.pdf This shows how the numbers in Table 3 from Maple were obtained. See also notes for files (1) above. ############################## 5a) A zipped directory Section83-Qepcad.zipped This shows how the numbers in Table 3 from Qepcad were obtained. See also notes for file (2) above. |

Type Of Material | Database/Collection of data |

Year Produced | 2015 |

Provided To Others? | Yes |

Title | Real Geometry and Connectedness via Triangular Description: CAD Example Bank |

Description | A PDF file which lists the examples, their properties and their source; A text file for Maple which is designed to be read by Maple for easy access to the examples; A text file for QEPCAD from which examples can be easily copied for input into QEPCAD. |

Type Of Material | Database/Collection of data |

Year Produced | 2013 |

Provided To Others? | Yes |

Title | Zenodo-SYNASC-learn |

Description | Dataset supporting the paper: Z. Huang, M. England, J.H. Davenport and L.C. Paulson Using Machine Learning to decide when to Precondition Cylindrical Algebraic Decomposition with Groebner Bases. Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC '16), pp. 45--52. IEEE, 2016. Digital Object Identifier: 10.1109/SYNASC.2016.020 |

Type Of Material | Database/Collection of data |

Year Produced | 2017 |

Provided To Others? | Yes |

Impact | Paper published, follow-on being worked on |

URL | https://zenodo.org/record/343885#.WMbt9PmLSCg |

Description | Branch Cuts Technology in Maple 17 |

Organisation | Maplesoft |

Country | Canada |

Sector | Private |

PI Contribution | Collaborated with Maplesoft (company) to include our work in their commerical products. We developed theory and implemented algorithm to calculate branch cuts of mathematical functions. This work was then incorporated into Maplesoft's commercial products (with them inputting significant staff time and expertise to ensure the successful completion). This will ensure the maximum impact of our work as Maple is widely used in both academia and industry worldwide. |

Start Year | 2012 |

Description | Cylindrical Algebraic Decomposition via Regular Chains |

Organisation | Chinese Academy of Sciences |

Department | Chongqing Key Laboratory of Automated Reasoning and Cognition Center |

Country | China |

Sector | Private |

PI Contribution | Theory and software collaboration leading to publication (in preparation). Includes collaborations with colleagues in Canada and China. Joint academic work combining two breakthroughs in the field to build a state of the art system. |

Collaborator Contribution | Though the collaboration started before the funding, and indeed contributed to the award of the funding, the funding strengthened and deepened the collaboration. In particular, when Changbo Chen moved to Chongqing, we maintained the collaboration. |

Impact | The joint papers with Marc MM and Changbo Chen listed. |

Start Year | 2009 |

Description | Cylindrical Algebraic Decomposition via Regular Chains |

Organisation | Western University |

Country | Canada |

Sector | Academic/University |

PI Contribution | Theory and software collaboration leading to publication (in preparation). Includes collaborations with colleagues in Canada and China. Joint academic work combining two breakthroughs in the field to build a state of the art system. |

Collaborator Contribution | Though the collaboration started before the funding, and indeed contributed to the award of the funding, the funding strengthened and deepened the collaboration. In particular, when Changbo Chen moved to Chongqing, we maintained the collaboration. |

Impact | The joint papers with Marc MM and Changbo Chen listed. |

Start Year | 2009 |

Description | Cylindrical Algebraic Decomposition via Regular Chains (2) |

Organisation | Chinese Academy of Sciences |

Department | Chongqing Institute of Green and Intelligent Technology (CIGIT) |

Country | China |

Sector | Academic/University |

PI Contribution | See (1). |

Start Year | 2013 |

Description | Intelligent Geometry Tools |

Organisation | Beihang University |

Country | China |

Sector | Academic/University |

PI Contribution | Expertise in cylundrical algebraic decomposition, and "without loss of generality" |

Collaborator Contribution | Expertise in geometric theorem proving and pedagogy |

Impact | Paper "Intelligent Geometry Tools"; COST application. |

Start Year | 2017 |

Description | Intelligent Geometry Tools |

Organisation | University of Cantabria |

Country | Spain |

Sector | Academic/University |

PI Contribution | Expertise in cylundrical algebraic decomposition, and "without loss of generality" |

Collaborator Contribution | Expertise in geometric theorem proving and pedagogy |

Impact | Paper "Intelligent Geometry Tools"; COST application. |

Start Year | 2017 |

Description | Intelligent Geometry Tools |

Organisation | University of Coimbra |

Country | Portugal |

Sector | Academic/University |

PI Contribution | Expertise in cylundrical algebraic decomposition, and "without loss of generality" |

Collaborator Contribution | Expertise in geometric theorem proving and pedagogy |

Impact | Paper "Intelligent Geometry Tools"; COST application. |

Start Year | 2017 |

Description | Intelligent Geometry Tools |

Organisation | University of Edinburgh |

Country | United Kingdom |

Sector | Academic/University |

PI Contribution | Expertise in cylundrical algebraic decomposition, and "without loss of generality" |

Collaborator Contribution | Expertise in geometric theorem proving and pedagogy |

Impact | Paper "Intelligent Geometry Tools"; COST application. |

Start Year | 2017 |

Description | Machine Learning in Cylindrical Algebraic Decomposition |

Organisation | University of Cambridge |

Department | Computer Laboratory |

Country | United Kingdom |

Sector | Academic/University |

PI Contribution | We brought an understanding of cylindrical algebraic decomposition technology, and the numerous choices involved in using it, and the features driving those choices. |

Collaborator Contribution | Cambridge brought a set of problems, and an understanding of how machine learning could be used in option selection IF one knew the features |

Impact | A comparison of three heuristics to choose variable ordering for cylindrical algebraic decomposition; Applying Machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition; |

Start Year | 2013 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | Coventry University |

Department | Centre for Research in Psychology, Behaviour and Achievement (PBA) |

Country | United Kingdom |

Sector | Academic/University |

PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. |

Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |

Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | Fondazione Bruno Kessler |

Country | Italy |

Sector | Private |

PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. |

Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |

Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | Johannes Kepler University of Linz |

Country | Austria |

Sector | Academic/University |

PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. |

Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |

Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | Maplesoft |

Country | Canada |

Sector | Private |

PI Contribution | |

Collaborator Contribution | |

Impact | |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | Max Planck Society |

Country | Germany |

Sector | Charity/Non Profit |

PI Contribution | |

Collaborator Contribution | |

Impact | |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | National Center for Scientific Research (Centre National de la Recherche Scientifique CNRS) |

Department | Lorraine Research Laboratory in Computer Science and its Applications (LORIA) |

Country | France |

Sector | Public |

PI Contribution | |

Collaborator Contribution | |

Impact | |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | RWTH Aachen University |

Department | Department of Computer Science |

Country | Germany |

Sector | Academic/University |

PI Contribution | |

Collaborator Contribution | |

Impact | |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | University of Genoa |

Country | Italy |

Sector | Academic/University |

PI Contribution | |

Collaborator Contribution | |

Impact | |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | University of Kassel |

Department | Institute of Mathematics |

Country | Germany |

Sector | Academic/University |

PI Contribution | |

Collaborator Contribution | |

Impact | |

Start Year | 2015 |

Description | Symbolic Computation and Satisfiability Checking |

Organisation | University of Oxford |

Department | Wellcome Trust Centre for Human Genetics |

Country | United Kingdom |

Sector | Charity/Non Profit |

PI Contribution | |

Collaborator Contribution | |

Impact | |

Start Year | 2015 |

Description | Truth Table Invariant Cylindrical Algebraic Decomposition Collaboration |

Organisation | Macquarie University |

Country | Australia |

Sector | Academic/University |

PI Contribution | Developed new problem statement and algorithmic solution for CAD. Joined up with a leading developer of CAD theory (who came for a 6 week research visit) to build a new algorithm making use of structure in the problem for more efficient solutions. |

Start Year | 2012 |

Title | ProjectionCAD |

Description | A collection of many algorithms (new and old) for CAD, implemented as a Maple package. Open source code, available freely online together with introductory guide and technical reports detailing implementation and theoretical findings which followed. |

Type Of Technology | Software |

Year Produced | 2013 |

Open Source License? | Yes |

Impact | Use in subsequent publications, inspired new developments in Maple |

URL | http://opus.bath.ac.uk/35636 |