格值命题逻辑系统L2n+1P(X)中基于半正则广义文字的自动推理算法
在格值命题逻辑系统L2n+1P(X)上,提出了半正则的正广义文字和半正则的负广义文字的概念,进一步给出了半正则广义子句和半正则广义子句集的定义,详细地讨论了L2n+1P(X)上以中界元M为归结水平的半正则广义文字之间的M-归结性,最后,给出了L2n+1P(X)上基于半正则广义文字的归结水平为M的归结自动推理算法,并验证了其可靠性和完备性.
半正则的广义文字、中界元、格值命题逻辑系统、归结自动推理、自动推理算法
23
O153(代数、数论、组合理论)
国家自然科学基金资助项目60474022,60875034;高等学校博士学科点专项科研基金资助项目20060613007
2009-10-27(万方平台首次上网日期,不代表论文的发表时间)
共6页
21-26