摘要：在一种支持并发程序提取的半构造逻辑系统中工作，我们从基于高斯消元法的构造证明中提取了一个反转非奇异实值矩阵的程序。并发用于有效地进行枢轴选取，即在非空实数向量中找到一个非零条目。
作者：Ulrich Berger, Monika Seisenberger, Dieter Spreen, Hideki Tsuiki
论文ID：2305.10125
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-18
PDF 下载： 英文版 中文版pdf翻译中