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.