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.
Keywords:
resolution principle; filter; lattice-valued logic; automated reasoning; simple generalized clause; complex generalized clause; lattice-implication algebraReferences:
| [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: 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.; 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.; 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, (Proc. of 6th Workshop on Computer Science Logic (CSL’92). Proc. of 6th Workshop on Computer Science Logic (CSL’92), Lecture Notes in Computer Science, vol. 702 (1993), Springer: Springer New York), 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: 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: Research Studies Press Baldock · Zbl 1048.03002 |
| [20] | Hähnle, R., Automated Deduction in Multiple-Valued Logics (1993), Oxford University Press: 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: 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.; 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.; 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.; 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.; 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.; 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: North-Holland Amsterdam · Zbl 0212.00902 |
| [38] | J. Ma, Study on lattice implication algebra and lattice-valued propositional logic LP \((X\); J. Ma, Study on lattice implication algebra and lattice-valued propositional logic LP \((X\) |
| [39] | J. Ma, Lattice-valued logical system and automated reasoning based on lattice implication algebra, Ph.D. thesis, Southwest Jiaotong University, Chengdu, China, 2002.; 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/>; 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, (Yager, R. R., Fuzzy Sets and Possibility Theory (1982), Pergamon Press: Pergamon Press New York), 224-231 |
| [44] | Murray, N. V., Completely nonclausal resolution theorem proving, Artif. Intell., 18, 1, 67-85 (1982) · Zbl 0472.68053 |
| [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.; 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: Springer New York |
| [48] | Novák, V.; Perfilieva, I.; Močkoř, J., Mathematical Principles of Fuzzy Logic (1999), Kluwer Academic Publication: 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.; 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: Prentice-Hall New Jersey · Zbl 0835.68093 |
| [58] | Salzer, G., Optimal axiomatizations for multiple-valued operators and quantifiers based on semilattices, (McRobbie, M.; Slaney, J., Proc. 13th Conference on Automated Deduction. Proc. 13th Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 1104 (1996), Springer: Springer New Brunswick, NJ), 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, (Siekmann, J., Proc. of the Eighth International Conference on Automated Reasoning (1986), Springer: Springer Berlin), 190-198 · Zbl 0644.03015 |
| [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.; 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: 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, \(R_0\)-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.; 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.; 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 \(L_{vpl}\), 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 \(L_{vfl}\), 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 \(L_{vfl}\), 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: 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
