-
题名广义RUE-NRF归结
被引量：2
- 1
-
-
作者
刘叙华
-
机构
吉林大学计算机科学系
-
出处
《吉林大学自然科学学报》
CAS
CSCD
1993年第1期37-40,共4页
-
基金
国家自然科学基金
国家教委博士点基金
+1 种基金
国家863计划
国家攀登计划项目资助课题
-
文摘
本文将RUE-NRF归结使用在广义子句集上,提出了广义RUE-NRF归结方法,并证明了这一方法对于一阶逻辑的完备性;将1型、2型删除策略引入广义RUE-NRF归结.
-
关键词
调解
rue-nrf
归结
消解
广义消解
-
Keywords
generalized resolution, paramodulation , rue-nrf resolution
-
分类号
TP31
[自动化与计算机技术—计算机软件与理论]
-
-
题名NC线性对称调解
被引量：2
- 2
-
-
作者
孙吉贵
刘叙华
-
机构
吉林大学计算机科学系
-
出处
《计算机学报》
EI
CSCD
北大核心
1993年第8期561-567,共7页
-
基金
国家自然科学基金
国家教委博士点基金
-
文摘
本文提出了NC调解方法,证明了NC对称调解与NC归结的结合及广义对称调解与广义归结的结合的线性演绎都是完备的。
-
关键词
广义归结
NC归结
NC调解
-
Keywords
generalized resolution,NC-resolution,generalized paramodulation,NC-paramodulation.
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名广义Horn集
- 3
-
-
作者
刘叙华
欧阳丹彤
-
机构
吉林大学计算机科学系
-
出处
《软件学报》
EI
CSCD
北大核心
1995年第4期248-256,共9页
-
基金
国家自然科学基金
博士点基金
+1 种基金
863计划
国家攀登计划项目
-
文摘
本文定义了广义Ｈｏｒｎ集，并在广义Ｈｏｒｎ集上证明了广义输入归结的完备性；广义输入对称调解的完备性；以及一定条件下的广义输入有向调解的完备性．文中还证明了广义调解法的提升引理．
-
关键词
对称调解
有向调解
广义
HORN集
-
Keywords
generalized resolution, generalized symmetric paramodulation, generalized directed paramodulation, generalized Horn set.
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名关于广义调解的一点注记
- 4
-
-
作者
刘叙华
孙吉贵
-
机构
吉林大学计算机科学系
-
出处
《吉林大学自然科学学报》
CAS
CSCD
1993年第3期59-60,共2页
-
基金
国家自然科学基金
博士点基金
+1 种基金
863计划
国家攀登计划
-
文摘
本文指出了广义调解完备性证明中一个错误,并且给出了使广义调解完备的根据.
-
关键词
广义归结
广义调解
NC调解
-
Keywords
generalized resolution, generalized paramodulation, NC-paramodulation
-
分类号
O141
[理学—基础数学]
-
-
题名广义λ－调解
- 5
-
-
作者
刘叙华
司徒芊
-
机构
吉林大学计算机科学系
-
出处
《计算机学报》
EI
CSCD
北大核心
1995年第2期135-140,共6页
-
基金
国家自然科学基金
博士点基金
+1 种基金
863计划
国家攀登计划资助
-
文摘
本文提出了算子模糊逻辑中的广义λ－调解方法，证明了它和广义λ－归结的联合使用，对于λＥ－不可满足广义子句集是完备的．
-
关键词
算子模糊逻辑
广义
Λ-归结
λ-调解
-
Keywords
Operator Fuzzy logic, generalized λ-resolution, generalized λ-paramodulation.
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
