As a continuate work, ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed, which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra. In this principle, the resolution level is an ideal of lattice implication algebra, instead of an element in truth-value field. Moreover, the soundness theorem is given. In the light of lifting lemma, the completeness theorem is established. This can provide a new tool for automated reasoning.
XU Wei-tao 1,3 (许伟涛), XU Yang 1,2(徐扬)
. Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra[J]. Journal of Shanghai Jiaotong University(Science), 2012
, 17(2)
: 178
-181
.
DOI: 10.1007/s12204-012-1249-1
[1] Robinson J A. A machine-oriented logic based on the resolution principle [J]. Journal of the Association for Computing Machinery, 1965, 12(1): 23-41.
[2] Luckham D. Refinement theorems in resolution theory [C]//Proceedings of IRIA Symposium Automatic Demonstration. Versailes, France: Spring-Verlag,
1968: 16-21.
[3] Chang C L, Lee R C-T. Symbolic logic and mechanical theorem proving [M]. New York: Academic Press,1973.
[4] Liu Xu-hua. Resolution-based automated reasoning [M]. Beijing: Science Press, 1994 (in Chinese).
[5] Wos L. Automated reasoning: 33 basic research problems [M]. New Jersey, USA: Prentice Hall, 1988.
[6] Morgan C G. A resolution principle for a class of many-valued logics [J]. Logique and Analyse, 1976,19(74-76): 311-339.
[7] Baaz M, Ferm¨uller C G. Resolution-based theorem proving for many valued logics [J]. Journal of Symbolic Computation, 1995, 19(4): 353-391.
[8] Xu Yang. Lattice implication algebras [J]. Journal of Southwest Jiaotong University, 1993, 28(1): 20-27 (in Chinese).
[9] Xu Y, Liu J, Song Z M, et al. On semantics of Lvalued first-order logic Lvfl [J]. International Journal of General Systems, 2000, 29(1): 53-79.
[10] Xu Y, Song Z M, Qin K Y, et al. Syntax of Lvalued first-order logic Lvfl [J]. International Journal of Multiple-Valued Logic, 2001, 7: 213-257.
[11] Xu Y, Ruan D, Qin K, et al. Lattice-valued logic: An alternative approach to treat fuzziness and incomparability [M]. Berlin: Springer-Verlag, 2003.
[12] Xu Y, Ruan D, Kerre E E, et al. α-resolution principle based on lattice-valued propositional logic LP(X)[J]. Information Sciences, 2000, 130(1-4): 195-223.
[13] Xu Y, Ruan D, Kerre E E, et al. α-Resolution principle based on first-order lattice-valued logic LF(X)[J]. Information Sciences, 2001, 132(1-4): 221-239.
[14] Xu W T, Xu Y, Deng W H, et al. Ideal-based resolution principle for lattice-valued propositional logic LP(X) [C]// Proceedings of the 4th International Intelligent
Systems and Knowledge Engineering Conference.Singapore: World Scientific, 2009: 601-606.
[15] Xu Y, Liu J, Ruan D, et al. Determination of α-resolution in lattice-valued first-order logic LF(X) [J].Information Sciences, 2011, 181(10): 1836-1862.
