project . 2021 - 2025 . On going

Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

UK Research and Innovation
  • Funder: UK Research and InnovationProject code: EP/T015748/1
  • Funded under: EPSRC Funder Contribution: 421,950 GBP
  • Status: On going
  • Start Date
    01 Jan 2021
    End Date
    30 Mar 2025
Description
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" ...
Description
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" ...
Any information missing or wrong?Report an Issue