DOI: 10.4204/EPTCS.393.12

ACL2 Proofs of Nonlinear Inequalities with Imandra

Grant Passmore (Imandra Inc.)

Nov 2023

0被引用

0笔记

摘要原文

We present a proof-producing integration of ACL2 and Imandra for proving nonlinear inequalities. This leverages a new Imandra interface exposing its nonlinear decision procedures. The reasoning takes place over the reals, but the proofs produced are valid over the rationals and may be run in both ACL2 and ACL2(r). The ACL2 proofs Imandra constructs are extracted from Positivstellensatz refutations, a real algebraic analogue of the Nullstellensatz, and are found using convex optimization.

展开全部

机器翻译

AI理解论文&经典十问

参考文献

被引用

社区问答

图表提取

参考文献

发布时间 · 被引用数 · 默认排序

被引用

发布时间 · 被引用数 · 默认排序

社区问答