{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:16Z","timestamp":1740123376165,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,11,29]],"date-time":"2018-11-29T00:00:00Z","timestamp":1543449600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,11,29]],"date-time":"2018-11-29T00:00:00Z","timestamp":1543449600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["1740079","1750009"],"award-info":[{"award-number":["1740079","1750009"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006754","name":"Army Research Laboratory","doi-asserted-by":"publisher","award":["US ARL Cooperative Agreement W911NF-17-2-0196 on Internet of Battle Things (IoBT)"],"award-info":[{"award-number":["US ARL Cooperative Agreement W911NF-17-2-0196 on Internet of Battle Things (IoBT)"]}],"id":[{"id":"10.13039\/100006754","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10817-018-9499-8","type":"journal-article","created":{"date-parts":[[2018,11,29]],"date-time":"2018-11-29T11:45:03Z","timestamp":1543491903000},"page":"1055-1075","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5983-9095","authenticated-orcid":false,"given":"Susmit","family":"Jha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tuhin","family":"Sahai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vasumathi","family":"Raman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Pinto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Francis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,11,29]]},"reference":[{"key":"9499_CR1","doi-asserted-by":"crossref","unstructured":"Abouzied, A., Angluin, D., Papadimitriou, C., Hellerstein, J.M., Silberschatz, A.: Learning and verifying quantified boolean queries by example. In: ACM Symposium on Principles of Database Systems, pp. 49\u201360. ACM (2013)","DOI":"10.1145\/2463664.2465220"},{"key":"9499_CR2","doi-asserted-by":"crossref","unstructured":"Angluin, D.: Computational learning theory: survey and selected bibliography. In: ACM Symposium on Theory of Computing, pp. 351\u2013369. ACM (1992)","DOI":"10.1145\/129712.129746"},{"key":"9499_CR3","doi-asserted-by":"crossref","unstructured":"Angluin, D., Kharitonov, M.: When won\u2019t membership queries help? In: ACM Symposium on Theory of Computing, pp. 444\u2013454. ACM (1991)","DOI":"10.1145\/103418.103420"},{"issue":"Jun","key":"9499_CR4","first-page":"1803","volume":"11","author":"D Baehrens","year":"2010","unstructured":"Baehrens, D., Schroeter, T., Harmeling, S., Kawanabe, M., Hansen, K., A\u017eller, K.-R.M.: How to explain individual classification decisions. J. Mach. Learn. Res. 11(Jun), 1803\u20131831 (2010)","journal-title":"J. Mach. Learn. Res."},{"key":"9499_CR5","doi-asserted-by":"crossref","unstructured":"Bittner, B., Bozzano, M., Cimatti, A., Gario, M., Griggio, A.: Towards pareto-optimal parameter synthesis for monotonie cost functions. In: FMCAD, pp. 23\u201330 (2014)","DOI":"10.1109\/FMCAD.2014.6987591"},{"key":"9499_CR6","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Godefroid, P.: Automatic synthesis of specifications from the dynamic observation of reactive programs. In: TACAS, pp. 321\u2013333 (1997)","DOI":"10.1007\/BFb0035397"},{"issue":"1","key":"9499_CR7","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1080\/15326349708807412","volume":"13","author":"A Boneh","year":"1997","unstructured":"Boneh, A., Hofri, M.: The coupon-collector problem revisiteda survey of engineering problems and computational methods. Stoch. Models 13(1), 39\u201366 (1997)","journal-title":"Stoch. Models"},{"issue":"1","key":"9499_CR8","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/2480359.2429123","volume":"48","author":"Matko Botin\u010dan","year":"2013","unstructured":"Botin\u010dan, M., Babi\u0107, D.: Sigma*: symbolic learning of input-output specifications. In: POPL, pp. 443\u2013456 (2013)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"9499_CR9","first-page":"93","volume":"43","author":"B Cook","year":"2013","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. FMSD 43(1), 93\u2013120 (2013)","journal-title":"FMSD"},{"issue":"11","key":"9499_CR10","doi-asserted-by":"publisher","first-page":"2664","DOI":"10.1109\/TNNLS.2015.2389037","volume":"26","author":"EJ de Fortuny","year":"2015","unstructured":"de Fortuny, E.J., Martens, D.: Active learning-based pedagogical rule extraction. IEEE Trans. Neural Netw. Learn. Syst. 26(11), 2664\u20132677 (2015)","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"9499_CR11","doi-asserted-by":"crossref","unstructured":"Dutta, S., Jha, S., Sanakaranarayanan, S., Tiwari, A.: Output range analysis for deep neural networks. arXiv preprint, \n                    arXiv:1709.09130\n                    \n                   (2017)","DOI":"10.1007\/978-3-319-77935-5_9"},{"issue":"3","key":"9499_CR12","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/0890-5401(89)90002-3","volume":"82","author":"A Ehrenfeucht","year":"1989","unstructured":"Ehrenfeucht, A., Haussler, D., Kearns, M., Valiant, L.: A general lower bound on the number of examples needed for learning. Inf. Comput. 82(3), 247\u2013261 (1989)","journal-title":"Inf. Comput."},{"key":"9499_CR13","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-05258-3_5","volume-title":"MICAI 2009: Advances in Artificial Intelligence","author":"Francisco Elizalde","year":"2009","unstructured":"Elizalde, F., Sucar, E., Noguez, J., Reyes, A.: Generating Explanations Based on Markov Decision Processes, pp. 51\u201362 (2009)"},{"key":"9499_CR14","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1016\/B978-1-55860-247-2.50025-5","volume-title":"Machine Learning Proceedings 1992","author":"Cao Feng","year":"1992","unstructured":"Feng, C., Muggleton, S.: Towards inductive generalisation in higher order logic. In: 9th International Workshop on Machine learning, pp. 154\u2013162 (2014)"},{"issue":"6","key":"9499_CR15","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1145\/2345156.2254116","volume":"47","author":"P Godefroid","year":"2012","unstructured":"Godefroid, P., Taly, A.: Automated synthesis of symbolic instruction encodings from i\/o samples. SIGPLAN Not. 47(6), 441\u2013452 (2012)","journal-title":"SIGPLAN Not."},{"issue":"2","key":"9499_CR16","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.artint.2004.01.002","volume":"156","author":"J Goldsmith","year":"2004","unstructured":"Goldsmith, J., Sloan, R.H., Sz\u00f6r\u00e9nyi, B., Tur\u00e1n, G.: Theory revision with queries: horn, read-once, and parity formulas. Artif. Intell. 156(2), 139\u2013176 (2004)","journal-title":"Artif. Intell."},{"key":"9499_CR17","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-54862-8_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Arie Gurfinkel","year":"2014","unstructured":"Gurfinkel, A., Belov, A., Marques-Silva, J.: Synthesizing Safe Bit-Precise Invariants, pp. 93\u2013108 (2014)"},{"key":"9499_CR18","first-page":"6","volume":"12","author":"M Harbers","year":"2010","unstructured":"Harbers, M., Meyer, J.-J., van den Bosch, K.: Explaining simulations through self explaining agents. J. Artif. Soc. Soc. Simul. 12, 6 (2010)","journal-title":"J. Artif. Soc. Soc. Simul."},{"issue":"1","key":"9499_CR19","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/j.tcs.2007.05.018","volume":"384","author":"L Hellerstein","year":"2007","unstructured":"Hellerstein, L., Servedio, R.A.: On pac learning algorithms for rich boolean function classes. Theor. Comput. Sci. 384(1), 66\u201376 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9499_CR20","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: In: Oracle-guided component-based program synthesis. In: ICSE, pp. 215\u2013224. IEEE (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"9499_CR21","unstructured":"Jha, S., Raman, V., Pinto, A., Sahai, T., Francis, M.: On learning sparse boolean formulae for explaining AI decisions. In: NASA Formal Methods\u20149th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16\u201318, 2017, Proceedings, pp. 99\u2013114 (2017)"},{"key":"9499_CR22","doi-asserted-by":"crossref","unstructured":"Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. In: Acta Informatica, Special Issue on Synthesis (2016)","DOI":"10.1007\/s00236-017-0294-5"},{"key":"9499_CR23","doi-asserted-by":"crossref","unstructured":"Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT, pp. 107\u2013116. ACM (2011)","DOI":"10.1145\/2038642.2038660"},{"issue":"6","key":"9499_CR24","doi-asserted-by":"publisher","first-page":"1298","DOI":"10.1145\/195613.195656","volume":"41","author":"M Kearns","year":"1994","unstructured":"Kearns, M., Li, M., Valiant, L.: Learning boolean formulas. J. ACM 41(6), 1298\u20131328 (1994)","journal-title":"J. ACM"},{"issue":"1","key":"9499_CR25","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/174644.174647","volume":"41","author":"M Kearns","year":"1994","unstructured":"Kearns, M., Valiant, L.: Cryptographic limitations on learning boolean formulae and finite automata. J. ACM 41(1), 67\u201395 (1994)","journal-title":"J. ACM"},{"key":"9499_CR26","doi-asserted-by":"crossref","unstructured":"Lakkaraju, H., Bach, S.H., Leskovec, J.: Interpretable decision sets: a joint framework for description and prediction. In: Proceedings of the 22nd ACM SIGKDD international conference on knowledge discovery and data mining, pp. 1675\u20131684. ACM (2016)","DOI":"10.1145\/2939672.2939874"},{"key":"9499_CR27","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546877","volume-title":"Planning Algorithms","author":"SM LaValle","year":"2006","unstructured":"LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)"},{"key":"9499_CR28","unstructured":"Lecun, Y., Cortes, C.: The MNIST database of handwritten digits. \n                    http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"issue":"10","key":"9499_CR29","doi-asserted-by":"publisher","first-page":"1243","DOI":"10.1080\/00140139208967392","volume":"35","author":"J Lee","year":"1992","unstructured":"Lee, J., Moray, N.: Trust, control strategies and allocation of function in human\u2013machine systems. Ergonomics 35(10), 1243\u20131270 (1992)","journal-title":"Ergonomics"},{"key":"9499_CR30","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-1-4615-2696-4_11","volume-title":"Theoretical Advances in Neural Computation and Learning","author":"Yishay Mansour","year":"1994","unstructured":"Mansour, Y.: Learning boolean functions via the Fourier transform. In: Theoretical Advances in Neural Computation and Learning, pp. 391\u2013424 (1994)"},{"key":"9499_CR31","volume-title":"Automated Planning: Theory & Practice","author":"D Nau","year":"2004","unstructured":"Nau, D., Ghallab, M., Traverso, P.: Automated Planning: Theory & Practice. Morgan Kaufmann Publishers Inc., San Francisco (2004)"},{"issue":"4","key":"9499_CR32","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1145\/48014.63140","volume":"35","author":"L Pitt","year":"1988","unstructured":"Pitt, L., Valiant, L.G.: Computational limitations on learning from examples. J. ACM 35(4), 965\u2013984 (1988)","journal-title":"J. ACM"},{"key":"9499_CR33","doi-asserted-by":"crossref","unstructured":"Raman, V.: Reactive switching protocols for multi-robot high-level tasks. In: IEEE\/RSJ, pp. 336\u2013341 (2014)","DOI":"10.1109\/IROS.2014.6942581"},{"key":"9499_CR34","doi-asserted-by":"crossref","unstructured":"Raman, V., Lignos, C., Finucane, C., Lee, K.C.T., Marcus, M.P., Kress-Gazit, H.: Sorry Dave, I\u2019m Afraid I can\u2019t do that: Explaining unachievable robot tasks using natural language. In: Robotics: Science and Systems (2013)","DOI":"10.15607\/RSS.2013.IX.023"},{"key":"9499_CR35","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, pp. 198\u2013216 (2015)","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"9499_CR36","doi-asserted-by":"crossref","unstructured":"Ribeiro, M.T., Singh, S., Guestrin, C.: Why Should I Trust You?: explaining the predictions of any classifier. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, pp. 1135\u20131144. ACM (2016)","DOI":"10.1145\/2939672.2939778"},{"key":"9499_CR37","doi-asserted-by":"crossref","unstructured":"Ribeiro, M.T., Singh, S., Guestrin, C.: \u201cWhy Should I Trust You?\u201d: explaining the predictions of any classifier. In: KDD, pp. 1135\u20131144 (2016)","DOI":"10.18653\/v1\/N16-3020"},{"issue":"5","key":"9499_CR38","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1109\/TKDE.2007.190734","volume":"20","author":"M Robnik-\u0160ikonja","year":"2008","unstructured":"Robnik-\u0160ikonja, M., Kononenko, I.: Explaining classifications for individual instances. IEEE Trans. Knowl. Data Eng. 20(5), 589\u2013600 (2008)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"9499_CR39","unstructured":"Russell, J., Cohn, R.: OODA loop. In: Book on Demand (2012)"},{"key":"9499_CR40","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC, pp. 221\u2013230 (2010)","DOI":"10.1145\/1755952.1755984"},{"key":"9499_CR41","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Miller, C., Raghunathan, R., Ravanbakhsh, H., Fainekos, G.: A model-based approach to synthesizing insulin infusion pump usage parameters for diabetic patients. In: Annual Allerton Conference on Communication, Control, and Computing, pp. 1610\u20131617 (2012)","DOI":"10.1109\/Allerton.2012.6483413"},{"issue":"1","key":"9499_CR42","first-page":"25","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. FMSD 32(1), 25\u201355 (2008)","journal-title":"FMSD"},{"issue":"3","key":"9499_CR43","first-page":"647","volume":"41","author":"E \u0160trumbelj","year":"2014","unstructured":"\u0160trumbelj, E., Kononenko, I.: Explaining prediction models and individual predictions with feature contributions. KIS 41(3), 647\u2013665 (2014)","journal-title":"KIS"},{"key":"9499_CR44","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-662-49674-9_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Caterina Urban","year":"2016","unstructured":"Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing Ranking Functions from Bits and Pieces, pp. 54\u201370 (2016)"},{"key":"9499_CR45","first-page":"309","volume":"42","author":"C Yuan","year":"2011","unstructured":"Yuan, C., Lim, H., Lu, T.-C.: Most relevant explanation in bayesian networks. J. Artif. Intell. Res. (JAIR) 42, 309\u2013352 (2011)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"9499_CR46","unstructured":"Zintgraf, L.M., Cohen, T.S., Adel, T., Welling, M.: Visualizing deep neural network decisions: prediction difference analysis. arXiv preprint \n                    arXiv:1702.04595\n                    \n                   (2017)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9499-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9499-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9499-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T23:05:11Z","timestamp":1589411111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9499-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,29]]},"references-count":46,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["9499"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9499-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,11,29]]},"assertion":[{"value":"11 November 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 November 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}