【作者】 郭远华；

【导师】 曾振柄；

【作者基本信息】 华东师范大学 ， 系统分析与集成， 2010， 博士

【摘要】 自动定理证明(Automated Theorem Proving)或者机器定理证明(MechanicalTheorem Proving)是通过计算机实现定理证明.二十世纪五十年代以来自动定理证明一直是计算机科学的热点之一,在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用.部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一阶逻辑的可满足问题,检查子句集的满足式映射中的阻塞是该方法的关键.论文提出的子句搜索方法在判定子句集可满足性的同时给出了一个模型从而得到满足式映射.格值逻辑的不完全可比性便于描述人类的思维、判断和决策.格值命题逻辑系统LP(X)于1993年建立,目前对LP(X)系统的自动推理研究主要是归结方法,论文讨论了它的tableau方法.常用的逻辑证明方法重点在于判定可满足性而不能给出符合人们阅读习惯的演绎过程.归结方法、语义表方法、相继式方法是定理证明中的常用方法,但是重点在于判定而不是演绎,论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现,生成了类似于手工证明的可读证明.具体而言论文的工作包括以下几方面:(1)提出了子句搜索方法判定命题子句集的可满足性并给出可满足子句集的一个模型.子句搜索方法通过查找到子句集Φ不可扩展的子句C来判定Φ的可满足性.结合部分实例化方法将子句搜索方法提升至一阶,分离了谓词公式的结构和变量,从而提高合一算法的效率并节省了存贮空间.用正整数代表原子,负整数代表负文字,简化了算法实现.(2)提出了格值命题逻辑系统LP(X)的tableau方法,语义表中的公式都是受限蕴涵公式.通过引入Bound~s(X)、Bound_s(X)和极大相容集证明了其正确性和完备性.对于真值域可直积分解的系统LP(X),讨论了其格直积分解证明.(3)提出了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产生了类似于手工证明的演绎序列.将公式转化为二叉树的形式存贮于动态数组中减小了公式冗余,用数组下标代表公式简化了实现.(4)提出了应用于自然推理方法的回溯方法.先从假设集出发构建证明树,再从树根节点逐层推导各公式的属性,实现了相干自然推理系统NR的类似手工证明的自然推理方法证明.综上所述,论文提出了判定子句集可满足性的子句搜索方法并将其提升至一阶,提出了格值命题逻辑系统LP(X)的tableau方法,提出了后推试探方法和回溯方法并实现了相干命题逻辑系统R的可读证明,在理论和应用方面都有积极意义.更多还原

【Abstract】 Automated theorem proving or mechanical theorem proving is concerned with the building of computing systems that automate the process of proving theorems. Since the 1950s ATP has been one of active research topics of computer science and successfully used in mathematics, hard test and verification, software generation and verification, protocol verification, and artificial intelligence.The partial instantiation method reduces satisfiability problems for first-order logic to a series of ground-level satisfiability problems. Finding out the blockages of satisfier mappings for clause set is necessary in this method. Clause searching method proposed by us not only decides the satisfiability of clause set but also presents a model then obtains a satisfier mapping. Lattice-valued logic is not completely comparable and proper to describing thinking, judging and decision-making. Lattice-valued propositional logic system LP(X) is proposed in 1993. At present automated reasoning research about LP(X) focuses on resolution method, this thesis discusses tableau method for LP(X). The usual deduction methods such as resolution method, tableau method, sequent calculus etc emphasis on decidability instead of deduction. This thesis discusses implementing probing method and natural deduction method for relevant propositional R, and generates readable deduction sequences similar to humans’. The main content is as follows:(1) Proposing clause searching method which decides satisfiability of clause setΦand presents a model for satisfied set. This method decides satisfiability by searching one clause which can not extended fromΦ. Updating clause searching method to first-order by use of partial instantiation methods. This thesis separates predicate formulae into two parts: structures and variables hence improves unification algorithm efficiency and saves storage space. We establish a mapping of one atom onto one positive integer and one negative word onto one negative integer.(2) Proposing tableau method for lattice-valued propositional system LP(X), and all formulae is bounding implications. By introducing concepts such as Bound~s(X), Bound_s(X) and maximally consistent set, we prove this method’s correctness and completeness. If truth value space L of system LP(X) is the direct product of L_i, then we can prove theorems in LP(X) by means of direct decomposition.(3) Proposing backward probing method, obtaining a proof tree consisting of formulae in deduction sequences, and generating readable deduction sequences similar to humans’. We reduce formulae redundancy by transforming formulae into binary tree forms and storing them in a dynamic array, then array subscripts stand for formulae. (4) Proposing backtrace method applied to natural deduction method. Firstly constructing a proof tree from hypothesis set, then starting from tree root we obtain formulae attributes layer by layer. The thesis implements natural deduction method for relevant natural deduction system NR and generates readable deduction sequences similar to humans’.In conclusion, this thesis proposes clause searching method to check satisfiability of clause set, lifts the new method to first-order, proposes tableau method for latticed-valued logic system LP(X), proposes backward probing method and backtrace method, generates readable proof for relevant propositional logic and has a positive meaning in the theory and application.更多还原