摘要：代数格理论中两个关键问题的NP困难性规约函数的形式验证：最接近的向量问题和最短向量问题，都在无穷范数中。形式化揭示了现有文献中存在的一些证明问题。本文描述了如何在形式化中纠正这些问题。这项工作是在证明助手Isabelle中完成的。
作者：Katharina Kreuzer, Tobias Nipkow
论文ID：2306.08375
分类：Computational Complexity
分类简称：cs.CC
提交时间：2023-06-16
PDF 下载： 英文版 中文版pdf翻译中