Forgetting in multi-agent modal logics. (English) Zbl 1478.68351
Summary: In the past decades, forgetting has been investigated for many logics and has found many applications in knowledge representation and reasoning. In this paper, we study forgetting in multi-agent modal logics. We adopt the semantic definition of existential bisimulation quantifiers as that of forgetting. We resort to canonical formulas of modal logics introduced by Moss. An arbitrary modal formula is equivalent to the disjunction of a unique set of satisfiable canonical formulas. We show that, for the logics of \(\mathsf{K}_{\mathsf{n}}, \mathsf{D}_{\mathsf{n}}, \mathsf{T}_{\mathsf{n}}, \mathsf{K} 45_{\mathsf{n}}, \mathsf{KD} 45_{\mathsf{n}}\) and \(\mathsf{S} 5_{\mathsf{n}}\), the result of forgetting an atom from a satisfiable canonical formula can be computed by simply substituting the literals of the atom with \(\top\). Thus we show that these logics are closed under forgetting, and hence have uniform interpolation. Finally, we generalize the above results to include common knowledge of propositional formulas.
MSC:
| 68T27 | Logic in artificial intelligence |
| 03B42 | Logics of knowledge and belief (including belief change) |
| 03B45 | Modal logic (including the logic of norms) |
| 68T42 | Agent technology and artificial intelligence |
References:
| [1] | Ackermann, W., Untersuchung über das eliminationsproblem der mathematischen logik, Math. Ann., 110, 390-413 (1935) · JFM 60.0022.01 |
| [2] | Aucher, G.; Belle, V., Multi-agent only knowing on planet Kripke, (Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI-2015) (2015), IJCAI/AAAI Press), 2713-2719 |
| [3] | Baral, C.; Zhang, Y., Knowledge updates: semantics and complexity issues, Artif. Intell., 164, 209-243 (2005) · Zbl 1132.68720 |
| [4] | Bílková, M., Uniform interpolation and propositional quantifiers in modal logics, Stud. Log., 85, 1-31 (2007) · Zbl 1113.03017 |
| [5] | Boole, G., An Investigation of the Laws of Thought (1854), Walton & Maberly |
| [6] | ten Cate, B.; Conradie, W.; Marx, M.; Venema, Y., Definitorially complete description logics, (Proceedings of the Tenth International Conference on Principles of Knowledge Representation and Reasoning (KR-2006) (2006), AAAI Press), 79-89 |
| [7] | D’Agostino, G.; Hollenberg, M., Logical questions concerning the \(μ\)-calculus: interpolation, Lyndon and Łoś-Tarski, J. Symb. Log., 65, 310-332 (2000) · Zbl 0982.03011 |
| [8] | D’Agostino, G.; Lenzi, G., On modal \(μ\)-calculus with explicit interpolants, J. Appl. Log., 4, 256-278 (2006) · Zbl 1106.03024 |
| [9] | D’Agostino, G.; Lenzi, G., A note on bisimulation quantifiers and fixed points over transitive frames, J. Log. Comput., 18, 601-614 (2007) · Zbl 1173.03018 |
| [10] | van Ditmarsch, H.; Herzig, A.; Lang, J.; Marquis, P., Introspective forgetting, Synthese, 169, 405-423 (2009) · Zbl 1180.03018 |
| [11] | Eiter, T.; Wang, K., Semantic forgetting in answer set programming, Artif. Intell., 172, 1644-1672 (2008) · Zbl 1184.68159 |
| [12] | Fang, L.; Liu, Y.; van Ditmarsch, H., Forgetting in multi-agent modal logics, (Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-2016) (2016), IJCAI/AAAI Press), 1066-1073 |
| [13] | Fine, K., Normal forms in modal logic, Notre Dame J. Form. Log., 16, 229-237 (1975) · Zbl 0245.02025 |
| [14] | French, T. N., Bisimulation Quantifiers for Modal Logics (2006), University of Western Australia, Ph.D. thesis · Zbl 1186.03054 |
| [15] | Gabbay, D.; Ohlbach, H. J., Quantifier elimination in second-order predicate logic, (Proceedings of the Third International Conference on Principles of Knowledge Representation and Reasoning (KR-1992) (1992), Morgan Kaufmann), 425-435 |
| [16] | Gabbay, D. M.; Schmidt, R. A.; Szalas, A., Second-order quantifier elimination: foundations, computational aspects and applications, (Studies in Logic: Mathematical Logic and Foundations, vol. 12 (2008), College Publications) · Zbl 1165.03011 |
| [17] | Ghilardi, S., An algebraic theory of normal forms, Ann. Pure Appl. Logic, 71, 189-245 (1995) · Zbl 0815.03010 |
| [18] | Ghilardi, S.; Zawadowski, M. W., Undefinability of propositional quantifiers in the modal system S4, Stud. Log., 55, 259-271 (1995) · Zbl 0831.03008 |
| [19] | Gonçalves, R.; Knorr, M.; Leite, J., The ultimate guide to forgetting in answer set programming, (Proceedings of the Fifteenth International Conference on Principles of Knowledge Representation and Reasoning (KR-2016) (2016), AAAI Press), 135-144 |
| [20] | Hales, J.; French, T.; Davies, R., Refinement quantified logics of knowledge and belief for multiple agents, (Proceedings of the Ninth Conference on Advances in Modal Logic (AiML-2012) (2012), College Publications), 317-338 · Zbl 1301.03019 |
| [21] | Halpern, J. Y.; Moses, Y., A guide to completeness and complexity for modal logics of knowledge and belief, Artif. Intell., 54, 319-379 (1992) · Zbl 0762.68029 |
| [22] | Herzig, A.; Lang, J.; Marquis, P., Action representation and partially observable planning using epistemic logic, (Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI-2003) (2003), Morgan Kaufmann), 1067-1073 |
| [23] | Herzig, A.; Mengin, J., Uniform interpolation by resolution in modal logic, (Proceedings of the Eleventh European Conference on Logics in Artificial Intelligence (JELIA-2008). Proceedings of the Eleventh European Conference on Logics in Artificial Intelligence (JELIA-2008), Lecture Notes in Computer Science, vol. 5293 (2008), Springer), 219-231 · Zbl 1178.03032 |
| [24] | Janin, D.; Walukiewicz, I., Automata for the modal \(μ\)-calculus and related results, (Proceedings of the Twentieth International Symposium on Mathematical Foundations of Computer Science (MFCS-1995). Proceedings of the Twentieth International Symposium on Mathematical Foundations of Computer Science (MFCS-1995), Lecture Notes in Computer Science, vol. 969 (1995), Springer), 552-562 · Zbl 1193.68163 |
| [25] | Konev, B.; Walther, D.; Wolter, F., Forgetting and uniform interpolation in large-scale description logic terminologies, (Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI-2009) (2009), IJCAI/AAAI Press), 830-835 |
| [26] | Koopmann, P.; Schmidt, R. A., Uniform interpolation and forgetting for \(ALC\) ontologies with ABoxes, (Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (2015) (2015), AAAI Press), 175-181 |
| [27] | Kozen, D., Results on the propositional \(μ\)-calculus, Theor. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007 |
| [28] | Lang, J.; Liberatore, P.; Marquis, P., Propositional independence: formula-variable independence and forgetting, J. Artif. Intell. Res., 18, 391-443 (2003) · Zbl 1056.68112 |
| [29] | Lang, J.; Marquis, P., Reasoning under inconsistency: a forgetting-based approach, Artif. Intell., 174, 799-823 (2010) · Zbl 1206.68301 |
| [30] | Lin, F., On strongest necessary and weakest sufficient conditions, Artif. Intell., 128, 143-159 (2001) · Zbl 0971.68127 |
| [31] | Lin, F.; Reiter, R., Forget it!, (Proceedings of AAAI Fall Symposium on Relevance (1994), AAAI Press), 154-159 |
| [32] | Lin, F.; Reiter, R., How to progress a database, Artif. Intell., 92, 131-167 (1997) · Zbl 1017.68510 |
| [33] | Liu, Y.; Lakemeyer, G., On first-order definability and computability of progression for local-effect actions and beyond, (Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI-2009) (2009), IJCAI/AAAI Press), 860-866 |
| [34] | Liu, Y.; Wen, X., On the progression of knowledge in the situation calculus, (Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-2011) (2011), IJCAI/AAAI Press), 976-982 |
| [35] | Ludwig, M.; Konev, B., Practical uniform interpolation and forgetting for \(ALC\) TBoxes with applications to logical difference, (Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR-2014) (2014), AAAI Press), 318-327 |
| [36] | Lutz, C.; Wolter, F., Foundations for uniform interpolation and forgetting in expressive description logics, (Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-2011) (2011), IJCAI/AAAI Press), 989-995 |
| [37] | Moss, L. S., Finite models constructed from canonical formulas, J. Philos. Log., 36, 605-640 (2007) · Zbl 1132.03007 |
| [38] | Pattinson, D., The logic of exact covers: completeness and uniform interpolation, (Proceedings of the Twenty-Eighth ACM/IEEE Symposium on Logic in Computer Science (LICS-2013) (2013), IEEE Computer Society Press), 418-427 · Zbl 1433.03058 |
| [39] | Studer, T., Common knowledge does not have the Beth property, Inf. Process. Lett., 109, 611-614 (2009) · Zbl 1214.03013 |
| [40] | Su, K.; Sattar, A.; Lv, G.; Zhang, Y., Variable forgetting in reasoning about knowledge, J. Artif. Intell. Res., 35, 677-716 (2009) · Zbl 1192.68677 |
| [41] | Visser, A., Uniform interpolation and layered bisimulation, (Gödel 96. Gödel 96, Brno, 1996 (1996), Springer), 139-164 · Zbl 0854.03026 |
| [42] | Wang, K.; Wang, Z.; Topor, R. W.; Pan, J. Z.; Antoniou, G., Eliminating concepts and roles from ontologies in expressive descriptive logics, Comput. Intell., 30, 205-232 (2014) · Zbl 1328.68222 |
| [43] | Wang, Y.; Zhang, Y.; Zhou, Y.; Zhang, M., Knowledge forgetting in answer set programming, J. Artif. Intell. Res., 50, 31-70 (2014) · Zbl 1442.68228 |
| [44] | Wang, Z.; Wang, K.; Topor, R.; Pan, J. Z., Forgetting for knowledge bases in DL-lite, Ann. Math. Artif. Intell., 58, 117-151 (2010) · Zbl 1205.68410 |
| [45] | Wolter, F., Fusions of modal logics revisited, (Proceedings of the First Workshop on Advances in Modal Logic (AiML-1996) (1998), CSLI Publications), 361-379 · Zbl 0956.03512 |
| [46] | Wong, K. S., Forgetting in Logic Programs (2009), University of New South Wales, Ph.D. thesis |
| [47] | Zhang, Y.; Foo, N. Y., Solving logic program conflict through strong and weak forgettings, Artif. Intell., 170, 739-778 (2006) · Zbl 1131.68037 |
| [48] | Zhang, Y.; Zhou, Y., Knowledge forgetting: properties and applications, Artif. Intell., 173, 1525-1537 (2009) · Zbl 1187.03015 |
| [49] | Zhang, Y.; Zhou, Y., Forgetting revisited, (Proceedings of the Twelfth International Conference on Principles of Knowledge Representation and Reasoning (KR-2010) (2010), AAAI Press), 602-604 |
| [50] | Zhao, Y.; Schmidt, R. A., Concept forgetting in \(ALCOI\)-ontologies using an Ackerman approach, (Proceedings of the Fourth International Semantic Web Conference (ISWC-2015). Proceedings of the Fourth International Semantic Web Conference (ISWC-2015), Lecture Notes in Computer Science, vol. 9366 (2015), Springer), 587-602 |
| [51] | Zhao, Y.; Schmidt, R. A., Forgetting concept and role symbols in \(ALCOIH \mu^+(\nabla, \sqcap)\)-ontologies, (Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-2016) (2016), IJCAI/AAAI Press), 1345-1353 |
| [52] | Zhao, Y.; Schmidt, R. A., Role forgetting for \(ALCOQH(\nabla)\)-ontologies using an Ackermann-based approach, (Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-2017) (2017), IJCAI/AAAI Press), 1354-1361 |
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.
