化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.
- artificial intelligence /
- multiple-value logic /
- automated reasoning /
- resolution principle

点击查看大图