×

zbMATH — the first resource for mathematics

Fuzzy answer set computation via satisfiability modulo theories. (English) Zbl 1379.68036
Summary: Fuzzy answer set programming (FASP) combines two declarative frameworks, answer set programming and fuzzy logic, in order to model reasoning by default over imprecise information. Several connectives are available to combine different expressions; in particular the Gödel and Łukasiewicz fuzzy connectives are usually considered, due to their properties. Although the Gödel conjunction can be easily eliminated from rule heads, we show through complexity arguments that such a simplification is infeasible in general for all other connectives. The paper analyzes a translation of FASP programs into satisfiability modulo theories (SMT), which in general produces quantified formulas because of the minimality of the semantics. Structural properties of many FASP programs allow to eliminate the quantification, or to sensibly reduce the number of quantified variables. Indeed, integrality constraints can replace recursive rules commonly used to force Boolean interpretations, and completion subformulas can guarantee minimality for acyclic programs with atomic heads. Moreover, head cycle free rules can be replaced by shifted subprograms, whose structure depends on the eliminated head connective, so that ordered completion may replace the minimality check if also Łukasiewicz disjunction in rule bodies is acyclic. The paper also presents and evaluates a prototype system implementing these translations.
MSC:
68N17 Logic programming
03B52 Fuzzy logic; logic of vagueness
68T37 Reasoning under uncertainty in the context of artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Akbarpour, B.; Paulson, L. C., Metitarski: an automatic theorem prover for real-valued special functions, J. Autom. Reasoning, 44, 3, 175-205, (2010) · Zbl 1215.68206
[2] Alviano, M.; Calimeri, F.; Charwat, G.; Dao-Tran, M.; Dodaro, C.; Ianni, G.; Krennwallner, T.; Kronegger, M.; Oetsch, J.; Pfandler, A.; Pührer, J.; Redl, C.; Ricca, F.; Schneider, P.; Schwengerer, M.; Spendier, L. K.; Wallner, J. P.; Xiao, G.; Cabalar, P.; Son, T. C., pp., (2013)
[3] Alviano, M.; Dodaro, C.; Faber, W.; Leone, N.; Ricca, F.; Cabalar, P.; Son, T. C., Logic Programming and Nonmonotonic Reasoning, 12th International Conference, LPNMR 2013, Corunna, Spain, September 15-19, 2013. Proceedings, WASP: A native ASP solver based on constraint learning, 54-66, (2013), Springer
[4] Alviano, M.; Faber, W.; Leone, N.; Perri, S.; Pfeifer, G.; Terracina, G.; de Moor, O.; Gottlob, G.; Furche, T.; Sellers, A. J., Datalog Reloaded - First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Revised Selected Papers, The disjunctive datalog system DLV, 282-301, (2010), Springer
[5] Alviano, M.; Peñaloza, R., Fuzzy answer sets approximations, TPLP, 13, 4-5, 753-767, (2013) · Zbl 1298.68058
[6] Asuncion, V.; Lin, F.; Zhang, Y.; Zhou, Y., Ordered completion for first-order logic programs on finite structures, Artif. Intell., 177-179, 1-24, (2012) · Zbl 1244.68072
[7] Baral, C., Knowledge Representation, Reasoning and Declarative Problem Solving, pp., (2003), Cambridge University Press · Zbl 1056.68139
[8] Barrett, C. W.; Sebastiani, R.; Seshia, S. A.; Tinelli, C.; Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability, Satisfiability modulo theories, 825-885, (2009), IOS Press
[9] Ben-Eliyahu, R.; Dechter, R., Propositional semantics for disjunctive logic programs, Ann. Math. Artif. Intell., 12, 1-2, 53-87, (1994) · Zbl 0858.68012
[10] Blondeel, M.; Schockaert, S.; Vermeir, D.; Cock, M. D., Complexity of fuzzy answer set programming under łukasiewicz semantics, Int. J. Approx. Reasoning, 55, 9, 1971-2003, (2014) · Zbl 1433.68082
[11] Calimeri, F.; Gebser, M.; Maratea, M.; Ricca, F., pp., (2014)
[12] Clark, K. L., pp., (1977)
[13] de Moura, L. M.; Bjørner, N.; Ramakrishnan, C. R.; Rehof, J., Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Z3: an efficient SMT solver, 337-340, (2008), Springer
[14] Delgrande, J. P.; Schaub, T.; Tompits, H.; Woltran, S.; Brewka, G.; Lang, J., pp., (2008)
[15] Eiter, T.; Fink, M.; Woltran, S., Semantical characterizations and complexity of equivalences in answer set programming, ACM Trans. Comput. Log., 8, 3, pp., (2007) · Zbl 1367.68031
[16] Eiter, T.; Gottlob, G., On the computational cost of disjunctive logic programming: propositional case, Ann. Math. Artif. Intell., 15, 3-4, 289-323, (1995) · Zbl 0858.68016
[17] Ge, Y.; de Moura, L. M.; Bouajjani, A.; Maler, O., Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, Complete instantiation for quantified formulas in satisfiabiliby modulo theories, 306-320, (2009), Springer
[18] Gebser, M.; Kaminski, R.; König, A.; Schaub, T.; Delgrande, J. P.; Faber, W., Logic Programming and Nonmonotonic Reasoning - 11th International Conference, LPNMR 2011, Vancouver, Canada, May 16-19, 2011. Proceedings, Advances in gringo series 3, 345-351, (2011), Springer
[19] Gebser, M.; Kaufmann, B.; Schaub, T., Conflict-driven answer set solving: from theory to practice, Artif. Intell., 187, 52-89, (2012) · Zbl 1251.68060
[20] Gelfond, M.; Lifschitz, V., Classical negation in logic programs and disjunctive databases, New Generation Comput., 9, 3/4, 365-386, (1991) · Zbl 0735.68012
[21] Janhunen, T.; de Mántaras, R. L.; Saitta, L., Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI’2004, Valencia, Spain, August 22-27, 2004, Representing normal programs with clauses, 358-362, (2004), IOS Press
[22] Janssen, J.; Schockaert, S.; Vermeir, D.; Cock, M. D., pp., (2012)
[23] Janssen, J.; Vermeir, D.; Schockaert, S.; Cock, M. D., Reducing fuzzy answer set programming to model finding in fuzzy logics, TPLP, 12, 6, 811-842, (2012) · Zbl 1255.68051
[24] Lee, J.; Wang, Y.; Fermé, E.; Leite, J., Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, Stable models of fuzzy propositional formulas, 326-339, (2014), Springer
[25] Lierler, Y.; Maratea, M.; Lifschitz, V.; Niemelä, I., Logic Programming and Nonmonotonic Reasoning, 7th International Conference, LPNMR 2004, Fort Lauderdale, FL, USA, January 6-8, 2004, Proceedings, Cmodels-2: Sat-based answer set solver enhanced to non-tight programs, 346-350, (2004), Springer · Zbl 1122.68377
[26] Lin, F.; You, J.-H., Abduction in logic programming: A new definition and an abductive procedure based on rewriting, Artificial Intelligence, 140, 1/2, 175-205, (2002) · Zbl 0999.68092
[27] Marek, V. W.; Remmel, J. B.; Delgrande, J. P.; Schaub, T., pp., (2004)
[28] Marek, V. W.; Truszczyński, M.; Apt, K. R.; Marek, V. W.; Truszczyński, M.; Warren, D. S., The Logic Programming Paradigm - A 25-Year Perspective, Stable Models and an Alternative Logic Programming Paradigm, 375-398, (1999), Springer Verlag · Zbl 0979.68524
[29] Mushthofa, M.; Schockaert, S.; Cock, M. D.; Schaub, T.; Friedrich, G.; O’Sullivan, B., ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, A finite-valued solver for disjunctive fuzzy answer set programs, 645-650, (2014), IOS Press · Zbl 1366.68018
[30] Niemelä, I., Logic programs with stable model semantics as a constraint programming paradigm, Ann. Math. Artif. Intell., 25, 3-4, 241-273, (1999) · Zbl 0940.68018
[31] Niemelä, I., Stable models and difference logic, Ann. Math. Artif. Intell., 53, 1-4, 313-329, (2008) · Zbl 1165.68338
[32] Nieuwenborgh, D. V.; Cock, M. D.; Vermeir, D., An introduction to fuzzy answer set programming, Ann. Math. Artif. Intell., 50, 3-4, 363-388, (2007) · Zbl 1125.68118
[33] Ratschan, S., Efficient solving of quantified inequality constraints over the real numbers, ACM Trans. Comput. Log., 7, 4, 723-748, (2006) · Zbl 1367.68270
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.