×

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
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] AkbarpourB. and PaulsonL. C.2010. Metitarski: An automatic theorem prover for real-valued special functions. J. Autom. Reasoning44, 3, 175-205.10.1007/s10817-009-9149-2 · Zbl 1215.68206 · doi:10.1007/s10817-009-9149-2
[2] AlvianoM., CalimeriF., CharwatG., Dao-TranM., DodaroC., IanniG., KrennwallnerT., KroneggerM., OetschJ., PfandlerA., PührerJ., RedlC., RiccaF., SchneiderP., SchwengererM., SpendierL. K., WallnerJ. P. and XiaoG.2013. The fourth answer set programming competition: Preliminary report. In LPNMR, P.Cabalar and T. C.Son, Eds. LNCS. 42-53.
[3] AlvianoM., DodaroC., FaberW., LeoneN. and RiccaF.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, P.Cabalar and T. C.Son, Eds. Lecture Notes in Computer Science, vol. 8148. Springer, 54-66.
[4] AlvianoM., FaberW., LeoneN., PerriS., PfeiferG. and TerracinaG.2010. The disjunctive datalog system DLV. In Datalog Reloaded - First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Revised Selected Papers, O.de Moor, G.Gottlob, T.Furche, and A. J.Sellers, Eds. Lecture Notes in Computer Science, vol. 6702. Springer, 282-301.
[5] AlvianoM. and PeñalozaR.2013. Fuzzy answer sets approximations. TPLP13, 4-5, 753-767. · Zbl 1298.68058
[6] AsuncionV., LinF., ZhangY. and ZhouY.2012. Ordered completion for first-order logic programs on finite structures. Artif. Intell.177-179, 1-24. · Zbl 1244.68072
[7] BaralC.2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press. · Zbl 1056.68139
[8] BarrettC. W., SebastianiR., SeshiaS. A. and TinelliC.2009. Satisfiability modulo theories. In Handbook of Satisfiability, A.Biere, M.Heule, H.van Maaren, and T.Walsh, Eds. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, 825-885.
[9] Ben-EliyahuR. and DechterR.1994. Propositional semantics for disjunctive logic programs. Ann. Math. Artif. Intell.12, 1-2, 53-87.10.1007/BF01530761 · Zbl 0858.68012 · doi:10.1007/BF01530761
[10] BlondeelM., SchockaertS., VermeirD. and CockM. D.2014. Complexity of fuzzy answer set programming under łukasiewicz semantics. Int. J. Approx. Reasoning55, 9, 1971-2003.10.1016/j.ijar.2013.10.011 · Zbl 1433.68082 · doi:10.1016/j.ijar.2013.10.011
[11] CalimeriF., GebserM., MarateaM. and RiccaF.2014. The design of the fifth answer set programming competition. CoRR abs/1405.3710.
[12] ClarkK. L.1977. Negation as failure. In Logic and Data Bases. 293-322.
[13] de MouraL. M. and BjørnerN.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, C. R.Ramakrishnan and J.Rehof, Eds. Lecture Notes in Computer Science, vol. 4963. Springer, 337-340.
[14] DelgrandeJ. P., SchaubT., TompitsH. and WoltranS.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, G.Brewka and J.Lang, Eds. 411-421.
[15] EiterT., FinkM. and WoltranS.2007. Semantical characterizations and complexity of equivalences in answer set programming. ACM Trans. Comput. Log.8, 3. · Zbl 1367.68031
[16] EiterT. and GottlobG.1995. On the computational cost of disjunctive logic programming: Propositional case. Ann. Math. Artif. Intell.15, 3-4, 289-323.10.1007/BF01536399 · Zbl 0858.68016 · doi:10.1007/BF01536399
[17] GeY. and de MouraL. 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, A.Bouajjani and O.Maler, Eds. Lecture Notes in Computer Science, vol. 5643. Springer, 306-320. · Zbl 1242.68280
[18] GebserM., KaminskiR., KönigA. and SchaubT.2011. Advances in gringo series 3. In Logic Programming and Nonmonotonic Reasoning - 11th International Conference, LPNMR 2011, Vancouver, Canada, May 16-19, 2011. Proceedings, J. P.Delgrande and W.Faber, Eds. Lecture Notes in Computer Science, vol. 6645. Springer, 345-351.
[19] GebserM., KaufmannB. and SchaubT.2012. Conflict-driven answer set solving: From theory to practice. Artif. Intell.187, 52-89. · Zbl 1251.68060
[20] GelfondM. and LifschitzV.1991. Classical negation in logic programs and disjunctive databases. New Generation Comput.9, 3/4, 365-386.10.1007/BF03037169 · Zbl 0735.68012 · doi:10.1007/BF03037169
[21] JanhunenT.2004. Representing normal programs with clauses. In Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI’2004, Valencia, Spain, August 22-27, 2004, R. L.de Mántaras and L.Saitta, Eds. IOS Press, 358-362.
[22] JanssenJ., SchockaertS., VermeirD. and CockM. D.2012. Answer Set Programming for Continuous Domains - A Fuzzy Logic Approach. Atlantis Computational Intelligence Systems, vol. 5. Atlantis Press.
[23] JanssenJ., VermeirD., SchockaertS. and CockM. D.2012. Reducing fuzzy answer set programming to model finding in fuzzy logics. TPLP12, 6, 811-842. · Zbl 1255.68051
[24] LeeJ. and WangY.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, E.Fermé and J.Leite, Eds. Lecture Notes in Computer Science, vol. 8761. Springer, 326-339.
[25] LierlerY. and MarateaM.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, V.Lifschitz and I.Niemelä, Eds. Lecture Notes in Computer Science, vol. 2923. Springer, 346-350. · Zbl 1122.68377
[26] LinF. and YouJ.-H.2002. Abduction in logic programming: A new definition and an abductive procedure based on rewriting. Artificial Intelligence140, 1/2, 175-205.10.1016/S0004-3702(02)00227-8 · Zbl 0999.68092 · doi:10.1016/S0004-3702(02)00227-8
[27] MarekV. W. and RemmelJ. 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, J. P.Delgrande and T.Schaub, Eds. 276-284.
[28] MarekV. W. and TruszczyńskiM.1999. Stable Models and an Alternative Logic Programming Paradigm. In The Logic Programming Paradigm - A 25-Year Perspective, K. R.Apt, V. W.Marek, M.Truszczyński, and D. S.Warren, Eds. Springer Verlag, 375-398.10.1007/978-3-642-60085-2 · Zbl 0979.68524 · doi:10.1007/978-3-642-60085-2
[29] MushthofaM., SchockaertS. and CockM. 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, T.Schaub, G.Friedrich, and B.O’Sullivan, Eds. Frontiers in Artificial Intelligence and Applications, vol. 263. IOS Press, 645-650. · Zbl 1366.68018
[30] NiemeläI.1999. Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell.25, 3-4, 241-273.10.1023/A:1018930122475 · Zbl 0940.68018 · doi:10.1023/A:1018930122475
[31] NiemeläI.2008. Stable models and difference logic. Ann. Math. Artif. Intell.53, 1-4, 313-329.10.1007/s10472-009-9118-9 · Zbl 1165.68338 · doi:10.1007/s10472-009-9118-9
[32] NieuwenborghD. V., CockM. D. and VermeirD.2007. An introduction to fuzzy answer set programming. Ann. Math. Artif. Intell.50, 3-4, 363-388.10.1007/s10472-007-9080-3 · Zbl 1125.68118 · doi:10.1007/s10472-007-9080-3
[33] RatschanS.2006. Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Log.7, 4, 723-748.10.1145/1183278.1183282 · Zbl 1367.68270 · doi:10.1145/1183278.1183282
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.