The possibilistic Horn non-clausal knowledge bases. (English) Zbl 07629312
Summary: Non-clausal deduction in classical logic is one of the oldest areas in artificial intelligence. It first appeared in the sixties and consequently a large body of research has been devoted to it. Within the last decades, computing with non-clausal formulas has been considered in several fields, and in particular, in answer set programming, wherein non-clausal or nested logic programs were conceived in 1999.
Possibilistic logic is the most extended approach to handle uncertain and partially inconsistent information. Here, we generalize some well-known clausal outcomes in possibilistic reasoning to the non-clausal setting, concretely the objective of our proposal is: (i) to extend available insights from clausal to non-clausal form; (ii) to show that possibilistic reasoning admits feasible classes also at the non-clausal level; (iii) to combine the high expressiveness of non-clausal possibilistic logic with the highest efficient (polynomial) reasoning mechanisms; and (iii) to suggest that some meaningful subclasses of possibilistic nested programs can be efficiently processed.
Firstly, we define the class of Possibilistic Horn Non-Clausal formulas, or \(\overline{\mathcal{H}}_{\Sigma} \), which covers the classes: possibilistic Horn and propositional Horn-NC. \( \overline{\mathcal{H}}_{\Sigma}\) is shown to be non-clausal, analogous to the standard Horn class.
Secondly, we define Possibilistic Non-Clausal Unit-Resolution, or \(\mathcal{UR}_{\Sigma} \), and prove that \(\mathcal{UR}_{\Sigma}\) correctly computes the inconsistency degree of Horn-NC bases. \( \mathcal{UR}_{\Sigma}\) is formulated in a clausal-like manner, which eases its understanding, formal proofs and future extension towards full non-clausal resolution.
Thirdly, we prove that computing the inconsistency degree of Horn-NC bases takes polynomial time. Although there already exist tractable classes in possibilistic logic, all of them are clausal, and thus, \( \overline{\mathcal{H}}_{\Sigma}\) turns out to be the first characterized polynomial non-clausal class within possibilistic reasoning. We discuss that our approach serves as a starting point to developing uncertain non-clausal reasoning on the basis of both methodologies: DPLL and resolution.
Possibilistic logic is the most extended approach to handle uncertain and partially inconsistent information. Here, we generalize some well-known clausal outcomes in possibilistic reasoning to the non-clausal setting, concretely the objective of our proposal is: (i) to extend available insights from clausal to non-clausal form; (ii) to show that possibilistic reasoning admits feasible classes also at the non-clausal level; (iii) to combine the high expressiveness of non-clausal possibilistic logic with the highest efficient (polynomial) reasoning mechanisms; and (iii) to suggest that some meaningful subclasses of possibilistic nested programs can be efficiently processed.
Firstly, we define the class of Possibilistic Horn Non-Clausal formulas, or \(\overline{\mathcal{H}}_{\Sigma} \), which covers the classes: possibilistic Horn and propositional Horn-NC. \( \overline{\mathcal{H}}_{\Sigma}\) is shown to be non-clausal, analogous to the standard Horn class.
Secondly, we define Possibilistic Non-Clausal Unit-Resolution, or \(\mathcal{UR}_{\Sigma} \), and prove that \(\mathcal{UR}_{\Sigma}\) correctly computes the inconsistency degree of Horn-NC bases. \( \mathcal{UR}_{\Sigma}\) is formulated in a clausal-like manner, which eases its understanding, formal proofs and future extension towards full non-clausal resolution.
Thirdly, we prove that computing the inconsistency degree of Horn-NC bases takes polynomial time. Although there already exist tractable classes in possibilistic logic, all of them are clausal, and thus, \( \overline{\mathcal{H}}_{\Sigma}\) turns out to be the first characterized polynomial non-clausal class within possibilistic reasoning. We discuss that our approach serves as a starting point to developing uncertain non-clausal reasoning on the basis of both methodologies: DPLL and resolution.
MSC:
| 68T37 | Reasoning under uncertainty in the context of artificial intelligence |
References:
| [1] | Aguilera, G.; de Guzman, I.; Ojeda, M., A reduction-based theorem prover for 3-valued logic, Mathw. Soft Comput., 4, 2, 99-127 (1997) · Zbl 0884.03006 |
| [2] | Alsinet, T.; Chesñevar, C. I.; Godo, L.; Simari, G. R., A logic programming framework for possibilistic argumentation: formalization and logical properties, Fuzzy Sets Syst., 159, 10, 1208-1228 (2008) · Zbl 1187.68601 |
| [3] | Alsinet, T.; Godo, L., A complete calculus for possibilistic logic programming with fuzzy propositional variables, (UAI ’00: Proceedings of the 16th Conference in Uncertainty in Artificial Intelligence. UAI ’00: Proceedings of the 16th Conference in Uncertainty in Artificial Intelligence, Stanford University, Stanford, California, USA, June 30 - July 3, 2000 (2000)), 1-10 |
| [4] | Alsinet, T.; Godo, L.; Sandri, S. A., Two formalisms of extended possibilistic logic programming with context-dependent fuzzy unification: a comparative description, Electron. Notes Theor. Comput. Sci., 66, 5, 1-21 (2002) · Zbl 1270.68058 |
| [5] | Bachmair, L.; Ganzinger, H., Resolution theorem proving, (Handbook of Automated Reasoning (2001)), 19-99, (in 2 volumes) · Zbl 0993.03008 |
| [6] | Baral, C., Knowledge Representation, Reasoning and Declarative Solving (2003), Cambridge University Press · Zbl 1056.68139 |
| [7] | Barrett, C. W.; Donham, J., Combining SAT methods with non-clausal decision heuristics, Electron. Notes Theor. Comput. Sci., 125, 3, 3-12 (2005) · Zbl 1272.68370 |
| [8] | Bauters, K.; Schockaert, S.; Cock, M. D.; Vermeir, D., Possible and necessary answer sets of possibilistic answer set programs, (IEEE 24th International Conference on Tools with Artificial Intelligence. IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, Athens, Greece, November 7-9, 2012 (2012)), 836-843 |
| [9] | Bauters, K.; Schockaert, S.; Cock, M. D.; Vermeir, D., Semantics for possibilistic answer set programs: uncertain rules versus rules with uncertain conclusions, Int. J. Approx. Reason., 55, 2, 739-761 (2014) · Zbl 1316.68036 |
| [10] | Beckert, B.; Hähnle, R.; Escalada-Imaz, G., Simplification of many-valued logic formulas using anti-links, J. Log. Comput., 8, 4, 569-587 (1998) · Zbl 0907.03008 |
| [11] | Ben-Ari, M., Mathematical Logic for Computer Science (2012), Springer · Zbl 1248.03001 |
| [12] | Benferhat, S.; Dubois, D.; Prade, H., Possibilistic logic: from nonmonotonicity to logic programming, (Symbolic and Quantitative Approaches to Reasoning and Uncertainty, European Conference, Proceedings. Symbolic and Quantitative Approaches to Reasoning and Uncertainty, European Conference, Proceedings, ECSQARU’93, Granada, Spain, November 8-10, 1993 (1993)), 17-24 |
| [13] | Brewka, G.; Niemelä, I.; Syrjänen, T., Logic programs with ordered disjunction, Comput. Intell., 20, 2, 335-357 (2004) |
| [14] | Bry, F.; Eisinger, N.; Eiter, T.; Furche, T.; Gottlob, G.; Ley, C.; Linse, B.; Pichler, R.; Wei, F., Foundations of rule-based query answering, (Reasoning Web, Tutorial Lectures. Reasoning Web, Tutorial Lectures, Third International Summer School 2007, Dresden, Germany, September 3-7, 2007 (2007)), 1-153 · Zbl 1170.68646 |
| [15] | Bubeck, U.; Kleine Büning, H., Nested boolean functions as models for quantified boolean formulas, (Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Proceedings, Helsinki, Finland, July 8-12, 2013 (2013)), 267-275 · Zbl 1390.68337 |
| [16] | Cabalar, P.; Fandinno, J.; Schaub, T.; Schellhorn, S., Gelfond-Zhang aggregates as propositional formulas, Artif. Intell., 274, 26-43 (2019) · Zbl 1478.68363 |
| [17] | Cadoli, M.; Schaerf, M., On the complexity of entailment in propositional multivalued logics, Ann. Math. Artif. Intell., 18, 1, 29-50 (1996) · Zbl 0890.03010 |
| [18] | Claessen, K.; Een, N.; Sheeran, M.; Sörenson, N.; Voronov, A.; Akesson, K., SAT-solving in practice, with a tutorial example from supervisory control, Discrete Event Dyn. Syst., 19, 495-524 (2009) · Zbl 1180.93065 |
| [19] | Confalonieri, R.; Nieves, J. C., Nested preferences in answer set programming, Fundam. Inform., 113, 1, 19-39 (2011) · Zbl 1243.68140 |
| [20] | Confalonieri, R.; Nieves, J. C.; Osorio, M.; Vázquez-Salceda, J., Dealing with explicit preferences and uncertainty in answer set programming, Ann. Math. Artif. Intell., 65, 2-3, 159-198 (2012) · Zbl 1258.68139 |
| [21] | Confalonieri, R.; Prade, H., Using possibilistic logic for modeling qualitative decision: answer set programming algorithms, Int. J. Approx. Reason., 55, 2, 711-738 (2014) · Zbl 1316.68173 |
| [22] | Couchariere, O.; Lesot, M.; Bouchon-Meunier, B., Consistency checking for extended description logics, (Proceedings of the 21st International Workshop on Description Logics (DL2008). Proceedings of the 21st International Workshop on Description Logics (DL2008), Dresden, Germany, May 13-16, 2008 (2008)), 13-16 |
| [23] | Darwiche, A., Decomposable negation normal form, J. ACM, 48, 4, 608-647 (2001) · Zbl 1127.03321 |
| [24] | Doherty, P.; Kachniarz, J.; Szalas, A., Meta-queries on deductive databases, Fundam. Inform., 40, 1, 7-30 (1999) · Zbl 0946.68034 |
| [25] | Dowling, W.; Gallier, J., Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. Log. Program., 3, 267-284 (1984) · Zbl 0593.68062 |
| [26] | Drechsler, R.; Junttila, T.; Niemelä, I., Non-clausal SAT and ATPG, (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability: Chapter 21 (2009), IOS Press), 655-693 |
| [27] | D’Silva, V.; Kroening, D.; Weissenbacher, G., A survey of automated techniques for formal software verification, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 27, 7 (2008) |
| [28] | Dubois, D.; Lang, J.; Prade, H., Towards possibilistic logic programming, (Logic Programming, Proceedings of the Eigth International Conference. Logic Programming, Proceedings of the Eigth International Conference, Paris, France, June 24-28, 1991 (1991)), 581-595 |
| [29] | Dubois, D.; Lang, J.; Prade, H., Possibilistic logic, (Handbook of Logic in Artificial Intelligence and Logic Programming (1994), Oxford University Press: Oxford University Press New York), 419-513 |
| [30] | Dubois, D.; Prade, H., Necessity measures and the resolution principle, IEEE Trans. Syst. Man Cybern., 17, 3, 474-478 (1987) · Zbl 0643.94053 |
| [31] | Dubois, D.; Prade, H., Resolution principles in possibilistic logic, Int. J. Approx. Reason., 4, 1, 1-21 (1990) · Zbl 0697.68083 |
| [32] | Dubois, D.; Prade, H., Possibilistic logic: a retrospective and prospective view, Fuzzy Sets Syst., 144, 1, 3-23 (2004) · Zbl 1076.68084 |
| [33] | Dubois, D.; Prade, H., Possibilistic logic - an overview, (Woods, J.; Gabbay, D. M.; Siekmann, J. H., Handbook of the History of Logic. Vol 9, Computational Logic (2014), North-Holland), 283-342 · Zbl 1404.03008 |
| [34] | Dubois, D.; Prade, H., A crash course on generalized possibilistic logic, (Scalable Uncertainty Management - 12th International Conference, Proceedings. Scalable Uncertainty Management - 12th International Conference, Proceedings, SUM 2018, Milan, Italy, October 3-5, 2018 (2018)), 3-17 · Zbl 1517.68354 |
| [35] | Dubois, D.; Prade, H.; Schockaert, S., Stable models in generalized possibilistic logic, (Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference. Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012, Rome, Italy, June 10-14, 2012 (2012)) |
| [36] | Dubois, D.; Prade, H.; Schockaert, S., Generalized possibilistic logic: foundations and applications to qualitative reasoning about uncertainty, Artif. Intell., 252, 139-174 (2017) · Zbl 1419.68110 |
| [37] | Dubois, O.; André, P.; Boufkhad, Y.; Carlie, Y., Chap. SAT vs. UNSAT, (Second DIMACS Implementation Challenge: Cliques, Coloring and Unsatisfiability. Second DIMACS Implementation Challenge: Cliques, Coloring and Unsatisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Sciences, vol. 26 (1996), American Mathematical Society), 415-436 · Zbl 0864.90090 |
| [38] | Egly, U.; Seidl, M.; Woltran, S., A solver for QBFs in nonprenex form, (ECAI 2006, 17th European Conference on Artificial Intelligence, Including Prestigious Applications of Intelligent Systems (PAIS 2006), Proceedings. ECAI 2006, 17th European Conference on Artificial Intelligence, Including Prestigious Applications of Intelligent Systems (PAIS 2006), Proceedings, August 29 - September 1, 2006, Riva del Garda, Italy (2006)), 477-481 |
| [39] | Egly, U.; Seidl, M.; Woltran, S., A solver for QBFs in negation normal form, Constraints Int. J., 14, 1, 38-79 (2009) · Zbl 1167.68054 |
| [40] | Färber, M.; Kaliszyk, C., Certification of nonclausal connection tableaux proofs, (Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, Proceedings. Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, Proceedings, TABLEAUX 2019, London, UK, September 3-5, 2019 (2019)), 21-38 · Zbl 1435.03033 |
| [41] | Ferraris, P., Logic programs with propositional connectives and aggregates, ACM Trans. Comput. Log., 12, 4, Article 25 pp. (2011) · Zbl 1351.68053 |
| [42] | Ferraris, P.; Lifschitz, V., Weight constraints as nested expressions, Theory Pract. Log. Program., 5, 1-2, 45-74 (2005) · Zbl 1093.68017 |
| [43] | Fiorino, G., A non-clausal tableau calculus for minsat, Inf. Process. Lett., 173, Article 106167 pp. (2022) · Zbl 1482.68269 |
| [44] | Franco, J.; Martin, J., A history of satisfiability, (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability: Chapter 1 (2009), IOS Press), 3-55 |
| [45] | Giusto, C. D.; Gabbrielli, M.; Meo, M. C., On the expressive power of multiple heads in CHR, ACM Trans. Comput. Log., 13, 1, Article 6 pp. (2012) · Zbl 1351.68049 |
| [46] | Gogic, G.; Kautz, H. A.; Papadimitriou, C. H.; Selman, B., The comparative linguistics of knowledge representation, (Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montréal Québec, Canada, August 20-25, 1995 (1995), Morgan Kaufmann), 862-869, 2 volumes |
| [47] | Habiballa, H., Resolution strategies for fuzzy description logic, (New Dimensions in Fuzzy Logic and Related Technologies. Proceedings of the 5th EUSFLAT Conference, Vol. 2, Regular Sessions. New Dimensions in Fuzzy Logic and Related Technologies. Proceedings of the 5th EUSFLAT Conference, Vol. 2, Regular Sessions, Ostrava, Czech Republic, September 11-14, 2007 (2007)), 27-36 |
| [48] | Habiballa, H., Fuzzy Logic: Algorithms, Techniques and Implementations, 55-74 (2012), InTec, chapter Resolution Principle and Fuzzy Logic |
| [49] | Hähnle, R.; Murray, N. V.; Rosenthal, E., Linearity and regularity with negation normal form, Theor. Comput. Sci., 328, 3, 325-354 (2004) · Zbl 1071.68091 |
| [50] | Hollunder, B., An alternative proof method for possibilistic logic and its application to terminological logics, Int. J. Approx. Reason., 12, 2, 85-109 (1995) · Zbl 0814.68120 |
| [51] | Horn, A., On sentences which are of direct unions of algebras, J. Symb. Log., 16, 1, 14-21 (1951) · Zbl 0043.24801 |
| [52] | Imaz, G. E., The Horn non-clausal class and its polynomiality (2021), 1-59 |
| [53] | G.E. Imaz, Normal nested answer set programs: syntactics, semantics and logical calculi, November 2022, pp. 1-40, in preparation. |
| [54] | Imaz, G. E., A first polynomial non-clausal class in many-valued logic, Fuzzy Sets Syst., 1-37 (October 2022), in press · Zbl 1522.03099 |
| [55] | Itai, A.; Makowsky, J., Unification as a complexity measure for logic programming, J. Log. Program., 4, 105-177 (1987) · Zbl 0641.68143 |
| [56] | Komuravelli, A.; Bjørner, N.; Gurfinkel, A.; McMillan, K. L., Compositional verification of procedural programs using horn clauses over integers and arrays, (Kaivola, R.; Wahl, T., Formal Methods in Computer-Aided Design. Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015 (2015), IEEE), 89-96 |
| [57] | Lang, J., Possibilistic logic: complexity and algorithms, (Gabbay, D.; Smets, Ph., Handbook of Defeasible Reasoning and Uncertainty Management System (2001), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht, The Netherlands), 179-220 · Zbl 0984.03022 |
| [58] | Lehmke, S., A resolution-based axiomatization of ‘bold’ propositional fuzzy logic, (Linz’96: Fuzzy Sets, Logics, and Artificial Intelligence (1996)), 115-119 |
| [59] | Li, C. M.; Manyà, F.; Soler, J. R., A tableau calculus for non-clausal maximum satisfiability, (Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, Proceedings. Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, Proceedings, TABLEAUX 2019, London, UK, September 3-5, 2019 (2019)), 58-73 · Zbl 1435.68372 |
| [60] | Lifschitz, V., Answer Set Programming (2019), Springer · Zbl 1480.68003 |
| [61] | Lifschitz, V.; Tang, L. R.; Turner, H., Nested expressions in logic programs, Ann. Math. Artif. Intell., 25, 3-4, 369-389 (1999) · Zbl 0940.68075 |
| [62] | McKinsey, J., The decision problem for some classes of sentences without quantifiers, J. Symb. Log., 8, 61-76 (1943) · Zbl 0063.03864 |
| [63] | Muhammad, R.; Stuckey, P. J., A stochastic non-CNF SAT solver, (Yang, Q.; Webb, G. I., PRICAI 2006: Trends in Artificial Intelligence, 9th Pacific Rim International Conference on Artificial Intelligence, Proceedings. PRICAI 2006: Trends in Artificial Intelligence, 9th Pacific Rim International Conference on Artificial Intelligence, Proceedings, Guilin, China, August 7-11, 2006. PRICAI 2006: Trends in Artificial Intelligence, 9th Pacific Rim International Conference on Artificial Intelligence, Proceedings. PRICAI 2006: Trends in Artificial Intelligence, 9th Pacific Rim International Conference on Artificial Intelligence, Proceedings, Guilin, China, August 7-11, 2006, Lecture Notes in Computer Science, vol. 4099 (2006), Springer), 120-129 |
| [64] | Murray, N., Completely non-clausal theorem proving, Artif. Intell., 18, 1, 67-85 (1982) · Zbl 0472.68053 |
| [65] | Murray, N.; Rosenthal, E., Adapting classical inference techniques to multiple-valued logics using signed formulas, Fundam. Inform., 3, 21, 237-253 (1994) · Zbl 0811.03015 |
| [66] | Navarro, J.; Voronkov, A., Generation of hard non-clausal random satisfiability problems, (The Twentieth National Conference on Artificial Intelligence (2005)), 426-436 |
| [67] | Nicolas, P.; Garcia, L.; Stéphan, I.; Lefèvre, C., Possibilistic uncertainty handling for answer set programming, Ann. Math. Artif. Intell., 47, 1-2, 139-181 (2006) · Zbl 1105.68104 |
| [68] | Nieves, J. C.; Lindgren, H., Possibilistic nested logic programs, (Technical Communications of the 28th International Conference on Logic Programming. Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary (2012)), 267-276 · Zbl 1281.68213 |
| [69] | Nieves, J. C.; Lindgren, H., Possibilistic nested logic programs and strong equivalence, Int. J. Approx. Reason., 59, 1-19 (2015) · Zbl 1311.68154 |
| [70] | Nieves, J. C.; Osorio, M.; Cortés, U., Semantics for possibilistic disjunctive programs, (Logic Programming and Nonmonotonic Reasoning, 9th International Conference, Proceedings. Logic Programming and Nonmonotonic Reasoning, 9th International Conference, Proceedings, LPNMR 2007, Tempe, AZ, USA, May 15-17, 2007 (2007)), 315-320 · Zbl 1149.68337 |
| [71] | Nieves, J. C.; Osorio, M.; Cortés, U., Semantics for possibilistic disjunctive programs, Theory Pract. Log. Program., 13, 1, 33-70 (2013) · Zbl 1272.68081 |
| [72] | Oliver, B. E.; Otten, J., Equality preprocessing in connection calculi, (Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 Co-Located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020). Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 Co-Located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual) (2020)), 76-92 |
| [73] | Otten, J., A non-clausal connection calculus, (Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, Proceedings. Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, Proceedings, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011 (2011)), 226-241 · Zbl 1333.03004 |
| [74] | Otten, J., Non-clausal connection calculi for non-classical logics, (Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, Proceedings. Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, Proceedings, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 (2017)), 209-227 · Zbl 1496.03049 |
| [75] | Papadimitriou, C. H., Computational Complexity (1994), Addison-Wesley · Zbl 0833.68049 |
| [76] | Platzer, A., Differential dynamic logic for hybrid systems, J. Autom. Reason., 41, 2, 143-189 (2008) · Zbl 1181.03035 |
| [77] | Scala, E.; Haslum, P.; Thiébaux, S.; Ramírez, M., Subgoaling techniques for satisficing and optimal numeric planning, J. Artif. Intell. Res., 68, 691-752 (2020) · Zbl 1461.68219 |
| [78] | Seidl, M., A solver for quantified Boolean formulas in negation normal form (2007), Universität Wien, PhD thesis |
| [79] | Stachniak, Z., Exploiting polarity in multiple-valued inference systems, (31st IEEE Int. Symp. on Multiple-Valued Logic (2001)), 149-156 |
| [80] | Tamura, N.; Taga, A.; Kitagawa, S.; Banbara, M., Compiling finite linear CSP into SAT, Constraints Int. J., 14, 2, 254-272 (2009) · Zbl 1186.68076 |
| [81] | Thiffault, C.; Bacchus, F.; Walsh, T., Solving non-clausal formulas with DPLL search, (Tenth International Conference on Principles and Practice of Constraint Programming (2004)), 663-678 · Zbl 1152.68588 |
| [82] | Unno, H.; Terauchi, T., Inferring simple solutions to recursion-free horn clauses via sampling, (Baier, C.; Tinelli, C., Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, Proceedings, ETAPS 2015, London, UK, April 11-18, 2015. Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, Proceedings, ETAPS 2015, London, UK, April 11-18, 2015, Lecture Notes in Computer Science, vol. 9035 (2015), Springer), 149-163 · Zbl 1420.68077 |
| [83] | Williams, P. F.; Biere, A.; Clarke, E. M.; Gupta, A., Combining decision diagrams and SAT procedures for efficient symbolic model checking, (Computer Aided Verification (CAV). Computer Aided Verification (CAV), LNCS, vol. 1855 (2000)), 124-138 · Zbl 0974.68526 |
| [84] | Xu, Y.; Liu, J.; He, X.; Zhong, X.; Chen, S., Non-clausal multi-ary α-generalized resolution calculus for a finite lattice-valued logic, Int. J. Comput. Intell. Syst., 11, 1, 384-401 (2018) |
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.
