检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:刘富春[1]
机构地区:[1]广东工业大学应用数学学院
出 处:《计算机科学》2006年第4期141-142,147,共3页Computer Science
基 金:广东省自然科学基金项目(020146;031541;广东工业大学青年基金项目(042027)
摘 要:逻辑程序具有丰富的表达能力和非确定性等特点,在定理机器证明、关系数据库系统、程序验证、模块化程序设计和非单调推理等方面都有了广泛的应用。本文是继续文[8]的工作。首先通过两个反例,指出了文[7]中关于否定完备化程序 Comp((?),Pr)和蕴涵完备化程序(Comp(→,Pr)的两个重要定理都存在一定程度的错误。然后对这两个定理进行了修改,用后继算子 T_(pr) 和 Fitting 算子 F_(pr)的不动点语义,分别给出了否定完备化程序 Comp(→,Pr)和蕴涵完备化程序 Comp(→,Pr)的 Herbrand 模型的充分务件和必要务件,这将在逻辑程序的最优不动点和最小不动点的语义研究中有着重要的应用价值。Logic programming has been widely applied in mechanical theorem proving, relational database system, modularized programming and non-monotone reasoning. This paper is the continuation of reference [8]. Two faults on →-completion and →-completion in reference [7] are found by examples. Then the fixedpoints of the consequence operator and Fitting's operator are presented, which characterize the semantics on →-completion and →-completion.
关 键 词:逻辑程序 否定和蕴涵完备化程序 Herbrand模型 后继算子 Fitting算子
分 类 号:TP31[自动化与计算机技术—计算机软件与理论] O159[自动化与计算机技术—计算机科学与技术]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:18.224.37.168