Multi-ary α-ordered linear minimal resolution method in lattice-valued logic system 1

Abstract

On the basis of α-minimal resolution principle, an α-n(t)-ary resolution dynamic automated reasoning method—multi-ary α-ordered linear minimal resolution method is studied in lattice-valued propositional logic system LP(X) and lattice-valued first-order logic system LF(X) based on lattice implication algebra (LIA). Firstly, multi-ary α-ordered linear minimal resolution method is established in LP(X), while its theorems of both soundness and completeness are proved. Then, multi-ary α-ordered linear minimal resolution method is further established in the corresponding lattice-valued first-order logic LF(X), along with its soundness theorem, lifting lemma, and completeness theorem. Then, the validity of multi-ary α-ordered linear minimal resolution based on lattice-valued logic is analyzed. At last, an multi-ary α-ordered linear minimal resolution algorithm in LP(X) is designed, and it is proved to be sound and complete, then it is further extended in the corresponding LF(X). This lays the foundation for the further study on α-n(t)-ary resolution dynamic automated reasoning program.

Keywords

Lattice implication algebra lattice-valued logic system resolution dynamic automated reasoning α-minimal resolution

Get full access to this article

View all access options for this article.

References

Robinson

J.A.

, A machine-oriented logic based on the resolution principle [J], Journal of the Association for Computing Machinery 12(1) (1965), 23–41.

Chang

C L.

Lee

R.C.T.

and Symbolic logic and mechanical theorem proving [M]. New York: Academic Press; 1973.

Loveland

D.W.

, Automated theorem proving: A logical basis [M]. Amsterdam, North-Holland; 1978.

Luckham

, Refinements in resolution theory, Proc. IRIA Symp. Automatic Demonstration, Spring-Verlag, New York; 1970, 163–190.

Sofronie

V.S.

Ihlemann

, Automated reasoning in some local extensions of ordered structures [J], Journal of Multiple-Valued Logic and Soft Computing 13(4-6) (2007), 397–414.

Liu

X.H.

, Resolution-based Automated Reasoning [M]. Beijing: Academic Press of China; 1994 (in Chinese).

, Ruan

and Qin

K.Y.

, et al. Lattice-valued logic–an alternative approach to treat fuzziness and incomparability, Berlin: Springer-Verlag; 2003.

, Ruan

and Kerre

E.E.

, et al. α-resolution principle based on lattice-valued propositional logic LP(X) [J], Information Sciences 130 (2000), 195–223.

, Ruan

and Kerre

E.E.

, et al. α-resolution principle based on lattice-valued first-order lattice-valued logic LF(X) [J], Information Sciences 132 (2001), 221–239.

10.

, Liu

and Zhong

X.M.

, et al. Multi-ary α-resolution principle for a lattice-valued logic[J], IEEE Transactions On Fuzzy Systems 21(5) (2013), 898–912.

11.

Pavelka

On fuzzy logic I: Many-valued rules of in-frence, II: Enriched residuated lattices and Semantics of propositional calculi, III: antical completeness of some many-valued propositional calculi [J]. in: Zeitschr. F.Math, Logik und Grundlagend Math 25 (1979), 45–52, 119–134, 447-464.

12.

, Chen

S.W.

and Ma

, Linguistic truth-valued lattice implication algebra and its properties [C] Proc. IMACS Multiconference on “Computational Engineering in Systems Applications” (CESA 2006). Beijing, China; 2006, 1413–1418.

13.

, Chen

S.W.

and Liu

, et al. Weak completeness of resolution in a linguistic truth-valued prepositional logic [C] Proc. IFSA2007: Theoretical Advances and Applications of Fuzzy Logic and Soft Computing, Cancun, Mexico; 2007, 358–366.

14.

X.B.

, Qiu

X.P.

and Chang

Z.Y.

, et al. The properties of α-resolution and J-resolution based on lattice-valued prepositional logic system [J], Chinese Quarterly Journal of Mathematics 6 (2008), 262–269 (in Chinese).

15.

Jia

R.H.

, Xu

and Liu

, α-Minimal resolution principle for a lattice-valued logic [J], Computational Intelligence Systems 8(1) (2015), 34–43.

16.

, Lattice implication algebras [J], Journal of Southwest Jiaotong University 89(1) (1993) 20–27 (in Chinese).

17.

and Qin

K.Y.

, Lattice-valued propositional logic(I) [J], Journal of Southwest Jiaotong University 1(1) (1993) 123–128 (English version).

18.

Qin

K.Y.

, Xu

and Song

Z.M.

, Lattice-valued propositional logic LP(X) (I) [J], Fuzzy Systems and Mathematics 11(4) (1997) 5–10 (in Chinese).

19.

T.W.

and Xu

, α-Ordered linear resolution for lattice-valued logic system based on lattice implication algebra [J], International Journal of Applied Management Science 4(4) (2012), 460–479.

20.

, Zhong

X.M.

, He

X.X.

, et al. Research advances on resolution automated reasoning in lattice-valued logic based on lattice implication algebra [C] The 10th International FLINS Conference on Uncertainty Modeling in Knowledge Engineering and Decision Making (FLINS2012), Istanbul, Turkey, 2012, 714–721.

21.

Jia

H.R.

, He

H.C.

, Xu

, et al. α-Ordered linear minimal resolution method in lattice-valued propositional logic system LP(X) [C] The 11th International FLINS Conference on Decision Making and Soft Computing (FLINS 2014), Paraíba, Brazil; 2014, 191–196.

22.

Liu

, Xu

and Zhong

X.M.

, Multi-ary α-semantic resolution automated reasoning based on lattice-valued first-order logic LF(X) [J], Journal of Intelligent & Fuzzy Systems 29(4) (2015), 1581–1593.