递归Prolog程序的正确性证明

CORRECTNESS PROOF OF THE RECURSIVE PROLOG PROGRAM

本文提出了一种称为Ｐｒｏ图的图形方法，并用该图形方法进行了递归Ｐｒｏｌｏｇ程序的正确性证明．文中包括Ｐｒｏ图的基本概念及生成规则，Ｐｒｏ图上各节点的关系，Ｐｒｏ图的激活过程，并给出了关于递归程序正确性证明的公理和定理．

The paper presents a graphic method called Pro-graph. This method canbe used in correctness proof of Prolog recursive program. The paper includes conception of Pro-graph, generative rules, relationship between nodes and 'fire' process of the graph. The paper introduces axioms and theorems about proof of the recursive program.