舆论纲要：矫正验算表面与算法接洽

矫正题目是人为智能中接洽的一个热门题目，它生存于科学创造、软硬件尝试、常识库的保护等多个范围。跟着暂时消息的爆裂式延长，必然引导各个范围中展示的矫正题目变得更为搀杂，简单依附体味的细工矫正将不许满意需要。这就诉求咱们创造体制化面向计划的矫正验算表面和本领，运用计划机扶助举行半机动化交互式以至机动化的矫正。暂时矫正验算的接洽尚居于起步阶段，固然仍旧创造了 AGM 表面、迭代矫正表面等公设体例以及 R 验算体例如许的情势化矫正验算体例，但仍生存少许题目：一是矫正验算体例中仍旧生存着简略准则，难以用作矫正验算机动化的表面普通。第二，运用矫正验算推导出的截止不许保护确定是极大削减。第三，不足不妨用来计划一切极大削减的本领。 对准那些题目，正文在矫正验算机动化表面普通和极大削减计划本领上面举行了深刻的领会与接洽，提出了一个不含简略准则的 R 验算体例和鉴于极小不融合子集的极大削减计划本领等，并在此普通上对准一阶谈话的多个特出子集提出了相映的算法。正文的重要处事和奉献囊括： (1) 领会并证领会极小不融合子集和极大削减之间的联系，提出了从极小不融合子集计划极大削减的算法，领会了由极小不融合子集求解极大削减题目的计划搀杂性。经过领会 Horn 子句极小不融合子集的个性，给出了一个鉴于融合性查看算法的极小不融合子集交互式列举算法。结果，获得了在 Horn 子句入彀算一切极大削减的交互式算法。(2) 在 R 验算表面的普通上，提出了消去简略准则的本领，创造了仅包括对于论理贯穿词标记和量词标记验算准则的不含简略准则的 R 验算体例，并证领会该体例仍旧具备可达性、真实性和实足性。提出了一种用来决定运用量词准则进程顶用于替代的项的本领。提出了需要 R 表白式的观念，证领会它与极小不融合子集的联系。提出了并证领会极大削减与极大融合子集之间的联系。(3) 领会并证领会极大削减题目和极小不融合子集题目可计划的充要前提，归纳提出了三种计划一切极大削减的本领：鉴于极小不融合子集的本领、鉴于极大融合子集的本领以及鉴于不含简略准则的 R 验算体例的交互式推导本领。(4) 给出了鉴于极小不融合子集计划一切极大削减的算法框架，并在此普通上辨别提出了对准不含变元的一阶谈话和 Datalog 中极大削减计划题目的停机算法，并证领会其精确性。