化LF(X)中任一公式为可归约形式的算法
Algorithm of Transforming Any Formula in LF(X)into Reducible Form
-
摘要:针对基于归结方法的自动推理过程中的化任一公式为可归约形式这一问题进行研究.简述了LF(X)及 其中公式的相关概念,证明了对LF(X)中公式进行转化的若干理论结果,并由此给出化LF(X)中任一公式为可 归约形式的理论基础和基本算法.Abstract:In the process of automated reasoning based on the resolution principle by computers, it is necessary to transform any formula into reducible form. The algorithm of transforming any formula in LF(X)is investigated. Based on the introduction of LF(X)and the related concepts, theoretic results for the transformation are proved. Subsequently, the algorithm of transforming any formula in LF(X)into a reducible form is given.
-
点击查看大图
计量
- 文章访问数:1287
- HTML全文浏览量:120
- PDF下载量:114
- 被引次数:0
下载: