命题公式的一种演绎判定方法

作     者：齐德昱 李小薪 Qi De-yu;Li Xiao-xin

作者机构：华南理工大学计算机科学与工程学院广东广州510640 

出 版 物：《华南理工大学学报（自然科学版）》 (Journal of South China University of Technology(Natural Science Edition))

年 卷 期：2008年第36卷第9期

页      码：71-76页

摘      要：目前命题公式的判定方法大都是基于语义的,不能给出演绎过程,而演绎过程是许多推理性应用的重要依据.文中针对命题演算系统L,提出了一种可同时给出演绎过程的判定方法——演绎判定方法.首先定义了消解复杂性的两种范式:最简范式和文字范式,在此基础上采用演绎方法证明了L中的可判定性定理,并设计了命题公式的演绎判定算法P(F).P(F)的时间复杂度为O(n3),远远小于基于真值表法的O(2n)和基于策略方案HAL的O(n5).

主 题 词：命题逻辑 公式判定 演绎判定 自动定理证明 

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3321/j.issn:1000-565X.2008.09.015

馆 藏 号：203100230...