{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,28]],"date-time":"2023-09-28T12:11:34Z","timestamp":1695903094953},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2023,7,25]],"date-time":"2023-07-25T00:00:00Z","timestamp":1690243200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,7,25]],"date-time":"2023-07-25T00:00:00Z","timestamp":1690243200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Datenschutz Datensich"],"published-print":{"date-parts":[[2023,8]]},"DOI":"10.1007\/s11623-023-1804-y","type":"journal-article","created":{"date-parts":[[2023,7,25]],"date-time":"2023-07-25T18:02:45Z","timestamp":1690308165000},"page":"487-491","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Lazily-Verifiable SAT Proof Checker in SPARK 2014"],"prefix":"10.1007","volume":"47","author":[{"given":"Andr\u00e9","family":"Dietrich","sequence":"first","affiliation":[]},{"given":"Christopher","family":"Schmidt","sequence":"additional","affiliation":[]},{"given":"Nico","family":"Enghardt","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Philipp","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,25]]},"reference":[{"issue":"5-6","key":"1804_CR1","doi-asserted-by":"publisher","first-page":"891","DOI":"10.1017\/S1471068419000255","volume":"19","author":"M Alviano","year":"2019","unstructured":"Mario Alviano, Carmine Dodaro, Johannes Klaus Fichte, Markus Hecher, Tobias Philipp, and Jakob Rath: Inconsistency proofs for ASP: the ASP \u2013 DRUPE format. Theory Pract. Log. Program., 19(5-6):891\u2013907, 2019.","journal-title":"Theory Pract. Log. Program."},{"key":"1804_CR2","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider-Kamp: Efficient certified RAT verification. In: Leonardo de Moura, editor, CADE 2017, volume 10395of LNCS, pages 220\u2013236. Springer, 2017.","DOI":"10.1007\/978-3-319-63046-5_14"},{"issue":"3","key":"1804_CR3","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"M. Davis and H. Putnam: A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3):201\u2013215, 1960.","journal-title":"Journal of the ACM"},{"issue":"7","key":"1804_CR4","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Martin Davis, George Logemann, and Donald W. Loveland: A machine program for theorem-proving. Communications of the ACM, 5(7):394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"1804_CR5","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson: An extensible sat solver. In: International Conference on Theory and Applications of Satisfiability Testing, 2003."},{"issue":"6","key":"1804_CR6","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/3560469","volume":"66","author":"JK Fichte","year":"2023","unstructured":"Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider: The silent (r)evolution of sat. Commun. ACM, 66(6):64\u201372, may 2023.","journal-title":"Commun. ACM"},{"key":"1804_CR7","unstructured":"Johannes Klaus Fichte, Markus Hecher, and Valentin Roland: Proofs for propositional model counting. In: Kuldeep S. Meel and Ofer Strichman, editors, SAT 2022, volume 236 of LIPIcs, pages 30:1\u201330:24. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2022."},{"key":"1804_CR8","unstructured":"Walter Forkel, Tobias Philipp, Adrian Rebola-Pardo, and Elias Werner: Fuzzing and verifying RAT refutations with deletion information. In: Vasile Rus and Zdravko Markov, editors, FLAIRS 2017, pages 190\u2013193. AAAI Press, 2017."},{"key":"1804_CR9","doi-asserted-by":"crossref","unstructured":"Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Martin C. Cooper, Nicholas Asher, and Jo\u00e3o Marques Silva: Tractable explanations for d-dnnf classifiers. In: AAAI 2022, pages 5719\u20135728. AAAI Press, 2022.","DOI":"10.1609\/aaai.v36i5.20514"},{"key":"1804_CR10","doi-asserted-by":"crossref","unstructured":"Alexey Ignatiev: Towards trustable explainable AI. In: Christian Bessiere, editor, IJCAI 2020, pages 5154\u20135158. ijcai.org, 2020.","DOI":"10.24963\/ijcai.2020\/726"},{"key":"1804_CR11","doi-asserted-by":"crossref","unstructured":"Peter Lammich: The GRAT tool chain \u2013 efficient (UN)SAT certificate checking with formal correctness guarantees. In Serge Gaspers and Toby Walsh, editors, SAT 2017, volume 10491of LNCS, pages 457\u2013463. Springer, 2017.","DOI":"10.1007\/978-3-319-66263-3_29"},{"key":"1804_CR12","series-title":"Proceedings of the 38th Annual Design Automation Conference (DAC)","volume-title":"Engineering an efficient SAT solver","author":"MW Moskewicz","year":"2001","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference (DAC), pages 530\u2013535, Las Vegas, Nevada, USA, 2001. Association for Computing Machinery."},{"key":"1804_CR13","series-title":"Proceedings of the International Conference on Computer Aided Design (ICCAD)","volume-title":"GRASP \u2013 a new search algorithm for satisfiability","author":"JPM Silva","year":"1996","unstructured":"Jo\u00e3o P. Marques Silva and Karem A. Sakallah: GRASP \u2013 a new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer Aided Design (ICCAD), pages 220\u2013227, Washington, 1996. IEEE Computer Society."},{"key":"1804_CR14","doi-asserted-by":"crossref","unstructured":"Nathan Wetzler, Marijn Heule, and Warren A. Hunt, Jr. Drat-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, SAT 2014, volume 8561of LNCS, pages 422\u2013429. Springer, 2014.","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"1804_CR15","doi-asserted-by":"crossref","unstructured":"Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr.: Mechanical verification of SAT refutations with extended resolution. In: Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP 2013, volume 7998of LNCS, pages 229\u2013244. Springer, 2013.","DOI":"10.1007\/978-3-642-39634-2_18"}],"container-title":["Datenschutz und Datensicherheit - DuD"],"original-title":[],"language":"de","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11623-023-1804-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11623-023-1804-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11623-023-1804-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T10:13:38Z","timestamp":1695809618000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11623-023-1804-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,25]]},"references-count":15,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["1804"],"URL":"https:\/\/doi.org\/10.1007\/s11623-023-1804-y","relation":{},"ISSN":["1614-0702","1862-2607"],"issn-type":[{"value":"1614-0702","type":"print"},{"value":"1862-2607","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,25]]},"assertion":[{"value":"25 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}