Dataset for Quantifier Elimination and CAD examples in Maple

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'：可导入至Maple的文件，用于加载交互式量词消去（Quantifier Elimination，QE）示例数据库，并附带构建与打印此类示例的相关函数。
- 'CADDatabase.mm'：可导入至Maple的文件，用于加载名为'CADExamples'的纯无量词示例表，且无辅助函数。此类示例涵盖多种类型，且兼容Maple的'QuantifierElimination'包中圆柱代数分解（Cylindrical Algebraic Decomposition，CAD）函数`CylindricalAlgebraicDecompose`的输入语义。
- 'TarskiFormulaLaTeXTools.mpl'：可导入至Maple的文件，用于优化Maple对源自'QuantifierElimination'包的塔斯基公式（TarskiFormula）的LaTeX排版效果，当该公式传入Maple内置的`latex`函数时生效。
- 'Example Database Info.pdf'：用于记录本数据集所有示例的参考文献与来源信息的PDF文档。

所有通过使用上述文件生成的公式或半代数集，均采用'RationalTarskiFormula'或'TarskiFormula'类型，以兼容'QuantifierElimination'包。经少量转换后，它们可适配Maple的'RegularChains'与'SyNRAC'包。
- 'QuantifierEliminationConversionTools.mpl'：可导入至Maple的文件，提供三个格式转换函数：`convertQEtoRC`、`convertQEtoSyNRAC`与`convertQEtoQEPCAD`，分别可将'QuantifierElimination'格式的塔斯基公式转换为适配'RegularChains'、'SyNRAC'或'QEPCAD'的格式。其中'QEPCAD'需要定制化输入，因此可将生成的字符串写入文件后，重定向至QEPCAD运行。

各文件的详细信息可查阅其元数据。

搜集汇总

背景与挑战

背景概述

该数据集专为Maple软件设计，提供量词消去（QE）和圆柱代数分解（CAD）的示例文件及相关工具，包括交互式数据库、示例表、LaTeX格式化工具和转换函数，以支持与'QuantifierElimination'包及其他Maple包的兼容性。数据集旨在帮助用户进行符号计算和代数研究，通过提供现成的示例和转换工具，简化在Maple中处理QE和CAD问题的流程。