整数与实数变量的线性算术有效决策程序
计算机科学中的逻辑
2007-05-23 v1
摘要
本文考虑基于有限自动机的算法，用于处理包含实数和整数变量的线性算术。以前的工作表明，这一理论可以通过使用无限单词上的有限自动机来处理，但这涉及一些难以实现的算法。本文的贡献在于使用拓扑论证明明确，仅需一种受限制的无限单词自动机类即可处理实数和整数线性算术。这使得可以使用大大简化的算法，这些算法已成功实现。
引用
@article{arxiv.cs/0303019,
title = {An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables},
author = {Bernard Boigelot and Sebastien Jodogne and Pierre Wolper},
journal= {arXiv preprint arXiv:cs/0303019},
year = {2007}
}
备注
20 pages, 6 figures