使用 Imandra 进行非线性不等式的 ACL2 证明
计算机科学中的逻辑
2023-11-16 v1 符号计算
摘要
我们提出了一种用于证明非线性不等式的 ACL2 与 Imandra 的产证集成。这利用了暴露其非线性决策过程的新 Imandra 接口。推理在实数上进行，但所产出的证明在有理数上有效，并可在 ACL2 和 ACL2(r) 中运行。Imandra 构建的 ACL2 证明提取自 Positivstellensatz 反驳（Nullstellensatz 的实代数类比），并通过凸优化求得。
引用
@article{arxiv.2311.08861,
title = {ACL2 Proofs of Nonlinear Inequalities with Imandra},
author = {Grant Passmore},
journal= {arXiv preprint arXiv:2311.08861},
year = {2023}
}
备注
In Proceedings ACL2-2023, arXiv:2311.08373