Abstract
Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.
Article PDF
Avoid common mistakes on your manuscript.
References
J.P. Robinson, A machine-oriented logic based on the resolution principle, J. ACM 12 (1965), 23–41.
Johan van Benthem and Alice ter Meulen, Handbook of Logic and Language, 2rd edition, Elsevier, 2010.
W. Bibel, Early history and perspectives of automated deduction. Proc. of the 30th Annual German Conference on AI, Osnabruck, Germany, September 10–13, 2007, pages 2–18.
M. Davis, The early history of automated deduction, in: A. Robinson and A. Voronkov eds.: “Handbook of Automated Reasoning”, pages: 5–15.
D. Plaisted, History and prospects for first-order automated deduction, Proceedings of the 25th International Conference on Automated Deduction, Berlin, Germany, August 1–7 2015, pp. 3–28.
S.H. Muggleton, Alan Turing and the development of Artificial Intelligence, AI communications, forthcoming, 2013.
S.H. Muggleton and L. De Raedt. Inductive logic programming: Theory and methods. Journal of Logic Programming, 19, 20 (1994), 629–679.
S.H. Muggleton, L. De Raedt, D. Poole, I. Bratko, P. Flach, and K. Inoue. ILP turns 20: biography and future challenges. Machine Learning, 86(1) (2011), 3–23.
S. H. Lee, N. Van, Danny, Yang, Kyung-Ae Lee, In-Hee Zhang, B. T. Park, H. Tai. Biomolecular theorem proving on a chip: a novel microfluidic solution to a classical logic problem, Lab Chip, 12 (2012), 1841–1848.
S. G. Naveen, L. John, B. Selmer, Small Steps toward Hypercomputation via Infinitary Machine Proof Verification and Proof Generation, Unconventional Computation and Natural Computation, 7956 (2013), 102–112.
C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard. Using first-order theorem provers in the Jahob data structure verification system. In: Verification, Model Checking, and Abstract Interpretation (pp. 74–88). Springer Berlin Heidelberg.
B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. In: Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on (pp. 331–340). IEEE.
C. Green, The application of theorem proving to question-answering systems Ph.D. thesis, Stanford University, Stanford, 1969.
U. Furbach, I. Glöckner, and B. Pelzer, An application of automated reasoning in natural language question answering, AI Communications, 23 (2–3)( 2010), 241–265.
Y. Xu, J. Liu, D. Ruan, and T.T. Lee, On the consistency of rule-bases based on lattice–valued first-order logic LF(X), International Journal of Intelligent System, 21 (2006), 399–424.
X.H. Wang, X.H. Liu, Generalized resolution, Chinese journal of computers, 2 (1982), 81–92 (in Chinese).
Z. Stachniak, Resolution Proof Systems: An Algebraic Theory, Kluwer Academic Publisher, Netherlands, 1996.
Z. Stachniak, Non-Clausal Reasoning with Definite Theories, Fundamenta Informaticae, 48 (2001), 1–26.
N. Murray, Completely non-clausal theorem proving. Artificial Intelligence, 18 (1982), 67–85.
R. Hahnle, Automated deduction in multiple-valued logics, 1993, Oxford University Press, Inc.
H. Habiballa, Non-clausal resolution - theory and practice. Research report: University of Ostrava, 2000.
Y. Xu, Lattice implication algebras, J. Southwest Jiaotong University, 89(1) (1993), 20–27 (in Chinese).
Y. Xu, D. Ruan, K.Y. Qin, and J. Liu, Lattice-Valued Logic: An Alternative Approach to Treat Fuzziness and Incomparability, Springer-Verlag, Berlin, 2003.
Y. Xu, J. Liu, X.M. Zhong, and S.W. Chen, Multi-ary α-resolution principle for a lattice-valued logic, IEEE Transactions on Fuzzy Systems, 21 (5) (2013), 898–912.
Y. Xu, D. Ruan, E.E. Kerre, and J. Liu, α-Resolution principle based on lattice-valued propositional logic LP(X). Information Sciences, 130(2000), 195–223.
Y. Xu, D. Ruan, E.E. Kerre, and J. Liu, α-Resolution principle based on lattice-valued first-order lattice-valued logic LF(X), Information Science, 132 (2001), 221–239.
Y. Xu, W. T. Xu, X. M. Zhong and X. X. He, α-Generalized Resolution Principle Based on Lattice-Valued Propositional Logic System LP(X), in Proc. of the 9th International FLINS Conference on Foundations and Applications of Computational Intelligence (FLINS2010), 66–71.
Y. Xu, J. Liu, D. Ruan, and X.B. Li, Determination of α-resolution in lattice-valued first-order logic LF(X), Information Sciences, 181 (2011), 1836–1862.
Y Xu, J. Liu, X.X. He, X.M. Zhong, and S.W. Chen, Non-clausal multi-ary α-generalized resolution principle for a lattice-valued propositional logic, Proceeding of the 11th International FLINS Conference on Decision Making and Soft Computing (FLINS2014)/9th International Conference on Intelligent Systems and Knowledge Engineering (ISKE 2014), Joao Pessoa, Brazil, August 17–20, 2014, pp. 197–202.
Y Xu, J. Liu, X.X. He, X.M. Zhong, and S.W. Chen, Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic, IEEE Proceeding of the 10th International Conference on Intelligent Systems and Knowledge Engineering (ISKE2015), 24–27 Nov. 2015, Taipei, Taiwan, pp. 1–7.
W.T. Xu, W.Q. Zhang, D.X. Zhang, Y. Yang, X.D. Pan, α -Resolution method for lattice-valued Horn generalized clauses in lattice-valued propositional logic systems, International Journal of Computational Intelligence Systems, 2015(8): pp 75–84.
X.M. Zhong, Y. Xu, J. Liu, and S.W. Chen, General form of alpha-resolution based on linguistic truth-valued lattice-valued logic, Soft Computing Journal, Vol. 16, 2012, pp. 1767–1781.
Y. Liu, Y. Xu, X.M. Zhong, Multi-ary α -semantic resolution automated reasoning based on lattice-valued first-order logic LF(X), Journal of Intelligent and Fuzzy Systems, 29(4)(2015): pp 1581–1593.
J. A. Goguen, L-type Fuzzy Sets, J. Math. An. Appl., 18 (1967), 145–174.
J. A. Goguen, The logic of inexact concepts, Synthese, 19(1968/69), 325–373.
J. Pavelka, On fuzzy logic I: Many-valued rules of inference, II: Enriched residuated lattices and semantics of propositional calculi, III: Semantical completeness of some many-valued propositional calculi, in: Zeitschr. F. Math. Logik und Grundlagend. Math, 25(1979), 45–52, 119–134, 447–464.
S. Gottwald, A Treatise on Many-Valued Logics. Studies in Logic and Computation, Vol. 9, Research Studies Press Ltd., Baldock, 2001.
L. Bolc, P. Borowik, Many-Valued Logics, Springer, Berlin, 1992.
V. Novak. Fuzzy Sets and Their Applications. Bristol: Adam Hilger, 1989.
V. Novak, I. Perfilieva, and J. Mockor. Mathematical Principles of Fuzzy Logic, Dordrecht: Kluwer, 2000.
P. Hajek, Metamathematics of fuzzy logic. Kluwer Academic Publishers - Dordrecht, 2000.
R. Cignoli, I. D’Ottaviano, and D. Mundici. Algebraic Foundations of Many-valued Reasoning, Dordrecht: Kluwer, 2000.
G. Birkhoff, Lattice Theory, 3rd edition, American Mathematical Society, Providence, R.L., 1967.
C.C. Chang, Algebraic analysis of many valued logic. Trans. Amer. Math. Soc., 88 (1958), 467–490.
R. Hahnle, Many-valued logic and mixed integer programming, Annals of Mathematics and Artificial Intelligence 12 (3–4)(1994), 231–263
P. Kullmann, S. Sandri, An annotated logic theorem prover for an extended possibilistic logic, Fuzzy Sets and Systems 144 (1) (2004) 67–91.
D. Guller, Binary resolution over Boolean lattices, Fuzzy Sets and Systems 157(2006), 2100–2127.
D. Guller, Binary resolution over complete residuated stone lattices, Fuzzy Sets and Systems, 159(2008), 1031–1041.
J. Ignjatović, M. Ćirić, and S. Bogdanović, Determinization of fuzzy automata with membership values in complete residuated lattices, Information Sciences, 178 (1)(2008), 164–180.
D. Guller, On the refutational completeness of signed binary resolution and hyperresolution, Fuzzy Sets and Systems, 160 (8)(2009), 1162–1176.
M. Banibrata and S. Raha. Approximate reasoning in fuzzy resolution, Fuzzy Information Processing Society (NAFIPS), 2012 Annual Meeting of the North American. IEEE.
M. Banibrata and S. Raha, Fuzzy resolution with similarity-based reasoning. Recent Developments and New Directions in Soft Computing. Springer International Publishing, 2014, pp. 361–378.
C. Ansótegui, M. Bofill, F. Manyà, & M. Villaret, S AT and SMT technology for many-valued logics. Journal of Multiple-Valued Logic & Soft Computing, 24(1–4)(2015), pp. 151–172.
C. Ansótegui, M. Bofill, F. Manyà, & M. Villaret, Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers, Fuzzy Sets and Systems, 292(1)(2016), pp. 32–48.
X.H. Liu, Resolution-Based Automated Reasoning, Academic Press, Bei**g, China, 1994 (in Chinese).
V. Loia, S. Senatore and M.I. Sessa, Similarity-based SLD resolution and its role for web knowledge discovery, Fuzzy Sets and Systems, 144 (1)(2004), 151–171.
J.J. Lu, N.V. Murray, E. Rosenthal, A framework for automated reasoning in multiple-valued logics, Journal of Automated Reasoning 21 (1998) 39–67.
J. Medina and M. Ojeda-Aciego, Multi-adjoint t-concept lattices, Information Sciences, 180 (5) (2010), 712–725.
S. Lehmke. A resolution-based axiomatisation of ‘bold’ propositional fuzzy logic. In: Fuzzy Sets, Logics, and Reasoning about Knowledge (Eds. by D. Dubois, E. P. Klement, and H. Prade), Kluwer Academic Publishers, Applied Logic, 1999.
C.S. Kim, D.S. Kim, J.S. Park, A new fuzzy resolution principle based on the antonym, Fuzzy Sets and Systems 113 (2) (2000) 299–307.
J. Liu, D. Ruan, Y. Xu, Z.M. Song, A resolution-like strategy based on a lattice-valued logic, IEEE Transactions on Fuzzy Systems, 11 (4) (2003), 560–567.
J. Hoffmann, Finding a tree structure in a resolution proof is NP-complete, Theoretical Computer Science, 410 (21–23)(2009), 2295–2300.
L. Di Lascio and A. Gisolfi, Graded tableaux for Rational Pavelka Logic, International Journal of Intelligent Systems, 20(12) (2005), 1273–1285.
P. Hofner and G. Struth, Automated reasoning in kleene algebra, In CADE 2007, F. Pfennig (ed.), LNCS 4603, 2007, pp. 279–294.
X.X. He, Y. Xu, J. Liu, D. Ruan, α-Lock resolution method for lattice-valued logic based on lattice implication algebra, Engineering Applications of Artificial Intelligence, Vol. 24, 2011, 1274–1280.
X.X. He, J. Liu, Y. Xu, L. Martinez, and D. Ruan, On α-satisfiability and its α-Lock resolution in a finite lattice-valued logic, Logic Journal of the IGPL, Logic Journal of IGPL, 20(3)(2011), 579–588.
X.X. He, Y. Xu, J. Liu, S.W. Chen, On compatibilities of α-lock resolution method in linguistic truth-valued lattice-valued logic, Soft Computing Journal, 16(4)(2012), pp. 699–709.
X.X. He, J. Liu, Y. Xu, L. Martinez, and D. Ruan, On α-satisfiability and its α-Lock resolution in a finite lattice-valued logic, Logic Journal of the IGPL, 20(3)(2012), pp. 579–588.
X.X. He, Y. Xu, J. Liu, S.W. Chen. A unified algorithm for finding k-IESFs in linguistic truth-valued lattice-valued propositional logic, Soft Computing, 18(11)(2014), pp. 2135–2147.
X.X. He, Y. Xu, J. Liu, α -Lock paramodulation for lattice-valued propositional logic, International Conference on Intelligent Systems and Knowledge Engineering (ISKE 2015), 24 Nov – 27 Nov, 2015, Taibei, pp 18–20
X.M. Zhong, Y. Xu, J. Liu, S.W. Chen, α-Quasi-lock semantic resolution method based on lattice-valued logic. International Journal of Computational Intelligence Systems, 7(3)(2014): 418–431.
X.M. Zhong and Y. Xu, alpha- group quasi-lock semantic resolution method based on lattice-valued propositional logic LP(X). Multiple-Valued Logic and Soft Computing 22(4–6)(2014): 581–598.
H.R. Jia, Y. Xu, Y. Liu, and J. Liu, Alpha-minimal resolution principle for a lattice-valued logic, International Journal of Computational Intelligence Systems, Vol. 8. No. 1, 2015, pp. 34–43.
S. Schockaert, J. Janssen, and D. Vermeir, Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction, Journal of Automated Reasoning, 49(2012), pp. 493–550.
D. Smutná-Hlinĕná and P. Vojtáš, Graded many-valued resolution with aggregation, Fuzzy Sets and Systems, 143 (2004), 157–168.
V. Sofronie-Stokkermans, Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators, Multiple-Valued Logic—An International Journal, 6(3–4) (2001), 289–344.
V. Sofronie-Stokkermans and C. Ihlemann, Automated reasoning in some local extensions of ordered structures, Journal of Multiple-Valued Logic and Soft Computing, 13(4–6) (2007), 397–414.
F. Liu, Tabulation proof procedures for fuzzy linguistic logic programming, International Journal of Approximate Reasoning, 63(2015), pp. 62–88.
J. Ma, W.J. Li, D. Ruan, Y Xu, Filter-based resolution principle for lattice-valued propositional logic LP(X), Information Sciences, 177 (2007), 1046–1062.
T.D. Khang, A resolution method for linguistic many-valued logic. Applied Mathematics & Information Sciences, 7(3)(2013), pp. 1193.
M. Kifer and V.S. Subrahmanian, Theory of generalized annotated logic programming and its applications, Journal of Logic Programming, 12(4)(1992): 335–367.
E. Komendantskaya, A.K. Seda, Sound and complete SLD-resolution for bilattice-based annotated logic programs, Electronic Notes in Theoretical Computer Science 2009, 225, 141–159.
M. Fitting, Bilattices and the semantics of logic programming. Journal of Logic Programming, 11(1991): 91–116.
F. Bacchus, Representing and Reasoning with Probabilistic Knowledge: A Logical Approach to Probabilities, 1991, MIT Press Cambridge, MA, USA.
P. Julián-Iranzo and C. Rubio-Manzano, A sound and complete semantics for a similarity-based logic programming language, Fuzzy Sets and Systems 317(15)(2017): 1–26.
Z. Pei, D. Ruan, J. Liu, Y. Xu, Linguistic Values-based Intelligent Information Processing: Theory, Methods, and Applications, Atlantis Press, 2009.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
This is an open access article under the CC BY-NC license (https://doi.org/creativecommons.org/licenses/by-nc/4.0/).
About this article
Cite this article
Xu, Y., Liu, J., He, X. et al. Non-Clausal Multi-ary α-Generalized Resolution Calculus for a Finite Lattice-Valued Logic. Int J Comput Intell Syst 11, 384–401 (2018). https://doi.org/10.2991/ijcis.11.1.29
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.2991/ijcis.11.1.29