{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:31:06Z","timestamp":1753889466620,"version":"3.41.0"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,8,13]],"date-time":"2019-08-13T00:00:00Z","timestamp":1565654400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R026092\/1, EP\/R026084\/1, EP\/N007565\/1"],"award-info":[{"award-number":["EP\/R026092\/1, EP\/R026084\/1, EP\/N007565\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>Resolution-based provers for multimodal normal logics require pruning of the search space for a proof to ameliorate the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution calculus for the basic multimodal logic, which divides the clause set according to the modal level at which clauses occur to reduce the number of possible inferences. We show that the calculus is complete for the logics being considered. We also show that the calculus can be combined with other strategies. In particular, we discuss the completeness of combining modal layering with negative and ordered resolution and provide experimental results comparing the different refinements.<\/jats:p>","DOI":"10.1145\/3331448","type":"journal-article","created":{"date-parts":[[2019,8,13]],"date-time":"2019-08-13T14:41:50Z","timestamp":1565707310000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Modal Resolution"],"prefix":"10.1145","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9792-5346","authenticated-orcid":false,"given":"Cl\u00e1udia","family":"Nalon","sequence":"first","affiliation":[{"name":"University of Bras\u00edlia, Bras\u00edlia, DF, Brazil"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5995-7494","authenticated-orcid":false,"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0455-0267","authenticated-orcid":false,"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,8,13]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/3006433.3006476"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9167-0"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/648238.751545"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753624"},{"key":"e_1_2_1_6_1","volume-title":"Patel-Schneider","author":"Baader Franz","year":"2003","unstructured":"Franz Baader , Diego Calvanese , Deborah L. McGuinness , Daniele Nardi , and Peter F . Patel-Schneider . 2003 . The Description Logic Handbook: Theory, Implementation , and Applications. Cambridge University Press . Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider. 2003. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press."},{"volume-title":"Handbook of Automated Reasoning","author":"Baaz Matthias","key":"e_1_2_1_7_1","unstructured":"Matthias Baaz , Uwe Egly , and Alexander Leitsch . 2001. Normal form transformations . In Handbook of Automated Reasoning , Alan Robinson and Andrei Voronkov (Eds.), vol. I . Elsevier and MIT Press , 273--333. Matthias Baaz, Uwe Egly, and Alexander Leitsch. 2001. Normal form transformations. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.), vol. I. Elsevier and MIT Press, 273--333."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR\u201992)","volume":"624","author":"Baaz Matthias","unstructured":"Matthias Baaz and Christian G. Ferm\u00fcller . 1992. Resolution for many-valued logics . In Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR\u201992) (Lecture Notes in Computer Science), Andre Voronkov (Ed.) , vol. 624 . Springer, 107--118. Matthias Baaz and Christian G. Ferm\u00fcller. 1992. Resolution for many-valued logics. In Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR\u201992) (Lecture Notes in Computer Science), Andre Voronkov (Ed.), vol. 624. Springer, 107--118."},{"volume-title":"Handbook of Automated Reasoning","author":"Baaz Matthias","key":"e_1_2_1_9_1","unstructured":"Matthias Baaz , Christian G. Ferm\u00fcller , and Gernot Salzer . 2001. Automated deduction for many-valued logics . In Handbook of Automated Reasoning , Alan Robinson and Andrei Voronkov (Eds.), vol. II . Elsevier and MIT Press , chap. 20, 1355--1402. Matthias Baaz, Christian G. Ferm\u00fcller, and Gernot Salzer. 2001. Automated deduction for many-valued logics. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.), vol. II. Elsevier and MIT Press, chap. 20, 1355--1402."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/648229.752455"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 15th International Joint Conference on Artificiall Intelligence (JCAI\u201997)","author":"Balbiani Philippe","year":"1997","unstructured":"Philippe Balbiani and St\u00e9phane Demri . 1997 . Prefixed tableaux systems for modal logics with enriched languages . In Proceedings of the 15th International Joint Conference on Artificiall Intelligence (JCAI\u201997) . Morgan Kaufmann, 190--195. Philippe Balbiani and St\u00e9phane Demri. 1997. Prefixed tableaux systems for modal logics with enriched languages. In Proceedings of the 15th International Joint Conference on Artificiall Intelligence (JCAI\u201997). Morgan Kaufmann, 190--195."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006249507577"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.6.685"},{"volume-title":"Modal Logic","author":"Blackburn Patrick","key":"e_1_2_1_14_1","unstructured":"Patrick Blackburn , Maarten de Rijke , and Yde Venema . 2001. Modal Logic . Cambridge University Press . Patrick Blackburn, Maarten de Rijke, and Yde Venema. 2001. Modal Logic. Cambridge University Press."},{"volume-title":"Handbook of Philosophical Logic","author":"Bra\u00fcner Torben","key":"e_1_2_1_15_1","unstructured":"Torben Bra\u00fcner . 2014. Hybrid logic . In Handbook of Philosophical Logic , vol. 17 . Dov M. Gabbay and Franz Guenthner (Eds.). Springer , 1--77. Torben Bra\u00fcner. 2014. Hybrid logic. In Handbook of Philosophical Logic, vol. 17. Dov M. Gabbay and Franz Guenthner (Eds.). Springer, 1--77."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/648228.752151"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.004"},{"key":"e_1_2_1_18_1","volume-title":"Mendelsohn","author":"Fitting Melvin","year":"1998","unstructured":"Melvin Fitting and Richard L . Mendelsohn . 1998 . First-Order Modal Logic. Kluwer . Melvin Fitting and Richard L. Mendelsohn. 1998. First-Order Modal Logic. Kluwer."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.1.5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_25"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.04.010"},{"volume-title":"Automated Deduction in Multiple-Valued Logics","author":"H\u00e4hnle Reiner","key":"e_1_2_1_22_1","unstructured":"Reiner H\u00e4hnle . 1993. Automated Deduction in Multiple-Valued Logics . Oxford University Press . Reiner H\u00e4hnle. 1993. Automated Deduction in Multiple-Valued Logics. Oxford University Press."},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"Verifying Concurrent Processes Using Temporal Logic","author":"Hailpern Brent T.","unstructured":"Brent T. Hailpern . 1982. Verifying Concurrent Processes Using Temporal Logic . Lecture Notes in Computer Science , vol. 129 . Springer . Brent T. Hailpern. 1982. Verifying Concurrent Processes Using Temporal Logic. Lecture Notes in Computer Science, vol. 129. Springer."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1146\/annurev.cs.02.060187.000345"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/646237.683015"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(92)90049-4"},{"key":"e_1_2_1_27_1","volume-title":"Kowalski","author":"Hayes Patrick J.","year":"1969","unstructured":"Patrick J. Hayes and Robert A . Kowalski . 1969 . Semantic trees in automatic theorem proving. In Proceedings of the 4th Annual Machine Intelligence Workshop. Elsevier , 87--101. Patrick J. Hayes and Robert A. Kowalski. 1969. Semantic trees in automatic theorem proving. In Proceedings of the 4th Annual Machine Intelligence Workshop. Elsevier, 87--101."},{"key":"e_1_2_1_28_1","volume-title":"Schmidt","author":"Horrocks Ian","year":"2006","unstructured":"Ian Horrocks , Ullrich Hustadt , Ulrike Sattler , and Renate A . Schmidt . 2006 . Computational modal logic. In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Elsevier , 181--245. Ian Horrocks, Ullrich Hustadt, Ulrike Sattler, and Renate A. Schmidt. 2006. Computational modal logic. In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Elsevier, 181--245."},{"volume-title":"Collegium Logicum","author":"Hustadt Ullrich","key":"e_1_2_1_29_1","unstructured":"Ullrich Hustadt and Boris Konev . 2004. TRP++ : A temporal resolution prover . In Collegium Logicum . Kurt G\u00f6del Society , 65--79. Ullrich Hustadt and Boris Konev. 2004. TRP++: A temporal resolution prover. In Collegium Logicum. Kurt G\u00f6del Society, 65--79."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_31"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"volume-title":"Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem","author":"Marx Maarten","key":"e_1_2_1_34_1","unstructured":"Maarten Marx . 2006. Complexity of modal logic . In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem , and Frank Wolter (Eds.). Elsevier , New York , 139--179. Maarten Marx. 2006. Complexity of modal logic. In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Elsevier, New York, 139--179."},{"volume-title":"Finite Model Theory and Its Applications","author":"Marx Maarten","key":"e_1_2_1_35_1","unstructured":"Maarten Marx and Yde Venema . 2007. Local variations on a loose theme: Modal logic and decidability . In Finite Model Theory and Its Applications . Springer , 371--429. Maarten Marx and Yde Venema. 2007. Local variations on a loose theme: Modal logic and decidability. In Finite Model Theory and Its Applications. Springer, 371--429."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/646891.709414"},{"key":"e_1_2_1_37_1","unstructured":"William W. McCune. 2007. OTTER 3.0 reference manual and guide.  William W. McCune. 2007. OTTER 3.0 reference manual and guide."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(72)90047-1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jalgor.2007.04.001"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_13"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_28"},{"key":"e_1_2_1_42_1","unstructured":"Cl\u00e1udia Nalon Ullrich Hustadt and Clare Dixon. 2016. K<sub>S<\/sub>P : Sources and benchmarks. Retrieved from http:\/\/www.cic.unb.br\/nalon\/#software.  Cl\u00e1udia Nalon Ullrich Hustadt and Clare Dixon. 2016. K<sub>S<\/sub>P : Sources and benchmarks. Retrieved from http:\/\/www.cic.unb.br\/nalon\/#software."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/3171837.3171985"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Cl\u00e1udia Nalon Ullrich Hustadt and Clare Dixon. 2018. K<sub>S<\/sub>P a resolution-based theorem prover for K<sub>n<\/sub>: Architecture refinements strategies and experiments. J. Auto. Reason. To appear.  Cl\u00e1udia Nalon Ullrich Hustadt and Clare Dixon. 2018. K<sub>S<\/sub>P a resolution-based theorem prover for K<sub> n <\/sub>: Architecture refinements strategies and experiments. J. Auto. Reason. To appear.","DOI":"10.1007\/s10817-018-09503-x"},{"volume-title":"Handbook of Automated Reasoning","author":"Nonnengart Andreas","key":"e_1_2_1_45_1","unstructured":"Andreas Nonnengart and Christoph Weidenbach . 2001. Computing small clause normal forms . In Handbook of Automated Reasoning , Alan Robinson and Andrei Voronkov (Eds.), vol. 1 . Elsevier and MIT Press , 335--367. Andreas Nonnengart and Christoph Weidenbach. 2001. Computing small clause normal forms. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.), vol. 1. Elsevier and MIT Press, 335--367."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/648228.752115"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.5.691"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.5.581"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the 19th International Conference on Automated Deduction (CADE\u201903)","volume":"2741","author":"Pan Guoqiang","unstructured":"Guoqiang Pan and Moshe Y. Vardi . 2003. Optimizing a BDD-based modal solver . In Proceedings of the 19th International Conference on Automated Deduction (CADE\u201903) (Lecture Notes in Computer Science) , vol. 2741 . Springer, 75--89. Guoqiang Pan and Moshe Y. Vardi. 2003. Optimizing a BDD-based modal solver. In Proceedings of the 19th International Conference on Automated Deduction (CADE\u201903) (Lecture Notes in Computer Science), vol. 2741. Springer, 75--89."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622420.1622430"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370324"},{"volume-title":"Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR8R\u201991)","author":"Anand","key":"e_1_2_1_53_1","unstructured":"Anand S. Rao and Michael P. Georgeff. 1991. Modeling rational agents within a BDI-architecture . In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR8R\u201991) . Morgan-Kaufmann, 473--484. Anand S. Rao and Michael P. Georgeff. 1991. Modeling rational agents within a BDI-architecture. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR8R\u201991). Morgan-Kaufmann, 473--484."},{"key":"e_1_2_1_54_1","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson John Alan","year":"1965","unstructured":"John Alan Robinson . 1965 . Automatic deduction with hyper-resolution . Int. J. Comput. Math. 1 (1965), 227 -- 234 . John Alan Robinson. 1965. Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1 (1965), 227--234.","journal-title":"Int. J. Comput. Math."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI\u201991)","author":"Schild Klaus","year":"1991","unstructured":"Klaus Schild . 1991 . A correspondence theory for terminological logics . In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI\u201991) . Morgan Kaufmann, 466--471. Klaus Schild. 1991. A correspondence theory for terminological logics. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI\u201991). Morgan Kaufmann, 466--471."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006043519663"},{"key":"e_1_2_1_58_1","unstructured":"Stephan Schulz. 2013. The E Theorem Prover. Retrieved from http:\/\/wwwlehre.dhbw-stuttgart.de\/ sschulz\/E\/E.html.  Stephan Schulz. 2013. The E Theorem Prover. Retrieved from http:\/\/wwwlehre.dhbw-stuttgart.de\/ sschulz\/E\/E.html."},{"volume-title":"Automated Reasoning and Mathematics\u2014Essays in Memory of William W. McCune (Lecture Notes in Computer Science), Maria Paola Bonacina and Mark E","author":"Schulz Stephan","key":"e_1_2_1_59_1","unstructured":"Stephan Schulz . 2013. Simple and efficient clause subsumption with feature vector indexing . In Automated Reasoning and Mathematics\u2014Essays in Memory of William W. McCune (Lecture Notes in Computer Science), Maria Paola Bonacina and Mark E . Stickel (Eds.), vol. 7788 . Springer , 45--67. Stephan Schulz. 2013. Simple and efficient clause subsumption with feature vector indexing. In Automated Reasoning and Mathematics\u2014Essays in Memory of William W. McCune (Lecture Notes in Computer Science), Maria Paola Bonacina and Mark E. Stickel (Eds.), vol. 7788. Springer, 45--67."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2014.01.002"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321428"},{"volume-title":"Proceedings of the 1st International Joint Conference on Artificial Intelligence (IJCAI\u201969)","author":"Slagle James R.","key":"e_1_2_1_62_1","unstructured":"James R. Slagle , C. L. Chang , and Richard C. T. Lee . 1969. Completeness theorems for semantic resolution in consequence-finding . In Proceedings of the 1st International Joint Conference on Artificial Intelligence (IJCAI\u201969) . William Kaufmann, 281--286. James R. Slagle, C. L. Chang, and Richard C. T. Lee. 1969. Completeness theorems for semantic resolution in consequence-finding. In Proceedings of the 1st International Joint Conference on Artificial Intelligence (IJCAI\u201969). William Kaufmann, 281--286."},{"key":"e_1_2_1_64_1","unstructured":"The SPASS Team. 2010. Automation of Logic: SPASS. Retrieved from http:\/\/www.spass-prover.org\/.  The SPASS Team. 2010. Automation of Logic: SPASS. Retrieved from http:\/\/www.spass-prover.org\/."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_26"},{"key":"e_1_2_1_66_1","unstructured":"Andrei Voronkov. 2013. Vampire. Retrieved from http:\/\/www.vprover.org\/index.cgi.  Andrei Voronkov. 2013. Vampire. Retrieved from http:\/\/www.vprover.org\/index.cgi."},{"volume-title":"Handbook of Automated Reasoning","author":"Waaler Arild","key":"e_1_2_1_67_1","unstructured":"Arild Waaler . 2001. Connections in nonclassical logics . In Handbook of Automated Reasoning , Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press , 1487--1578. Arild Waaler. 2001. Connections in nonclassical logics. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press, 1487--1578."},{"volume-title":"Automated Deduction in Non-Classical Logics","author":"Wallen Lincoln A.","key":"e_1_2_1_68_1","unstructured":"Lincoln A. Wallen . 1990. Automated Deduction in Non-Classical Logics . MIT Press . Lincoln A. Wallen. 1990. Automated Deduction in Non-Classical Logics. MIT Press."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/321296.321302"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331448","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331448","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:28Z","timestamp":1750207408000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331448"}},"subtitle":["Proofs, Layers, and Refinements"],"short-title":[],"issued":{"date-parts":[[2019,8,13]]},"references-count":67,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3331448"],"URL":"https:\/\/doi.org\/10.1145\/3331448","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,8,13]]},"assertion":[{"value":"2017-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-08-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}