期刊导航
期刊开放获取
vip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
1
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
模态逻辑D演绎过程的化简规则
1
作者
程晓春
孙吉贵
刘叙华
《吉林大学自然科学学报》
CAS
CSCD
1995年第2期39-43,共5页
以分析模态逻辑中文字公式的极性为基础,将经典逻辑的Davis-putnam纯文字化简规则推广到了命题模态逻辑D系统的自动演绎中,并给出了一些刻划D逻辑自动演绎特征的化简规则,这些化简规则通过对公式、子公式和公式集的有...
以分析模态逻辑中文字公式的极性为基础,将经典逻辑的Davis-putnam纯文字化简规则推广到了命题模态逻辑D系统的自动演绎中,并给出了一些刻划D逻辑自动演绎特征的化简规则,这些化简规则通过对公式、子公式和公式集的有效性(或不可满足性)的有条件的判断,进行证明过程的剪枝和化简,以提高D逻辑自动演绎的效率;这些化简规则都是依据公式(集)本身的结构特征,可用于D逻辑的任意一种推理实现系统,在机器上是容易实现的。
展开更多
关键词
模态逻辑
d
系统
化简规则
自动演绎
tableau
法
在线阅读
下载PDF
职称材料
题名
模态逻辑D演绎过程的化简规则
1
作者
程晓春
孙吉贵
刘叙华
机构
吉林大学符号计算与知识工程开放实验室
出处
《吉林大学自然科学学报》
CAS
CSCD
1995年第2期39-43,共5页
基金
国家自然科学基金
"863"计划和国家攀登计划资助课题
文摘
以分析模态逻辑中文字公式的极性为基础,将经典逻辑的Davis-putnam纯文字化简规则推广到了命题模态逻辑D系统的自动演绎中,并给出了一些刻划D逻辑自动演绎特征的化简规则,这些化简规则通过对公式、子公式和公式集的有效性(或不可满足性)的有条件的判断,进行证明过程的剪枝和化简,以提高D逻辑自动演绎的效率;这些化简规则都是依据公式(集)本身的结构特征,可用于D逻辑的任意一种推理实现系统,在机器上是容易实现的。
关键词
模态逻辑
d
系统
化简规则
自动演绎
tableau
法
Keywords
modal logic d
,
reducing rules
,
tableau method
分类号
O141 [理学—基础数学]
TP301 [自动化与计算机技术—计算机系统结构]
在线阅读
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
模态逻辑D演绎过程的化简规则
程晓春
孙吉贵
刘叙华
《吉林大学自然科学学报》
CAS
CSCD
1995
0
在线阅读
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部