基于超演绎的自动定理证明方法、装置及存储介质

摘要

本发明公开了一种基于超演绎的自动定理证明方法、装置及存储介质，从一阶逻辑子句集S选择包括单个核子子句及多个电子子句的子集构建标准矛盾体，得到矛盾体分离式R。若R为空子句，定理被证明。当R不为空子句时，若R有效且全为正文字，则将R加入到S中，停止本次矛盾体分离超演绎；当R含负文字，则在S中重新选择子句继续演绎；若无效，需回退到上一演绎步骤，在S中重新选择子句继续演绎；当S遍历完或满足定理判定终止条件，结束本次矛盾体分离超演绎。通过本发明的实施，具有每个矛盾体分离演绎只有1个子句含负文字的特点，能有效缩减多元演绎的路径搜索空间和提升演绎效率，增强了多元演绎推理系统的一阶逻辑自动定理证明能力。