一阶谓词逻辑的图形推理法

Graphical Reasoning Method to First-order Predicate Logic

针对已有一阶谓词逻辑推理方法中存在的推理效率低等问题,研究一种基于谓词/变迁系统的图形推理法。定义了描述谓词间与/或关系的谓词-与/或图,借助谓词-与/或图表示谓词/变迁系统,提出一种实现反向推理的目标制导的图形推理法。该方法推理效率高,较已有的推理方法具有一定的优越性。

Traditional reasoning methods to first-order predicate logic have some problems such as inference inefficient, so a graphical reasoning method based on predicate/transition system was presented. The concept of predicate-and/or graph describing the and/or relation among predicates was presented, and several pre-and/or graph representations of predicate/transition system were defined. Finaly, a goal guiding graphical reasoning method adopting backward rea- soning way was put forward. This method has high efficiency and some advantages compared with other present reason- ing methods.