Description
This dataset provides the following:
- 'QE Example Database.mpl': a file that can be read into Maple that loads an interactive database of QE examples, along with functions to build and print them,
- 'CADDatabase.mm': a file that can be read into Maple that loads a table of purely unquantified examples for CAD, 'CADExamples', with no auxillary functions. These examples are of various types, but are compatible with the input semantics of 'CylindricalAlgebraicDecompose' for the package 'QuantifierElimination' for Maple.
- 'TarskiFormulaLaTeXTools.mpl': a file that can be read into Maple that allows Maple to better format Tarski formulae (type 'TarskiFormula' arising from the package 'QuantifierElimination') for LaTeX when passed into Maple's inbuilt function 'latex'.
- 'Example Database Info.pdf': A pdf documenting reference and origin information about all examples from the databases included.
All formulae or otherwise semi-algebraic sets produced by usage of these files are in 'RationalTarskiFormula' or 'TarskiFormula' type, for compatibility with 'QuantifierElimination'. They are amenable to usage with Maple packages 'RegularChains' or 'SyNRAC', after some conversion.
- 'QuantifierEliminationConversionTools.mpl': a file that can be read into Maple that loads two functions for conversion of Tarski formulae from 'QuantifierElimination' format, 'convertQEtoRC', 'convertQEtoSyNRAC', and 'convertQEtoQEPCAD' which convert to format amenable to 'RegularChains', 'SyNRAC', or 'QEPCAD' respectively. 'QEPCAD' requires bespoke input, so one can write the produced string to a file before redirection into QEPCAD.
More information about each file is in the metadata for each file.
- 'QE Example Database.mpl': a file that can be read into Maple that loads an interactive database of QE examples, along with functions to build and print them,
- 'CADDatabase.mm': a file that can be read into Maple that loads a table of purely unquantified examples for CAD, 'CADExamples', with no auxillary functions. These examples are of various types, but are compatible with the input semantics of 'CylindricalAlgebraicDecompose' for the package 'QuantifierElimination' for Maple.
- 'TarskiFormulaLaTeXTools.mpl': a file that can be read into Maple that allows Maple to better format Tarski formulae (type 'TarskiFormula' arising from the package 'QuantifierElimination') for LaTeX when passed into Maple's inbuilt function 'latex'.
- 'Example Database Info.pdf': A pdf documenting reference and origin information about all examples from the databases included.
All formulae or otherwise semi-algebraic sets produced by usage of these files are in 'RationalTarskiFormula' or 'TarskiFormula' type, for compatibility with 'QuantifierElimination'. They are amenable to usage with Maple packages 'RegularChains' or 'SyNRAC', after some conversion.
- 'QuantifierEliminationConversionTools.mpl': a file that can be read into Maple that loads two functions for conversion of Tarski formulae from 'QuantifierElimination' format, 'convertQEtoRC', 'convertQEtoSyNRAC', and 'convertQEtoQEPCAD' which convert to format amenable to 'RegularChains', 'SyNRAC', or 'QEPCAD' respectively. 'QEPCAD' requires bespoke input, so one can write the produced string to a file before redirection into QEPCAD.
More information about each file is in the metadata for each file.
| Date made available | 1 Jul 2023 |
|---|---|
| Publisher | University of Bath |
Research output
- 3 Chapter in a published conference proceeding
-
A Poly-algorithmic Approach to Quantifier Elimination
Davenport, J. H., Tonks, Z. P. & Uncu, A. K., 10 May 2024, Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023. Stratulat, S., Marin, M., Negru, V. & Zaharie, D. (eds.). U. S. A.: IEEE, p. 44-51 8 p. (Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023).Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding
-
Lazard-style CAD and Equational Constraints
Davenport, J. H., Nair, A. S., Sankaran, G. K. & Uncu, A. K., 24 Jul 2023, ISSAC 2023 - Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation. Jeronimo, G. (ed.). Association for Computing Machinery, p. 218-226 9 p. (ACM International Conference Proceeding Series).Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding
Open Access4 Link opens in a new tab Citations (SciVal) -
A Poly-algorithmic Quantifier Elimination Package in Maple
Tonks, Z., 28 Feb 2020, Maple in Mathematics Education and Research - 3rd Maple Conference, MC 2019, Proceedings. Gerhard, J. & Kotsireas, I. (eds.). Springer International Publishing, p. 171-186 16 p. (Communications in Computer and Information Science; vol. 1125 CCIS).Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding
6 Link opens in a new tab Citations (SciVal)
Student theses
-
Poly-algorithmic Techniques in Real Quantifier Elimination
Tonks, Z. (Author), Davenport, J. (Supervisor) & Bradford, R. (Supervisor), 8 Sept 2021Student thesis: Doctoral Thesis › PhD
File
Cite this
- DataSetCite