Dataset for Quantifier Elimination and CAD examples in Maple
Quantifier Elimination over the reals is a problem in Computer Algebra consisting of quantified boolean formulae of polynomial constraints. This dataset provides a collection of real world examples amalgamated from a range of sources, most not seen together before. This database is useful for the purposes of benchmarking and testing, and in particular is an accompaniment for the future to be released Maple package 'QuantifierElimination'. While the main contribution is the collection of Quantifier Elimination problems, auxillary functions are provided for various other purposes, including viewing and building the examples. Also, examples for pure CAD are provided, ie. just semi-algebraic formulae. Lastly, a document detailing references for sources of these examples is provided.
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.
Cite this dataset as:
Tonks, Z.,
2023.
Dataset for Quantifier Elimination and CAD examples in Maple.
Bath: University of Bath Research Data Archive.
Available from: https://doi.org/10.15125/BATH-00746.
Export
Data
CADDatabase.mm
text/plain (4kB)
Creative Commons: Attribution 4.0
A file that can be read into Maple loading a table of unquantified semi algebraic expressions called 'CADExamples', and nothing else. No auxillary functions are provided in this file.
Code
TarskiFormulaLaTeXTools.mpl
text/plain (2kB)
Software: MIT License
A file that can be read into Maple, which having done so will enable Maple to better produce the LaTeX for Tarski formulae, 'TarskiFormula' type enabled by the package 'QuantifierElimination'. Hence the Maple inbuilt 'latex' will produce better LaTeX for such formulae.
QuantifierElimi … ersionTools.mpl
text/plain (3kB)
Software: MIT License
A file that can be read into Maple, which loads three functions 'convertQEtoRC','convertQEtoSyNRAC', c'onvertQEtoQEPCAD' which will convert a QE example written in 'QuantifierElimination' format to that of RegularChains, SyNRAC, or QEPCAD respectively. Note that the Quantifier Elimination procedure in RegularChains is RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination. Note that these functions require the original problem in prenex form. Note QEPCAD will accept redirection of a problem
QE Example Bank.mpl
text/plain (95kB)
Software: MIT License
A file that can be read into Maple that loads tables containing explicit QE problems, and tables and functions from which QE examples can be built. Also loads auxillary functions that can be used to view or interact with such tables, and a "Help" function explaining how to use everything further. All QE problems produced are of format amenable to usage with the package 'QuantifierElimination', which enables the 'TarskiFormula' type.
Creators
Zak Tonks
University of Bath
Documentation
Data processing and preparation activities:
The CAD and QE examples contained in the relevant database come from a wide range of sources, documented in the contained pdf. Where appropriate, these may have been reformatted into Maple format, eg. from Mathematica format for the economics examples. Many of the examples arise from David Wilson's CAD database (reference found in the .pdf), and where appropriate they have been reformatted as the relevant QE problem for the QE database. Otherwise, they may have had some slight reformatting such that they form lists of relations, or sets of polynomials.
Technical details and requirements:
Maple 2019.0 or newer is sufficient to view the examples. Previous versions of Maple may suffice, although cannot be guaranteed. The examples are all written to be directly compatible for functions contained in the package 'QuantifierElimination' for Maple, to be released. Conversion for usage with Maple packages 'RegularChains' or 'SyNRAC' is available by the included conversion routines. A version of 'RegularChains' is included with any consumer version of Maple, but the newest version is also available online. 'SyNRAC' is only available online.
Documentation Files
Example Database Info.pdf
application/pdf (261kB)
Creative Commons: Attribution 4.0
Provides references for sources of all semi-algebraic formulae contained in the files in this repository.
Funders
Engineering and Physical Sciences Research Council
https://doi.org/10.13039/501100000266
PhD Studentship, Hybrid Techniques in Quantifier Elimination
EP/EG-CM1146/1
Maplesoft
PhD Studentship, Hybrid Techniques in Quantifier Elimination
EP/EG-CM1146/1
Publication details
Publication date: 1 July 2023
by: University of Bath
Version: 1
DOI: https://doi.org/10.15125/BATH-00746
URL for this record: https://researchdata.bath.ac.uk/id/eprint/746
Related papers and books
Tonks, Z., 2020. A Poly-algorithmic Quantifier Elimination Package in Maple. In: Communications in Computer and Information Science. Springer International Publishing, 171-186. Available from: https://doi.org/10.1007/978-3-030-41258-6_13.
Davenport, J. H., Nair, A. S., Sankaran, G. K., and Uncu, A. K., 2023. Lazard-style CAD and Equational Constraints. In: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation. ACM. Available from: https://doi.org/10.1145/3597066.3597090.
Davenport, J. H., Tonks, Z. P., and Uncu, A. K., 2023. A Poly-algorithmic Approach to Quantifier Elimination. In: 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). IEEE. Available from: https://doi.org/10.1109/synasc61333.2023.00013.
Contact information
Please contact the Research Data Service in the first instance for all matters concerning this item.
Contact person: Zak Tonks
Faculty of Science
Computer Science
