Hostname: page-component-8448b6f56d-mp689 Total loading time: 0 Render date: 2024-04-17T21:38:03.184Z Has data issue: false hasContentIssue false

Fuzzy answer set computation via satisfiability modulo theories

Published online by Cambridge University Press:  03 September 2015

MARIO ALVIANO
Affiliation:
University of Calabria, Italy
RAFAEL PEÑALOZA
Affiliation:
Free University of Bozen-Bolzano, Italy

Abstract

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.

Type
Regular Papers
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Akbarpour, B. and Paulson, L. C. 2010. Metitarski: An automatic theorem prover for real-valued special functions. J. Autom. Reasoning 44, 3, 175205.CrossRefGoogle Scholar
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. and Xiao, G. 2013. The fourth answer set programming competition: Preliminary report. In LPNMR, Cabalar, P. and Son, T. C., Eds. LNCS. 42–53.Google Scholar
Alviano, M., Dodaro, C., Faber, W., Leone, N. and Ricca, F. 2013. WASP: A native ASP solver based on constraint learning. In Logic Programming and Nonmonotonic Reasoning, 12th International Conference, LPNMR 2013, Corunna, Spain, September 15-19, 2013. Proceedings, Cabalar, P. and Son, T. C., Eds. Lecture Notes in Computer Science, vol. 8148. Springer, 5466.CrossRefGoogle Scholar
Alviano, M., Faber, W., Leone, N., Perri, S., Pfeifer, G. and Terracina, G. 2010. The disjunctive datalog system DLV. In Datalog Reloaded - First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Revised Selected Papers, de Moor, O., Gottlob, G., Furche, T., and Sellers, A. J., Eds. Lecture Notes in Computer Science, vol. 6702. Springer, 282301.Google Scholar
Alviano, M. and Peñaloza, R. 2013. Fuzzy answer sets approximations. TPLP 13, 4–5, 753767.Google Scholar
Asuncion, V., Lin, F., Zhang, Y. and Zhou, Y. 2012. Ordered completion for first-order logic programs on finite structures. Artif. Intell. 177–179, 124.CrossRefGoogle Scholar
Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press.CrossRefGoogle Scholar
Barrett, C. W., Sebastiani, R., Seshia, S. A. and Tinelli, C. 2009. Satisfiability modulo theories. In Handbook of Satisfiability, Biere, A., Heule, M., van Maaren, H., and Walsh, T., Eds. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, 825885.Google Scholar
Ben-Eliyahu, R. and Dechter, R. 1994. Propositional semantics for disjunctive logic programs. Ann. Math. Artif. Intell. 12, 1–2, 5387.CrossRefGoogle Scholar
Blondeel, M., Schockaert, S., Vermeir, D. and Cock, M. D. 2014. Complexity of fuzzy answer set programming under łukasiewicz semantics. Int. J. Approx. Reasoning 55, 9, 19712003.CrossRefGoogle Scholar
Calimeri, F., Gebser, M., Maratea, M. and Ricca, F. 2014. The design of the fifth answer set programming competition. CoRR abs/1405.3710.Google Scholar
Clark, K. L. 1977. Negation as failure. In Logic and Data Bases. 293–322.CrossRefGoogle Scholar
de Moura, L. M. and Bjørner, N. 2008. Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Ramakrishnan, C. R. and Rehof, J., Eds. Lecture Notes in Computer Science, vol. 4963. Springer, 337340.Google Scholar
Delgrande, J. P., Schaub, T., Tompits, H. and Woltran, S. 2008. Belief revision of logic programs under answer set semantics. In Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference, KR 2008, Sydney, Australia, September 16-19, 2008, Brewka, G. and Lang, J., Eds. 411–421.Google Scholar
Eiter, T., Fink, M. and Woltran, S. 2007. Semantical characterizations and complexity of equivalences in answer set programming. ACM Trans. Comput. Log. 8, 3.CrossRefGoogle Scholar
Eiter, T. and Gottlob, G. 1995. On the computational cost of disjunctive logic programming: Propositional case. Ann. Math. Artif. Intell. 15, 3–4, 289323.CrossRefGoogle Scholar
Ge, Y. and de Moura, L. M. 2009. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, Bouajjani, A. and Maler, O., Eds. Lecture Notes in Computer Science, vol. 5643. Springer, 306320.CrossRefGoogle Scholar
Gebser, M., Kaminski, R., König, A. and Schaub, T. 2011. Advances in gringo series 3. In Logic Programming and Nonmonotonic Reasoning - 11th International Conference, LPNMR 2011, Vancouver, Canada, May 16-19, 2011. Proceedings, Delgrande, J. P. and Faber, W., Eds. Lecture Notes in Computer Science, vol. 6645. Springer, 345351.Google Scholar
Gebser, M., Kaufmann, B. and Schaub, T. 2012. Conflict-driven answer set solving: From theory to practice. Artif. Intell. 187, 5289.CrossRefGoogle Scholar
Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Generation Comput. 9, 3/4, 365386.CrossRefGoogle Scholar
Janhunen, T. 2004. Representing normal programs with clauses. In Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, Valencia, Spain, August 22-27, 2004, de Mántaras, R. L. and Saitta, L., Eds. IOS Press, 358362.Google Scholar
Janssen, J., Schockaert, S., Vermeir, D. and Cock, M. D. 2012. Answer Set Programming for Continuous Domains - A Fuzzy Logic Approach. Atlantis Computational Intelligence Systems, vol. 5. Atlantis Press.CrossRefGoogle Scholar
Janssen, J., Vermeir, D., Schockaert, S. and Cock, M. D. 2012. Reducing fuzzy answer set programming to model finding in fuzzy logics. TPLP 12, 6, 811842.Google Scholar
Lee, J. and Wang, Y. 2014. Stable models of fuzzy propositional formulas. In Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, Fermé, E. and Leite, J., Eds. Lecture Notes in Computer Science, vol. 8761. Springer, 326339.Google Scholar
Lierler, Y. and Maratea, M. 2004. Cmodels-2: Sat-based answer set solver enhanced to non-tight programs. In Logic Programming and Nonmonotonic Reasoning, 7th International Conference, LPNMR 2004, Fort Lauderdale, FL, USA, January 6-8, 2004, Proceedings, Lifschitz, V. and Niemelä, I., Eds. Lecture Notes in Computer Science, vol. 2923. Springer, 346350.Google Scholar
Lin, F. and You, J.-H. 2002. Abduction in logic programming: A new definition and an abductive procedure based on rewriting. Artificial Intelligence 140, 1/2, 175205.CrossRefGoogle Scholar
Marek, V. W. and Remmel, J. B. 2004. Answer set programming with default logic. In 10th International Workshop on Non-Monotonic Reasoning (NMR 2004), Whistler, Canada, June 6-8, 2004, Proceedings, Delgrande, J. P. and Schaub, T., Eds. 276–284.Google Scholar
Marek, V. W. and Truszczyński, M. 1999. Stable Models and an Alternative Logic Programming Paradigm. In The Logic Programming Paradigm – A 25-Year Perspective, Apt, K. R., Marek, V. W., Truszczyński, M., and Warren, D. S., Eds. Springer Verlag, 375398.CrossRefGoogle Scholar
Mushthofa, M., Schockaert, S. and Cock, M. D. 2014. A finite-valued solver for disjunctive fuzzy answer set programs. In ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, Schaub, T., Friedrich, G., and O'Sullivan, B., Eds. Frontiers in Artificial Intelligence and Applications, vol. 263. IOS Press, 645650.Google Scholar
Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell. 25, 3–4, 241273.CrossRefGoogle Scholar
Niemelä, I. 2008. Stable models and difference logic. Ann. Math. Artif. Intell. 53, 1–4, 313329.CrossRefGoogle Scholar
Nieuwenborgh, D. V., Cock, M. D. and Vermeir, D. 2007. An introduction to fuzzy answer set programming. Ann. Math. Artif. Intell. 50, 3–4, 363388.CrossRefGoogle Scholar
Ratschan, S. 2006. Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Log. 7, 4, 723748.CrossRefGoogle Scholar
Supplementary material: PDF

Alviano and Peñaloza supplementary material

Online Appendix

Download Alviano and Peñaloza supplementary material(PDF)
PDF 205.6 KB