Scholarlink

<p>The <i>cylindrical algebraic covering</i> method was originally proposed to decide the satisfiability of a set of <i>non-linear real arithmetic</i> 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 <i>quantifier elimination</i> 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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Extensions of the Cylindrical Algebraic Covering Method for Quantifiers

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年4月28日

查看全文
  • Jasper Nalbach,
  • Gereon Kremer

摘要

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.