受限的proflog语言及其表推演过程语义  

CONSTRAINED PROFLOG LANGUAGE AND ITS PROCEDURAL SEMANTICS BASED ON TABLEAU

作　　者：陈荣[1] 孙吉贵[2] 姜云飞[1] 

机构地区：[1]中山大学,软件所,广东,广州,510275 [2]吉林大学,计算机科学系,吉林,长春,130023

出　　处：《广西师范大学学报（自然科学版）》2003年第1期27-33,共7页Journal of Guangxi Normal University:Natural Science Edition

基　　金：广东省自然科学基金，中山大学校科研和教改项目

摘　　要：Fitting提出一种逻辑程序设计语言proflog,并把表推演机制作为语言的过程语义.表推演具有直观、灵活的特点,它的单步扩展规则具有很强的语义特征,它是扩展逻辑程序类的另一个理想的证明论.不过proflog包含了全部一阶理论,等词的替换性使得proflog过程语义比较复杂.在此提出讨论一种受限的程序语言cProflog,它包含函词,但限制了等词的替换性,体现了表达能力与计算复杂性之间的平衡.对于逻辑程序语言cProflog,还给出了复杂性较低的表推演过程.

关 键 词：表推演 过程语义 非单调性 逻辑程序设计语言 证明论 proflog 扩展规则 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]