PROLOG逻辑程序正确性证明

ＰＲＯＬＯＧ是一种逻辑程序设计语言，本文以这种语言为例，提出了谓词依赖性、等价式、谓词规范等概念，并且在此基础上对ＰＲＯＬＯＧ谓词加以分类。最后基于一阶谓词逻辑提出了ＰＲＯＬＯＧ程序正确性的一种证明方法。