Algorithm of Transforming Any Formula
in LF(X)into Reducible Form

MENG Dan; SONG Zhen-ming; QIN Ke-yun

Volume 16 Issue 4

Aug. 2003

Turn off MathJax

Article Contents

Journal of Southwest Jiaotong University > 2003 > 16(4): 433-437.

MENG Dan, SONG Zhen-ming, QIN Ke-yun. Algorithm of Transforming Any Formulain LF(X)into Reducible Form[J]. Journal of Southwest Jiaotong University, 2003, 16(4): 433-437.

Citation:

MENG Dan, SONG Zhen-ming, QIN Ke-yun. Algorithm of Transforming Any Formula in LF(X)into Reducible Form[J]. Journal of Southwest Jiaotong University, 2003, 16(4): 433-437.

MENG Dan, SONG Zhen-ming, QIN Ke-yun. Algorithm of Transforming Any Formulain LF(X)into Reducible Form[J]. Journal of Southwest Jiaotong University, 2003, 16(4): 433-437.

Citation:

MENG Dan, SONG Zhen-ming, QIN Ke-yun. Algorithm of Transforming Any Formula in LF(X)into Reducible Form[J]. Journal of Southwest Jiaotong University, 2003, 16(4): 433-437.

PDF( 0 KB)

Algorithm of Transforming Any Formula in LF(X)into Reducible Form

Publish Date: 25 Aug 2003

Abstract

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