{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:10:23Z","timestamp":1737501023761,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540766483"},{"type":"electronic","value":"9783540766506"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-76650-6_5","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T07:12:49Z","timestamp":1193382769000},"page":"57-75","source":"Crossref","is-referenced-by-count":0,"title":["A Verification Framework for Agent Knowledge"],"prefix":"10.1007","author":[{"given":"Jin Song","family":"Dong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuzhang","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ho-fung","family":"Leung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Arkoudas, K.: Athena. http:\/\/www.cag.csail.mit.edu\/~kostas\/dpls\/athena\/"},{"key":"5_CR2","series-title":"Lecture Notes in Artificial Intelligence","first-page":"50","volume-title":"CLIMA 2004","author":"K. Arkoudas","year":"2005","unstructured":"Arkoudas, K., Bringsjord, S.: Metareasoning for multi-agent epistemic logics. In: Leite, J.A., Torroni, P. (eds.) CLIMA 2004. LNCS (LNAI), vol.\u00a03487, pp. 50\u201365. Springer, Heidelberg (2005)"},{"issue":"6","key":"5_CR3","doi-asserted-by":"publisher","first-page":"1236","DOI":"10.1214\/aos\/1176343654","volume":"4","author":"R.J. Aumann","year":"1976","unstructured":"Aumann, R.J.: Agreeing to disagree. The Annals of Statistics\u00a04(6), 1236\u20131239 (1976)","journal-title":"The Annals of Statistics"},{"key":"5_CR4","unstructured":"Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge, and private suspicions. In: Proceedings of the 7th conference on theoretical aspects of rationality and knowledge, pp. 43\u201356 (1998)"},{"key":"5_CR5","first-page":"293","volume-title":"The Tbilisi Symposium on Logic, Language and Computation: Selected Papers","author":"D. Basin","year":"1998","unstructured":"Basin, D., Matthews, S., Vigan\u00f2, L.: A modular presentation of modal logics in a logical framework. In: Ginzburg, J., Khasidashvili, Z., Vogel, C., L\u00e9vy, J.-J., Vallduv\u00ed, E. (eds.) The Tbilisi Symposium on Logic, Language and Computation: Selected Papers, pp. 293\u2013307. CSLI Publications, Stanford, CA (1998)"},{"issue":"3","key":"5_CR6","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1093\/logcom\/8.3.401","volume":"8","author":"M. Benerecetti","year":"1998","unstructured":"Benerecetti, M., Giunchiglia, F., Serafini, L.: Model checking multiagent systems. Journal of Logic and Computation\u00a08(3), 401\u2013423 (1998)","journal-title":"Journal of Logic and Computation"},{"issue":"2-3","key":"5_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076(2-3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"5_CR8","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about knowledge. MIT Press, Cambridge, Mass. (1995)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-540-27813-9_41","volume-title":"CAV 2004","author":"P. Gammie","year":"2004","unstructured":"Gammie, P., van der Meyden, R.: Mck: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 479\u2013483. Springer, Heidelberg (2004)"},{"key":"5_CR10","unstructured":"Gerbrandy, J.: Bisimulations on Planet Kripke. PhD thesis, University of Amsterdam (1999)"},{"key":"5_CR11","first-page":"325","volume-title":"KR 1991","author":"J.Y. Halpern","year":"1991","unstructured":"Halpern, J.Y., Vardi, M.Y.: Model checking vs. theorem proving: A manifesto. In: Allen, J., Fikes, R.E., Sandewall, E. (eds.) KR 1991, pp. 325\u2013334. Morgan Kaufmann Publishers, San Mateo, CA (1991)"},{"key":"5_CR12","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M. Huth","year":"1999","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (1999)"},{"key":"5_CR13","unstructured":"Kim, J.-S., Kowalski, R.A.: An application of amalgamated logic to multi-agent belief. In: Proceedings MetaLogic 1990, pp. 272\u2013283 (1990)"},{"key":"5_CR14","volume-title":"Convention: A Philosophical Study","author":"D.K. Lewis","year":"1969","unstructured":"Lewis, D.K.: Convention: A Philosophical Study. Harvard University Press, Cambridge, MA (1969)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Lutz, C.: Complexity and succinctness of public announcement logic. In: Proceedings of the 5th international joint conference on Autonomous agents and multiagent systems, pp. 137\u2013143 (2006)","DOI":"10.1145\/1160633.1160657"},{"key":"5_CR16","unstructured":"McCarthy, J.: Formalization of common sense. In: Lifschitz, V. (ed.) Ablex (1990)"},{"key":"5_CR17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569852","volume-title":"Epistemic Logic for AI and Computer Science","author":"J.-J.C. Meyer","year":"1995","unstructured":"Meyer, J.-J.C., Hoek, W.V.D.: Epistemic Logic for AI and Computer Science. Cambridge University Press, New York (1995)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/860575.860609","volume-title":"AAMAS 2003","author":"W. Penczek","year":"2003","unstructured":"Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: AAMAS 2003, pp. 209\u2013216. ACM Press, New York (2003)"},{"key":"5_CR21","unstructured":"Plaza, J.A.: Logics of public communications. In: Emrich, M.L., Pfeifer, M.S., Hadzikadic, M., Ras, Z.W. (eds.) Proceedings of the 4th International Symposium on Methodologies for Intelligent Systems, pp. 201\u2013216 (1989)"},{"key":"5_CR22","unstructured":"Sadrzadeh, M.: Modal linear logic in higher order logic, an experiment in coq. In: Basin, D., Burkhart, W. (eds.) Proceedings of Theorem Proving in Higher Order Logics, Rome, Italy, pp. 75\u201393 (2003)"},{"key":"5_CR23","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/3-540-46017-9_9","volume-title":"Proceedings of the 9th International SPIN Workshop on Model Checking of Software","author":"W. Hoek van der","year":"2002","unstructured":"van der Hoek, W., Wooldridge, M.: Model checking knowledge and time. In: Proceedings of the 9th International SPIN Workshop on Model Checking of Software, pp. 95\u2013111. Springer, London (2002)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"van Ditmarsch, H.P., van der Hoek, W., Kooi, B.P.: Dynamic epistemic logic with assignment. In: Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, New York, NY, USA, pp. 141\u2013148 (2005)","DOI":"10.1145\/1082473.1082495"},{"key":"5_CR25","volume-title":"Dynamic Epistemic Logic","author":"H.P. Ditmarsch van","year":"2006","unstructured":"van Ditmarsch, H.P., van der Hoek, W., Kooi, B.P.: Dynamic Epistemic Logic. Springer, Heidelberg (2006)"},{"key":"5_CR26","unstructured":"van Eijck, J.: Dynamic epistemic modelling. CWI Technical Report SEN-E0424, Centrum voor Wiskunde en Informatica, Armsterdam (2004)"},{"key":"5_CR27","doi-asserted-by":"publisher","first-page":"952","DOI":"10.1145\/544862.544965","volume-title":"AAMAS 2002","author":"M. Wooldridge","year":"2002","unstructured":"Wooldridge, M., Fisher, M., Huget, M.-P., Parsons, S.: Model checking multi-agent systems with mable. In: AAMAS 2002, pp. 952\u2013959. ACM Press, New York (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-76650-6_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T22:42:41Z","timestamp":1737499361000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-76650-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540766483","9783540766506"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-76650-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}