We present a survey of algorithms, mostly drawn from the broad field of logic in computer science, that rely on Schanuel’s conjecture for termination and/or correctness. Schanuel’s conjecture is a central hypothesis in transcendental number theory that generalises many existing classical results such as the Lindemann-Weierstrass theorem and Baker’s theorem on linear independence of logarithms of algebraic numbers. The algorithmic use of Schanuel’s conjecture was spearheaded by computer algebraists in the 1970s, as well as by Macintyre and Wilkie in the 1990s, most notably to establish the decidability of real arithmetic expanded with the exponential function. Since then, many further applications have been recorded in the literature. We present and discuss several of these algorithms, with a particular focus on the precise role played by Schanuel’s conjecture.

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

Algorithmic Applications of Schanuel’s Conjecture

  • Toghrul Karimov,
  • Joris Nieuwveld,
  • Joël Ouaknine,
  • Mihir Vahanwala,
  • James Worrell

摘要

We present a survey of algorithms, mostly drawn from the broad field of logic in computer science, that rely on Schanuel’s conjecture for termination and/or correctness. Schanuel’s conjecture is a central hypothesis in transcendental number theory that generalises many existing classical results such as the Lindemann-Weierstrass theorem and Baker’s theorem on linear independence of logarithms of algebraic numbers. The algorithmic use of Schanuel’s conjecture was spearheaded by computer algebraists in the 1970s, as well as by Macintyre and Wilkie in the 1990s, most notably to establish the decidability of real arithmetic expanded with the exponential function. Since then, many further applications have been recorded in the literature. We present and discuss several of these algorithms, with a particular focus on the precise role played by Schanuel’s conjecture.