Extensions of the Cylindrical Algebraic Covering Method for Quantifiers
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911191388913664 |
|---|---|
| author | Nalbach, Jasper Kremer, Gereon |
| author_facet | Nalbach, Jasper Kremer, Gereon |
| contents | The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cylindrical algebraic covering method to allow for checking the truth of arbitrary non-linear arithmetic formulas, adding support for both quantifiers and Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas. After introducing the algorithm, we elaborate on various extensions, optimizations and heuristics. Finally, we present an experimental evaluation of our implementation and provide a comparison with state-of-the-art SMT solvers and quantifier elimination tools. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_03070 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Extensions of the Cylindrical Algebraic Covering Method for Quantifiers Nalbach, Jasper Kremer, Gereon Symbolic Computation The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cylindrical algebraic covering method to allow for checking the truth of arbitrary non-linear arithmetic formulas, adding support for both quantifiers and Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas. After introducing the algorithm, we elaborate on various extensions, optimizations and heuristics. Finally, we present an experimental evaluation of our implementation and provide a comparison with state-of-the-art SMT solvers and quantifier elimination tools. |
| title | Extensions of the Cylindrical Algebraic Covering Method for Quantifiers |
| topic | Symbolic Computation |
| url | https://arxiv.org/abs/2411.03070 |