{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T05:59:42Z","timestamp":1774418382581,"version":"3.50.1"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T00:00:00Z","timestamp":1498262400000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-09- C-0181 and FA8750-14-C-0021"],"award-info":[{"award-number":["FA8750-09- C-0181 and FA8750-14-C-0021"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-05- 2-0283, FA8750-14-C-0005, FA8750-07-D-0185, HR0011-06-C- 0025, HR0011-07-C-0060 and NBCH-D030010"],"award-info":[{"award-number":["FA8750-05- 2-0283, FA8750-14-C-0005, FA8750-07-D-0185, HR0011-06-C- 0025, HR0011-07-C-0060 and NBCH-D030010"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["IIS- 0534881 and IIS-0803481"],"award-info":[{"award-number":["IIS- 0534881 and IIS-0803481"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["W911NF-08-1-0242"],"award-info":[{"award-number":["W911NF-08-1-0242"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-08-1-0670"],"award-info":[{"award-number":["N00014-08-1-0670"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2016,6,24]]},"abstract":"<jats:p>Many representation schemes combining first-order logic and probability have been proposed in recent years. Progress in unifying logical and probabilistic inference has been slower. Existing methods are mainly variants of lifted variable elimination and belief propagation, neither of which take logical structure into account. We propose the first method that has the full power of both graphical model inference and first-order theorem proving (in finite domains with Herbrand interpretations). We first define probabilistic theorem proving (PTP), their generalization, as the problem of computing the probability of a logical formula given the probabilities or weights of a set of formulas. We then show how PTP can be reduced to the problem of lifted weighted model counting, and develop an efficient algorithm for the latter. We prove the correctness of this algorithm, investigate its properties, and show how it generalizes previous approaches. Experiments show that it greatly outperforms lifted variable elimination when logical structure is present. Finally, we propose an algorithm for approximate PTP, and show that it is superior to lifted belief propagation.<\/jats:p>","DOI":"10.1145\/2936726","type":"journal-article","created":{"date-parts":[[2016,6,27]],"date-time":"2016-06-27T09:41:38Z","timestamp":1467020498000},"page":"107-115","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Probabilistic theorem proving"],"prefix":"10.1145","volume":"59","author":[{"given":"Vibhav","family":"Gogate","sequence":"first","affiliation":[{"name":"University of Texas at Dallas, Richardson, TX"}]},{"given":"Pedro","family":"Domingos","sequence":"additional","affiliation":[{"name":"University of Washington Seattle, WA"}]}],"member":"320","published-online":{"date-parts":[[2016,6,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/102400"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/647288.721114"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.11.002"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00069-2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1625275.1625673"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1369181"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2006.11.003"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855041"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1296231"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.10.009"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/3023549.3023574"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90019-V"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Twenty-Fourth Annual Conference on Neural Information Processing Systems","author":"Jha A.","year":"2010","unstructured":"Jha, A., Gogate, V., Meliou, A., Suciu, D. Lifted inference from the other side: The tractable features. In Proceedings of the Twenty-Fourth Annual Conference on Neural Information Processing Systems (2010), 973--981."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1620163.1620237"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(86)90031-7"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1630659.1630801"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1597538.1597612"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/539488"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1619332.1619409"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_17"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1620163.1620242"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900006147"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2936726","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2936726","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2936726","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:47:52Z","timestamp":1763459272000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2936726"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,24]]},"references-count":25,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2016,6,24]]}},"alternative-id":["10.1145\/2936726"],"URL":"https:\/\/doi.org\/10.1145\/2936726","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,24]]},"assertion":[{"value":"2016-06-24","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}