VTS and Lazard Projection CAD in Quantifier Elimination with Maple
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 31 | |
| Author | 0000-0001-6019-1775 (ORCID) | |
| Contributors | 0000-0001-6019-1775 (ORCID) | |
| License | CC Attribution - NonCommercial - NoDerivatives 3.0 Germany: You are free to use, copy, distribute and transmit the work or content in unchanged form for any legal and non-commercial purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/48017 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language | ||
| Producer | 0000-0001-6019-1775 (ORCID) | |
| Production Year | 2020 | |
| Production Place | Bath, UK |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
| |
| Keywords |
8
11
17
21
00:00
QuantificationComputer-aided designAxonometric projectionGaussian eliminationComputerMIDICodeObject (grammar)Web pageUniverse (mathematics)Projektive GeometrieArchaeological field surveyPower (physics)Quantifier eliminationVirtualizationSoftware developerRule of inferencePhysical systemLocal ringXML
00:28
CodeQuantifier eliminationComputer-aided designReal numberSet (mathematics)System callQuantificationFocus (optics)PolygonAlgorithmProjektive GeometrieTask (computing)Point (geometry)Well-formed formulaComputer animation
01:05
Real numberQuantifier eliminationBoolean algebraOperator (mathematics)Well-formed formulaConstraint (mathematics)PolynomialRow (database)RecursionOperator (mathematics)Theory of relativityPolynomialWell-formed formulaConstraint (mathematics)XML
01:28
Real numberQuantifier eliminationOperator (mathematics)Boolean algebraVariable (mathematics)QuantificationWell-formed formulaConstraint (mathematics)PolynomialWell-formed formulaVariable (mathematics)Point (geometry)String (computer science)Gaussian eliminationOperator (mathematics)Computer animation
01:57
Quantifier eliminationQuantificationEquivalence relationWell-formed formulaReal numberGeometryAlgebraic numberVariable (mathematics)Gaussian eliminationWell-formed formulaPlanningQuantificationLinear algebraReal numberGeometryXML
02:30
Quantifier eliminationWell-formed formulaEquivalence relationAlgebraic numberGeometryNetwork topologyModulo (jargon)TheoryAlgorithmExtension (kinesiology)CASE <Informatik>Variable (mathematics)Real numberCodecSoftware frameworkFerry CorstenModul <Datentyp>Well-formed formulaInterpreter (computing)Modulo (jargon)TheoryComputer animationXML
03:01
Modulo (jargon)TheoryAlgorithmLinear algebraDatabaseDatabaseImage resolutionSoftware frameworkAlgorithmComputer animation
03:22
AlgorithmVirtual realityTerm (mathematics)Variable (mathematics)RecursionReal numberElectronic mailing listPoint (geometry)Substitute goodMultiplication signVariable (mathematics)Distribution (mathematics)VirtualizationHypermediaPairwise comparisonTerm (mathematics)Group actionAlgorithmExistential quantificationSource codeXML
04:18
AlgorithmTerm (mathematics)Virtual realityVariable (mathematics)RecursionDegree (graph theory)RootPolynomialRadical (chemistry)TheoryDegree (graph theory)Variable (mathematics)Limit (category theory)Physical lawHypermediaFreewareComputer animation
04:45
AlgorithmVirtual realityTerm (mathematics)Variable (mathematics)RecursionRootDegree (graph theory)PolynomialGroup actionRadical (chemistry)Degree (graph theory)Group actionHelmholtz decompositionWell-formed formulaComputer animation
05:14
AlgorithmComputer-aided designHelmholtz decompositionCylinder (geometry)Algebraic numberComplete metric spacePolynomialWell-formed formulaSpacetimeSensitivity analysisSpecial unitary groupVariable (mathematics)AreaMultiplication signDegree (graph theory)QuicksortNumber theoryImplementationStructural loadXMLComputer animation
05:46
AlgorithmComputer-aided designAlgebraic numberHelmholtz decompositionCylinder (geometry)PolynomialWell-formed formulaComplete metric spaceVariable (mathematics)GeometryoutputAxonometric projectionVariable (mathematics)SpacetimeGeometryoutputData structureBitProjektive GeometrieState of matterComputer-aided designWell-formed formulaNichtlineares GleichungssystemBoolean algebraComputer animation
06:19
Statement (computer science)Computer-aided designVariable (mathematics)Computer-aided designLimit (category theory)Degree (graph theory)Statement (computer science)System callGreedy algorithmVariable (mathematics)Computer chessQuantificationTerm (mathematics)Strategy gameBlock (periodic table)XMLComputer animation
06:43
Variable (mathematics)Term (mathematics)Variable (mathematics)Greedy algorithmBlock (periodic table)Strategy gameSource codeXML
07:07
Block (periodic table)Data structureForm (programming)Network topologyVariable (mathematics)QuantificationVertex (graph theory)QuicksortNetwork topologyQuantificationResultantVariable (mathematics)Data structureBlock (periodic table)Source codeXML
07:23
Data structureForm (programming)Block (periodic table)Network topologyVariable (mathematics)Vertex (graph theory)QuantificationRepresentation theoryPolynomialComputer-aided designAxiom of choiceForcing (mathematics)Variable (mathematics)Group actionAtomic numberLaptopAxiom of choiceNumber theoryQuantificationWell-formed formulaComputer iconDegree (graph theory)Block (periodic table)Computer-aided designEntire functionImplementation
08:09
Invariant (mathematics)Computer-aided designPolynomialNetwork topologyData structureForm (programming)Block (periodic table)Variable (mathematics)Vertex (graph theory)QuantificationRepresentation theoryAxiom of choicePolygonWell-formed formulaPolynomialComputer-aided designModal logicGroup actionContext awarenessArithmetic meanData structureSpacetimeQuicksortFrequencyComputer animation
08:44
Computer-aided designContext awarenessVariable (mathematics)QuicksortNetwork topologyArithmetic meanContext awarenessComputer-aided designTerm (mathematics)Level (video gaming)Variable (mathematics)Direction (geometry)WaveXML
09:30
PiAlgorithmComputer-aided designContext awarenessVariable (mathematics)Similarity (geometry)Vertex (graph theory)MassMilitary baseOrder (biology)Different (Kate Ryan album)Wave packetData structureSystem callProjektive GeometrieComputer virusComputer-aided designSimilarity (geometry)Polynomial
09:54
Computer-aided designElectric currentConstraint (mathematics)Context awarenessVariable (mathematics)Similarity (geometry)Vertex (graph theory)Axonometric projectionSound effectMilitary baseNichtlineares GleichungssystemConstraint (mathematics)Computer animation
10:13
Computer-aided designConstraint (mathematics)Sound effectContext awarenessVariable (mathematics)Vertex (graph theory)Similarity (geometry)Axonometric projectionPolygonoutputAdditionDifferenz <Mathematik>WordUsabilityProjektive GeometrieArithmetic meanAdditionPresentation of a groupNetwork topologyDifferenz <Mathematik>Well-formed formulaComputer animationXML
10:51
AdditionDifferenz <Mathematik>outputComputer-aided designPresentation of a groupAlgorithmNetwork topologyHybrid computerPolygonContext awarenessNetwork topologyContext awarenessPresentation of a groupComputer-aided designCodecSoftware frameworkComputer animation
11:15
Partial derivativeComputer-aided designWell-formed formulaOffice suiteWell-formed formulaQuantifier eliminationComputer-aided designQuantificationSet (mathematics)PolynomialSource codeXML
11:45
Object-oriented programmingComputer-aided designPartial derivativeWell-formed formulaNetwork topologyFunction (mathematics)QuantificationFunction (mathematics)BitForm (programming)Object (grammar)Task (computing)Term (mathematics)QuantificationBarrelled spaceFunctional (mathematics)Network topologyChemical equationWell-formed formulaNichtlineares GleichungssystemoutputComputer animation
12:22
Constraint (mathematics)Axonometric projectionComputer-aided designWell-formed formulaoutputPolynomialOperator (mathematics)Connected spaceWave packetNichtlineares GleichungssystemWell-formed formulaQuicksortConstraint (mathematics)Level (video gaming)Computer architectureSign (mathematics)Number theoryProjektive GeometrieGeometryPolynomialInvariant (mathematics)XMLComputer animation
12:56
Constraint (mathematics)Axonometric projectionComputer-aided designWell-formed formulaoutputPolynomialOperator (mathematics)Default (computer science)Nichtlineares GleichungssystemProjektive GeometrieMultiplicationComputer configurationSingle-precision floating-point formatMilitary baseConstraint (mathematics)Process (computing)PropagatorRight angleMoment (mathematics)Wave packetDiscrete groupComputer animation
13:44
Constraint (mathematics)TriangleSystem programmingPhysical systemPhase transitionAxonometric projectionProduct (business)Variable (mathematics)Nichtlineares GleichungssystemConstraint (mathematics)Projektive GeometrieMultiplicationPhase transitionCASE <Informatik>Variable (mathematics)Product (business)Network topologyDivisorPropagatorMoment (mathematics)Military baseSource codeXML
14:09
Constraint (mathematics)TriangleSystem programmingPhysical systemProduct (business)ResultantAxonometric projectionPhase transitionVariable (mathematics)GeometryInterrupt <Informatik>RootFaktorenanalyseNichtlineares GleichungssystemConstraint (mathematics)GeometryPropagatorIdeal (ethics)RootMilitary baseQuicksortInformationComputer animation
14:26
Constraint (mathematics)Variable (mathematics)Axonometric projectionImplementationGaussian eliminationHeuristicOrder (biology)Factory (trading post)AdditionMultiplicationQuantumNichtlineares GleichungssystemProjektive GeometrieConstraint (mathematics)TheoryCASE <Informatik>Row (database)XMLComputer animation
15:03
Constraint (mathematics)Variable (mathematics)HeuristicAxonometric projectionSound effectNichtlineares GleichungssystemHeuristicBitSound effectPolynomialConstraint (mathematics)Multiplication signDivisorProjektive GeometrieVariable (mathematics)FreewareKey (cryptography)Real numberWell-formed formulaExtension (kinesiology)Computer animation
15:38
Equivalence relationQuantificationWell-formed formulaNumber theoryVariable (mathematics)Well-formed formulaReal numberEquivalence relationVariable (mathematics)
16:07
Equivalence relationQuantificationWell-formed formulaNumber theoryVariable (mathematics)AlgorithmProcess (computing)Process (computing)Form (programming)AlgorithmVideo gameLatent heatSpeech synthesisSoftware frameworkComputer-aided designWell-formed formulaDreiecksmatrix
16:27
Well-formed formulaEquivalence relationQuantificationVariable (mathematics)Number theoryAlgorithmPolygonPresentation of a groupProcess (computing)Computer-aided designComputer-aided designPolygonSet (mathematics)AlgorithmLine (geometry)Object (grammar)Computer animation
16:51
Constraint (mathematics)Axonometric projectionProjektive GeometrieConstraint (mathematics)Computer-aided designContext awarenessCellular automatonNetwork socketHelmholtz decompositionUniform resource locatorThomas BayesPhysical lawPressureOcean currentSpacetimeDecision theorySource code
17:23
Axonometric projectionConstraint (mathematics)Helmholtz decompositionCellular automatonDifferent (Kate Ryan album)Helmholtz decompositionSet (mathematics)Constraint (mathematics)Cellular automatonComputer-aided designContext awarenessPresentation of a groupAlgorithmQuantifier eliminationThomas BayesAdditionComputer animation
18:13
Computer-aided designPartial derivativeConstraint (mathematics)Axonometric projectionHelmholtz decompositionCellular automatonStack (abstract data type)Cellular automatonConstructor (object-oriented programming)Term (mathematics)Context awarenessPartial derivativeComputer animation
18:34
Computer-aided designPartial derivativeConstraint (mathematics)Axonometric projectionHelmholtz decompositionCellular automatonStack (abstract data type)AlgorithmBitComputer-aided designComputer animation
18:51
Electronic mailing listSoftwareMultiplication signGaussian eliminationProjektive GeometrieView (database)PlastikkarteQuantifier eliminationCodeSharewareTerm (mathematics)Source codeXML
19:13
Well-formed formulaWell-formed formulaImplementationMultiplication signWorkstation <Musikinstrument>Projektive GeometrieSource codeXML
19:46
Well-formed formulaComputer-aided designSoftware developerSoftwareTerm (mathematics)Mathematical analysisBitBenchmarkProper mapSource codeXML
20:04
Well-formed formulaComputer-aided designBenchmarkOffice suitePolygonAlgorithmImplementationComputer-aided designComputer animation
20:21
Well-formed formulaComputer-aided designFeedbackExtension (kinesiology)Projektive GeometrieQuicksortNumbering schemeFormal grammarAreaGaussian eliminationCovering spaceBit rateOnline helpImplementationVector potentialFeedbackTerm (mathematics)Well-formed formulaQuantificationComputer-aided designComputer animation
Transcript: English(auto-generated)
00:01
Okay, hello everybody and welcome to this virtual talk at ICMS 2020. My name is Zach Tonks from University of Bath and you're watching VTS and ZAR Projection CAD in Quantifier Elimination with Maple. So getting right into it, this talk is largely a very, very top-down overview of everything in my PhD project, supervised by James Davenport, also the University of Bath, also very
00:21
integrated within ICMS, and the co-development of which there's a lot is supported and supervised by Maplesoft, which I'm very grateful for. Largely, the project is development of the package Quantifier Elimination in Maple, consisting of a set of tools for Quantifier Elimination, which I'll call QEE over REALS. So the main purpose of this project is to congregate a lot of contemporary research on VTS and CAD,
00:45
mostly with respect to CAD, of which there are some new features from fairly current research and introduces some new ideas for both of these, and in particular, there's a very big focus on a main idea, which is to do with interplay between VTS and CAD, call this poly algorithm to do QEE.
01:06
So getting right into what QEE is, I'm going to call a tasky formula, a polynomial constraint F row 0, where I can have less or fewer, less or more of these relation operators, and then, or it's going to be a Boolean formula using the operators and, or, or, implies, etc. of these polynomial constraints, or of other tasky formulae recursively.
01:28
And then a quantified tasky formula is one where any sub-formula can have quantified variables, so for all x or variables y are allowable at any point in this formula. But most importantly, a pre and x formula is one where you have a string of quantified variables
01:46
preceding a unquantified formula only featuring and, or, or as operators. And so there's going to be m of these quantified variables amongst n variables. And then quantifier elimination is unsurprisingly to eliminate all the quantified variables
02:02
from this pre and x formula to obtain a quantifier-free formula, which is going to be in remaining n minus m variables. If there are m, if there are n quantified variables, then this will certainly be equivalent to true or false. Otherwise, it may be any other quantifier-free formula in x1 through xn minus m. And these QE problems
02:23
crop up in various places in real algebraic geometry. We've seen them from economics, motion planning, and AI. In particular, we had some work in economics where these are fully quantified problems, fully existential usually, completely quadratic or linear in the quantified variables, usually, which is a special case, certainly with respect to the algorithms.
02:47
SMT, satisfiability modulo theory over the theory of real arithmetic, you can informally interpret SMT problems as fully existentially quantified tasky formulae problems, sorry, QE problems.
03:01
And otherwise, QE algorithms with incrementality are useful in SMT frameworks. Such that you can solve SMT problems completely incrementally is usually how they do things. An important database of SMT problems is SMTlib, where they have their own format, SMT2. So I've been using this database myself.
03:23
So getting into the two main algorithms for QE, which is not a comprehensive list of algorithms for QE, but for me is VTS and CAD. So VTS is virtual term substitution. The term virtual comes from the fact that you are not necessarily substituting real numbers at any one point during this algorithm. You substitute virtual substitution points, which may be substitution points in other quantified variables,
03:44
and potentially with infinitesimals, which I'm not going to go into in great detail. But this does mean that it's entirely symbolic and quite concise, especially in comparison to the other algorithms, CAD, which I'll talk about. It's largely completely ignorant of unquantified variables. It doesn't mind too much. It is recursive in some sense. So basically the action of VTS, so distribution of an existential quantifier into a conjunction,
04:07
will spawn a bunch of other intermediate QE problems that you can then propagate VTS on, for example. So it can be viewed as recursive, which is a particularly nuance. But the main drawback is that it's degree limited.
04:21
So we can only act upon quantified variables that are appearing in theory of up to degree five, but right now up to degree three via work from Maricosta, which I've paid close attention to when I was implementing this. So we can only really right now eliminate variables appearing of degree three or less.
04:45
And worse, action of VTS can actually increase the degree of intermediate formulae. So it being low degree to start with, so a quantified variable appearing in low degree to start with is not a guarantee that VTS can complete the QE alone.
05:00
Given if you eliminate something appearing quadratically, then you may double the degree of the formulae that you gain. Hence, you can no longer use VTS anymore if you can't factor those. So moving on towards CAD, which is cylindrical algebraic decomposition. It's entirely complete, so it doesn't care about degree. If given enough time, then it will complete QE for your formula.
05:26
It's very often implemented, so there's a load of competitive implementations in and outside of Maple in particular. There's a lot of ongoing research on it in various areas. And even the implementations can differ between implementations, despite the same sort of underlying technology.
05:47
It's very sensitive to the number of variables, including those that are unquantified. So even if you have a lot of unquantified variables in your formula, you still need to construct, you still need to work in space for those unquantified variables, which is unfortunate. And it can easily be led astray via spurious geometry irrelevant to your input problem.
06:07
So it's a bit of a sledgehammer. A lot of the Boolean structure of your formula is lost as soon as you go into CAD bar things like equational constraints, which you'll go into. This is especially true of projection CAD, projection lifting. So the mission statement really for my PhD was, can I hybridise between VTS and CAD
06:24
and potentially anything else, such that each is used in a way to mitigate the other's shortcomings. So in particular, VTS's shortcomings are that it is degree limited. So I have a hard stop as soon as I get something of degree four, which I can't factor. So can I use CAD intelligently to overcome these degree limitations?
06:43
And the answer is, I hope yes. So the idea is to use VTS as far as possible, commuting similarly quantified variables in any one block of quantifiers, which is all you can do in terms of variable strategy, to eliminate variables of least degree first. So in particular, I deploy a greedy variable strategy in terms of
07:01
trying to eliminate linear variables appearing linearly first, tie breaking with quadratic, etc. And then you get sort of a tree structure having eliminated variables from any one block of quantifiers. So you can propagate VTS on these individual nodes, the QE problems that you get as a result of propagating VTS.
07:24
And in the last block of quantifiers in particular, in the last block of quantified variables, if all variables appear as degree four and I can't factor, then I'm forced to go into CAD. Other implementations would probably collapse the entire VTS formula into one formula for CAD to traverse.
07:42
So I give CAD another fully quantified problem. What I'm going to do instead is I'm going to use CAD in a choice of nodes, so a choice of one of the intermediate problems given to me by VTS. And that will be a problem in the fewest possible number of variables, in particular the fewest number of quantified variables, and hopefully the fewest number of atoms.
08:05
And potentially I can get a quantifier-free answer purely from that, else I'm going to use incremental CAD to solve the implicit QE problem for further nodes if necessary. So what I'm using here is that there's somewhat some conjecture here that all VTS nodes look similar due to
08:21
the action of VTS, so a lot of formulae given to me by VTS are going to look very similar. So then where they do look fairly similar, then that means that the polynomials basically be similar between these nodes, and in fact the brilliant structure, which is a particular boon of this, using this methodology, should be quite similar as well.
08:41
So then that's where incremental CAD should really help. So what I've been doing since I last was at conferences and sort of presenting this kind of work, is I was basically doing a canonicalisation that incremental CAD works very well in the context of VTS. We can use CAD in the deepest possible VTS node attained, meaning CAD in the fewest variables, including the
09:03
fewest quantified variables, and then I can prepend variables, and what that means is in particular prepend other quantified variables, so I can traverse the VTS tree depth-wise and actually go up to nodes of a lesser level, including further quantified variables, basically because VTS and CAD work in opposition in terms of directions, and if it wasn't this way, then this method wouldn't really work.
09:32
We also have a poly-share criteria, what I call a poly-share criteria, which is when I can actually reuse a CAD among similar nodes, and when I actually discard a CAD, because I wouldn't want to
09:41
use this master CAD idea on a node which looks completely dissimilar to one that I used CAD on before, because the polynomials are completely different, or the structure is completely different, so what does similar actually mean? Also, I've been doing stuff with equational constraints, again, via some work by my colleagues with
10:02
a Lazard projection, so equational constraints usually leads to Grubner bases as well for pre-processing. I've also been looking at variable orderings, especially with respect to CAD, in conjunction with equational constraints, and avoidance of something called Lazard curtains, which is from, again, my colleagues' work for this ICMS generally as well.
10:24
Which I'll be talking about later as well, so that's all linked to equational constraints as well. Also, in this project are evolutionary techniques. This is basically just a word that I use to encapsulate what would usually be called incremental from what other people use, because I use
10:43
evolutionary to mean incremental and decremental, meaning addition and subtraction, subformally from an original formula as well. I've got evolutionary VTS and CAD implemented, including a new presentation of this VTS, which I've presented before at SC2 last year, and this canonically extends to evolutionary techniques acting on a hybrid tree in the context of a polyagram.
11:06
So basically, both incremental and decremental VTS and CAD are there, especially if they could be used within an SMT framework or something like that. So the actual package quantifier elimination, implementing everything mentioned here, it offers standalone CAD for QE as
11:25
well, so you can do just purely partial CAD with no VTS on QE if you want. And it also offers stock CAD in the sense that it will provide you with the literal CAD for an unquantified formula or set of polynomials if you so want that.
11:41
So that's not doing any QE, that's just giving you literally the CAD if you want it. The whole package is largely object oriented, mainly because VTS and CAD work pretty much in terms of trees, so I thought that made quite a lot of sense. Hopefully it's designed to have very easy to use syntax in terms of input and output. I'm talking
12:01
about rich output there, I'll talk about that in terms of witnesses a little bit in a moment. And it also provides the sub-package quantifier tools, which is mainly there to make sense of tasky formulae a bit more. So what is an equation constraint, or if there's a function for giving you the prenex form of some formula or something like that.
12:23
So what are actual equation constraints, which I've been mentioning so much? So if you have a quantified formula, which is in particular a conjunction, then at the very least the equations in this conjunction, at the top level of this conjunction, are your equation constraints. So the idea of equation constraints in CAD first came about due to McCallum, who said we only need
12:43
to be sign invariant in the sections over at least one of the fi, which is going to result in fewer polynomials in projection via some restricted projection operators, which generally means less geometry due to fewer roots, etc. So here what we've done, I say what we've done, again, what my colleagues at Bath have done is for their interest in equation constraints in the Lazar projection.
13:05
So if you basically use this equation constraint work with respect to the Lazar projection, then you get some caveats, but tentatively in quantifier elimination, equation constraints with Lazar projection are implemented. And you can use single equation constraints or multiple equation constraints
13:23
and propagation, and this is all controllable via keyword options in Maple. So I just need to decide really on the default values of these options and stuff like that. But it's all there and we're investigating that, and I'll talk more to that in a moment as well. Naturally, when you're talking equations, you've also got Grabner bases.
13:40
So I do use Grabner bases to preprocess the equation constraints. I'm not going to go into this too much either, but basically the idea is I want to form triangular systems out of the equation constraints where I can to better cater to the projection phase when you do use multiple equation constraints. So this is all really conjecture, but I have the idea of taking a product monomial ordering on the
14:03
PLEX of the last K variables where you have K equation constraints in CAAD and TDAG on the rest, basically to replace propagation of equation constraints where that can result in some spurious roots and hence some geometry in CAAD which you don't really want. So using Grabner bases to really replace propagation of equation constraints in CAAD ideally.
14:24
So again, I won't go into this too much. But equation constraints are also all tied to variable orderings as well. So the CAAD in quantum theory of elimination so far seems to be very sensitive to variable ordering as most CAAD implementations are. In particular, it really seems to like the projection-based orderings.
14:42
So we're talking NDRR and SOTD, the orderings like that from previous works. They're in principle quite costly, requiring N factorial projections. But it really is worth trying to cater your projection and landing a really good projection when you have restricted projection, multiple equation constraints, stuff like that.
15:03
In addition to this, you've got the existing Brown heuristic which is a really cheap heuristic in order to get a variable ordering from. But I noticed that this doesn't really pay attention to equation constraints that much. So if you really do want to pay attention to equation constraints, then basically you can modify the Brown heuristic to apply those tiebreakers to equation constraints before any other polynomials first.
15:27
These have a really large effect on projection, presumably, so you may as well try to cater to them a bit more. So that's something very minor I did as well. I call that the EC heuristic. So moving on to witnesses for QE. So these are assignments of quantified variables to
15:43
real numbers that prove the equivalence of a quantified formula to its quantifier-free answer. So that means that if you have an existentially quantified formula, a fully existentially quantified formula, and then you get that it's satisfiable, so it's true, then you want the assignments to prove that it's true, at the very least.
16:00
And conversely, for a universally quantified formula, you want to know why it's unsatisfiable, so you get the assignment. So Costa had the idea for this, really. He created the whole framework for it. All I've really done is formalize this into an algorithm and present it as an algorithm previously. It requires a formula to be completely similarly quantified and completely traversed by VTS in general for this back substitution process.
16:27
But also I can concatenate witnesses from CAD with those from VTS to provide the missing witnesses that you would get from VTS when you use VTS and CAD together. And this is specific to using the poly algorithm because you can track any one CAD to exactly one VTS node such that you can do this.
16:46
So I can always get a full set of witnesses even when I don't use purely VTS, basically. So along the line, going back towards Equatial Constraints and CAD with the Lazard projection. Again, this is very relevant to the work in this ICMS from my colleagues, Akshar and James from Bath.
17:08
Lazard curtain is basically something like a nullification occurrence in the context of using the McCallum projection, but instead when using Restriction projections via Equatial Constraints in the Lazard projection.
17:21
So they've been talking about this and they've got some work on that. In that paper for this ICMS they have their own methodology of dealing with these curtain cells by doing extra decomposition on those cells where your Equatial Constraints are nullified. They provide an algorithm to do this. This is implemented within Quantifier Elimination. This is all very new and basically only just tested and seems to be working.
17:46
But I need to investigate it some more and get some more data on this. But it seems to work. The context for me of this decomposition is a little bit different because the original presentation for them, they provide a whole new CAD based on the sets gained from that.
18:02
I have to merge in a CAD and the new cells gained from this decomposition instead. But anyway, you should look at that work as well in his talk on this, obviously, if you haven't already. In addition, I can sort of proceed all this with some partial CAD methodology.
18:20
So any cell where stack construction failed for me, I can just set it aside until I know that it is completely necessary that I need that cell for deduction of a Quantifier-free answer in the context of QE. I can do this locally in the sense of a single CAD, but also in a global sense, in terms of a poly-algorithm, I can discard a whole CAD if I want, even if that would be completely costly.
18:45
So there's a whole lot of work here, so I'm extending a little bit on what they're doing with regards to the curtains there. And that's basically it. This has been a very fast top-down overview of everything in Quantifier Elimination and my PhD project.
19:00
I do have a software demo of this ICMS on Thursday, so obviously I can demonstrate the actual package a lot more there if you're interested, so please do come to that, virtually of course. So this is a to-do list of some things that are currently missing from the project, I guess, especially in terms of code and the package.
19:21
The simplification of formulae produced in VTS is very weak. As I say, VTS produces more quantified formulae throughout the usage of VTS, and the simplification is basically very weak compared to, I think, other implementations of VTS. I haven't really had time to look into it in this project yet. I know that some solutions to the
19:40
simplification of formulae do exist, so I'd like to see that make its way into the package sometime in the future. The lifting in CAD is fairly bespoke. It's using a lot of technology in Maple, which is fairly new or, I guess, a little bit undeveloped, so it's pushing some development there in terms of what I need to improve the lifting.
20:00
I'm very grateful for Maplesoft for working with me on that. Obviously, basically, I really need to investigate the performance properly. I conclude all the benchmarking and analysis of the data of this poly algorithmic method versus pure CAD and other implementations and the such like.
20:21
Also, outside of this project, what I'd like to see in this area is an implementation of new CAD or CAC. New CAD is non-uniform CAD by Brown, and CAC, again from some colleagues, is cylindrical algebraic coverings. I'd like to see that as sort of standalone QE to traverse fully existentially quantified formulae in Maple.
20:48
I'd like to see an implementation of these in Maple potentially. It would help out quantifier elimination a lot, because these sorts of problems appear within VTS quite a lot. So if there's a helper to do that quite fast, that would help quantifier elimination quite a lot in terms of VTS especially.
21:06
But yeah, I'm happy to take a lot of feedback and questions in the session, considering obviously this was very fast and I couldn't go into detail on a lot of things here, but hopefully that's given some stuff to talk about. So thanks, see you in the session.