×

zbMATH — the first resource for mathematics

Filter-based resolution principle for lattice-valued propositional logic LP\((X)\). (English) Zbl 1114.03019
Summary: As one of the most powerful approaches in automated reasoning, the resolution principle has been introduced to nonclassical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logics are a kind of important nonclassical logics, which can be applied to describe and handle incomparability by the incomparable elements in its truth-value field. In this paper, a filter-based resolution principle for the lattice-valued propositional logic LP\((X)\) based on a lattice implication algebra is presented, where the filter of the truth-value field, being a lattice implication algebra, is taken as the criterion for measuring the satisfiability of a lattice-valued logical formula. The notions and properties of lattice implication algebra, filter of lattice implication algebra, and the lattice-valued propositional logic LP\((X)\) are given first. The definitions and structures of two kinds of lattice-valued logical formulae, i.e., the simple generalized clauses and complex generalized clauses, are presented then. Finally, the filter-based resolution principle is given, and after that the soundness theorem and weak completeness theorem for the presented approach are proved.

MSC:
03B52 Fuzzy logic; logic of vagueness
03B35 Mechanization of proofs and logical operations
Software:
DISCOUNT; OTTER; CLIN
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aguilera, G.; de Guzmán, L.; Ojeda-Aciego, M.; Valverde, A., Reductions for non-clausal theorem proving, Theor. comput. sci., 266, 81-112, (2001) · Zbl 0989.68128
[2] Baaz, M.; Leitsch, A., Complexity of resolution proofs and function introduction, Ann. pure appl. logic, 57, 181-215, (1992) · Zbl 0769.03009
[3] Baaz, M.; Fermüller, C.G., Resolution-based theorem proving for many-valued logics, J. symbol. comput., 19, 353-391, (1995) · Zbl 0839.68091
[4] Buro, M.; Büning, H., On resolution with short clauses, Ann. math. artif. intell., 18, 243-260, (1996) · Zbl 0892.03004
[5] Cárdenas Viedma, I.N.S.M.A.; Marín Morales, R., Fuzzy temporal constraint logic: a valid resolution principle, Fuzzy sets syst., 117, 231-250, (2001) · Zbl 0984.03021
[6] Chang, C.; Lee, R., Symbolic and mechanical theorem proving, (1973), Academic Press New York · Zbl 0263.68046
[7] Chu, H.; Plaisted, D., CLIN-S—A semantically guided first-order theorem prover, J. automat. reason., 18, 183-188, (1997)
[8] Denzinger, J.; Kronenburg, M.; Schulz, S., DISCOUNT—A distributed and learning equational prover, J. automat. reason., 18, 189-198, (1997)
[9] Dixon, C., Temporal resolution using a breadth-first search algorithm, Ann. math. artif. intell., 22, 87-115, (1998) · Zbl 0976.03010
[10] D. Dubois, J. Lang, H. Prade, Theorem proving under uncertainty—a possibility theory based approach, in: Proc. of the International Joint Conference on Artificial Intelligence (IJCAI’87), Mitano, Italy, 1987, pp. 984-986.
[11] D. Dubois, J. Lang, H. Prade, Automated reasoning using possibility logic semantics, belief revision and variable certainty weights, in: Proc. of the Fifth Workshop on Uncertainty in Artificial Intelligence, Windor, Ont., 1989, pp. 81-87.
[12] Dubois, D.; Prade, H., Resolution principle in possibilistic logic, Internat. J. approx. reason., 4, 1, 1-21, (1990) · Zbl 0697.68083
[13] Fermüller, C.; Leitsch, A., Model building by resolution, (), 134-148 · Zbl 0788.68128
[14] Formisano, A.; Polocriti, A., T-resolution: refinements and model elimination, J. automat. reason., 22, 433-483, (1999) · Zbl 0929.68112
[15] Franco, J.; Gelder, A.V., A perspective on certain polynomial-time solvable classes of satisfiability, Discr. appl. math., 125, 177-214, (2003) · Zbl 1012.68085
[16] Gabbay, D.M.; Reyle, U., Labelled resolution for classical and non-classical logics, Stud. log., 59, 179-216, (1997) · Zbl 0976.03012
[17] Genesereth, M.R.; Nilsson, N.J., Logical foundations of artificial intelligence, (1987), Morgan Kaufmann San Mateo, CA · Zbl 0645.68104
[18] Giunchiglia, E.; Narizzano, M.; Tacchella, A., Back jumping for quantified Boolean logic satisfiability, Artif. intell., 145, 99-120, (2003) · Zbl 1082.68795
[19] Gottwald, S., A treatise on many-valued logics, Studies in logic and computation, vol. 9, (2001), Research Studies Press Baldock · Zbl 1048.03002
[20] Hähnle, R., Automated deduction in multiple-valued logics, (1993), Oxford University Press Oxford · Zbl 0798.03010
[21] Hähnle, R., Commodious axiomatization of quantifiers in multiple-value logic, Stud. log., 61, 1, 101-121, (1998) · Zbl 0962.03018
[22] Hájek, P., Metamathematics of fuzzy logic, (1998), Kluwer Academic Publishers Dordrecht · Zbl 0937.03030
[23] Kalla, P.; Zeng, Z.; Ciesielski, M.J., Strategies for solving the Boolean satisfiability problem using binary decision diagrams, J. syst. architect., 47, 491-503, (2001)
[24] M. Kifer, On the expressive power of annotated logic program, in: Proc. of the 1989 North American Conference on Logic Programming, Cleveland, OH, 1989, pp. 1069-1089.
[25] M. Kifer, E. Lozinskii, RI: A logic for reasoning with inconsistency, in: Proc. of the 21st International Symposium on Multiple-Valued Logics (ISMVL’91), Victoria, BC, Canada, 1991, pp. 253-262. · Zbl 0717.03005
[26] Kim, C.S.; Kim, D.S.; Park, J.S., A new fuzzy resolution principle based on the antonym, Fuzzy sets and syst., 113, 299-307, (2000) · Zbl 0951.68148
[27] Kirousis, L.M.; Kolaitis, P.G., The complexity of minimal satisfiability problems, Inform. comput., 187, 20-39, (2003) · Zbl 1082.68036
[28] Lee, S.J.; Plaisted, D.A., Eliminating duplication with the hyper-linking strategy, J. automat. reason., 9, 25-42, (1992) · Zbl 0784.68077
[29] Letz, R., LINUS-A link instantiation prover with unit support, J. automat. reason., 18, 205-210, (1997)
[30] Liu, J.; Xu, Y., Filter and structure of lattice implication algebra, Chin. sci. bull., 10, 1049-1052, (1997)
[31] J. Liu, Study on lattice-valued logic system and lattice-valued resolution principle, Ph.D. thesis, Southwest Jiaotong University, Chengdu, China, 1999.
[32] Liu, X., Resolution-based automated reasoning, (1994), Chinese Academic Press
[33] Loveland, D.W., Mechanical theorem proving by model elimination, ACM trans. math. software, 15, 2, 236-251, (1968) · Zbl 0162.02804
[34] J.J. Lu, N.V. Murray, E. Rosenthal, Signed formulas and annotated logics, in: Proc. of the 23rd International Symposium on Multiple-Valued Logics (ISMVL’93), 1993, pp. 48-53.
[35] J.J. Lu, N.V. Murray, E. Rosenthal, Signed formulas and fuzzy operator logics, in: J. Komorowski, Z.W. Ras (Eds.), Proc. of the Seventh International Symposium on Mathodologies for Intelligent Systems (ISMIS’93), 1993, pp. 75-84.
[36] Lu, J.J.; Murray, N.V.; Rosenthal, E., A framework for reasoning in multiple-valued logics, J. automat. reason., 21, 1, 39-67, (1998) · Zbl 0913.03023
[37] Łukasiewicz, J., Selected works, (1970), North-Holland Amsterdam · Zbl 0212.00902
[38] J. Ma, Study on lattice implication algebra and lattice-valued propositional logic LP(X), Master’s thesis, Southwest Jiaotong University, Chengdu, China, 1999.
[39] J. Ma, Lattice-valued logical system and automated reasoning based on lattice implication algebra, Ph.D. thesis, Southwest Jiaotong University, Chengdu, China, 2002.
[40] W. McCune, OTTER 3.0 reference manual and guide, Tech. Rep. Tech. Rep. ANL-94/6, Argonne National Laboratory, 1994. Available from: <http://www-unix.mcs.anl.gov/AR/otter/>.
[41] Morgan, C., Resolution for many-valued logics, Logique et anal. (N.S.), 19, 311-339, (1976) · Zbl 0352.02017
[42] Mukaidono, M., On some properties of fuzzy logic, Systems comput. controls, 6, 2, 36-43, (1975)
[43] Mukaidono, M., Fuzzy inference of resolution style, (), 224-231
[44] Murray, N.V., Completely nonclausal resolution theorem proving, Artif. intell., 18, 1, 67-85, (1982)
[45] N.V. Murray, E. Rosenthal, Improving tableau proof in multiple valued logics, in: Proc. of 21st International Symposium of Multiple-Valued Logics (ISMVL’91), Victoria, BC, Canada, 1991, pp. 230-237.
[46] Nieuwenhuis, R.; Rivero, J.M.V., Barcelona, J. automat. reason., 18, 2, 171-176, (1997)
[47] Nipkow, T.; Paulson, L.C.; Wenzel, M., A proof assistant for higher-order logic, (2003), Springer New York
[48] Novák, V.; Perfilieva, I.; Močkoř, J., Mathematical principles of fuzzy logic, (1999), Kluwer Academic Publication Boston · Zbl 0940.03028
[49] Orlowska, E., The resolution principle for ω+-valued logic, Fund. inform., 2, 1, 1-15, (1978) · Zbl 0433.03006
[50] Orlowska, E., Resolution system and their application II, Fund. inform., 3, 3, 333-362, (1980)
[51] Orlowska, E., Mechanical proof methods for post logics, Logique et anal. (N.S.), 28, 110, 173-192, (1985) · Zbl 0587.03007
[52] Pavelka, J., On fuzzy logic I: many-valued rules of inference, Z. math. logik grundlagen math., 25, 45-52, (1979), 119-134, 447-464 · Zbl 0435.03020
[53] Policriti, A.; Schwartz, J.T., T theorem proving I, J. symbolic comput., 20, 315-342, (1995) · Zbl 0851.68101
[54] Post, E.L., Introduction to a general theory of elementary propositions, Amer. J. math., 43, 163-185, (1921) · JFM 48.1122.01
[55] K. Qin, Study of lattice-valued logic system and its application based on lattice implication algebra, Ph.D. thesis, Southwest Jiaotong University, Chengdu, China, 1996.
[56] Robinson, J.A., A machine-oriented logic based on the resolution principle, J. ACM, 12, 23-41, (1965) · Zbl 0139.12303
[57] Russell, S.; Norvig, P., Artificial intelligence: A modern approach, (1995), Prentice-Hall New Jersey · Zbl 0835.68093
[58] Salzer, G., Optimal axiomatizations for multiple-valued operators and quantifiers based on semilattices, (), 688-702 · Zbl 1415.03030
[59] Schmidt, R., Decidability by resolution for propositional model logics, J. automat. reason., 22, 376-396, (1999) · Zbl 0924.68178
[60] Schmitt, P., Computational aspects of three-valued logic, (), 190-198
[61] Smutná-Hliněná, D.; Vojtáš, P., Graded many-valued resolution with aggregation, Fuzzy sets syst., 143, 157-168, (2004) · Zbl 1054.03021
[62] Z. Song, Study of uncertainty reasoning based on lattice implication algebra in intelligent control, Ph.D. thesis, Southwest Jiaotong University, Chengdu, China, 1998.
[63] Stachniak, Z., Resolution proof systems: an algebraic theory, (1996), Kluwer Academic Publishers Dordrecht · Zbl 0849.03010
[64] Sofronie-Stokkermans, V., Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators, Mult.-valued log., 6, 3/4, 289-344, (2001) · Zbl 1019.03003
[65] Sutcliffe, G.; Suttner, C., Evaluat. general purpose automat. theorem proving syst., 131, 39-54, (2001) · Zbl 0996.68182
[66] Wang, G., MV-algebras, BL-algebras, R0-algebras, and multiple-valued logic, Fuzzy syst. math., 16, 2, 1-15, (2002) · Zbl 1333.06029
[67] X. Wang, Study on lattice-valued logic based on lattice implication algebra and its model theory, Ph.D. thesis, Southwest Jiaotong University, Chengdu, China, 2004.
[68] Warners, J.P.; van Maaren, H., A two-phase algorithm for solving a class of hard satisfiability problems 1, Oper. res. lett., 23, 81-88, (1998) · Zbl 0960.90100
[69] L. Wos, D. Carson, G. Robinson, The unit preference strategy in theorem proving, in: Proc. of the Fall Joint Computer Conference, 1964, pp. 615-621. · Zbl 0135.18306
[70] Wos, L.; Carson, D.; Robinson, G., Efficiency and completeness of the set-of-support strategy in theorem proving, ACM trans. math. software, 12, 536-541, (1965) · Zbl 0135.18401
[71] Xu, Y., Lattice implication algebra, J. southwest jiaotong univ., 28, 1, 20-27, (1993) · Zbl 0784.03035
[72] Xu, Y.; Qin, K., Lattice-valued propositional logic (I), J. southwest jiaotong univ., 2, 123-128, (1993), (English version) · Zbl 0807.03020
[73] Xu, Y.; Qin, K., Lattice-valued propositional logic (II), J. southwest jiaotong univ., 1, 22-27, (1994), (English version) · Zbl 0824.03009
[74] Xu, Y.; Qin, K.; Song, Z., Syntax of lattice-valued first-order logic FM, Chin. sci. bull., 10, 1052-1055, (1997)
[75] Xu, Y.; Qin, K.; Liu, J.; Song, Z., L-valued propositional logic lvpl, Inform. sci., 114, 205-235, (1999) · Zbl 0936.03023
[76] Xu, Y.; Liu, J.; Song, Z.; Qin, K., On semantics of L-valued first-order logic lvfl, Internat. J. gen. systems, 29, 53-79, (2000) · Zbl 0953.03028
[77] Xu, Y.; Ruan, D.; Kerre, E.E.; Liu, J., α-resolution principle based on lattice-valued propositional logic LP(X), Inform. sci., 130, 1-29, (2000)
[78] Xu, Y.; Song, Z.; Qin, K.; Liu, J., Syntax of L-valued first-order logic lvfl, Mult.-valued log., 7, 213-257, (2001) · Zbl 1003.03525
[79] Xu, Y.; Ruan, D.; Kerre, E.E.; Liu, J., α-resolution principle based on first-order lattice-valued logic LF(X), Inform. sci., 132, 221-239, (2001) · Zbl 0997.03006
[80] Xu, Y.; Ruan, D.; Qin, K.; Liu, J., Lattice-valued logic—an alternative approach to treat fuzziness and incomparability, (2003), Springer New York · Zbl 1048.03003
[81] Yager, R.R., Inference in a multiple-valued logic system, Internat. J. man – machine studies, 23, 27-44, (1985) · Zbl 0581.03015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.