论大幅拓展自动化证明方法的潜在应用范畴
计算机科学中的逻辑
2021-05-27 v3
摘要
在本文中，我们考察了计算机辅助证明方法比通常所认识的可被远更广泛地应用的潜力。更具体地说，我们认为存在大量机会可推导有用且范围极窄的数学结果与性质，它们仅与高度专门化的工程应用有实际相关性，却因具有纯数学与应用数学领域 conventionally 所追求者所不具备的非典型特征而被忽视。作为一个具体示例，我们展示了将用于证明多项式非负性的自动化方法作为维度固定（dimension-pinning）策略的一部分，以证明 d 维正定矩阵的相对增益阵列（RGA）之逆在 时为双随机矩阵。
引用
@article{arxiv.1906.00931,
title = {On Radically Expanding the Landscape of Potential Applications for Automated Proof Methods},
author = {Jeffrey Uhlmann and Jie Wang},
journal= {arXiv preprint arXiv:1906.00931},
year = {2021}
}
备注
Expanded narrative