摘要
该文将命题逻辑的定理证明转换为多项式方程的求解问题,从而提出了一种基于非子句的代数化方法．在代数化的过程中,以一种形式化的方式给出了命题公式的文法定义,通过语法、语义分析实现了命题公式的代数化．此外,又根据特征列的性质,提出了一种逻辑推论自动生成的方法．
A formal definition of proposition formulae was provided by context-free grammar,and the conversion from proposition formulae to polynomials was solved automatically. Using Wu＇s Method, the paper presented another solution to the problem of theorem reasoning. In addition, a method for producing logical deduction was introduced.
出处
《华东师范大学学报（自然科学版）》
CAS
CSCD
北大核心
2006年第1期80-86,共7页
Journal of East China Normal University(Natural Science)
关键词
吴方法
命题逻辑
上下文无关文法
定理证明
逻辑推论
Wu＇s Method
propositional calculus
context-free grammar
theorem reason-ing
logical deduction
