{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T23:28:32Z","timestamp":1775258912899,"version":"3.50.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,10,27]],"date-time":"2018-10-27T00:00:00Z","timestamp":1540598400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100008394","name":"Natur og Univers, Det Frie Forskningsr\u00e5d","doi-asserted-by":"crossref","award":["DFF-7014-00041"],"award-info":[{"award-number":["DFF-7014-00041"]}],"id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.1007\/s10817-018-9490-4","type":"journal-article","created":{"date-parts":[[2018,10,27]],"date-time":"2018-10-27T11:54:13Z","timestamp":1540641253000},"page":"695-722","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formally Verifying the Solution to the Boolean Pythagorean Triples Problem"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7866-7484","authenticated-orcid":false,"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,27]]},"reference":[{"key":"9490_CR1","unstructured":"Anand, A., Appel, A.W., Morrisett, G., Paraskevopoulou, Z., Pollack, R., B\u00e9langer, O.S., Sozeau, M., Weaver, M.: CertiCoq: a verified compiler for Coq. In: CoqPL Workshop (2017)"},{"key":"9490_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"9490_CR3","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21, 827\u2013859 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9490_CR4","first-page":"151","volume-title":"STOC","author":"SA Cook","year":"1971","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) STOC, pp. 151\u2013158. ACM, New York (1971)"},{"key":"9490_CR5","unstructured":"Cooper, J., Overstreet, R.: Coloring so that no pythagorean triple is monochromatic. CoRR arXiv:1505.02222 (2015)"},{"issue":"2\/3","key":"9490_CR6","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.P.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"9490_CR7","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Jr., W.A.H., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de\u00a0Moura [14], pp. 220\u2013236","DOI":"10.1007\/978-3-319-63046-5_14"},{"issue":"4","key":"9490_CR8","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s10817-017-9405-9","volume":"59","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Larsen, K.S., Schneider-Kamp, P.: Formally proving size optimality of sorting networks. J. Autom. Reason. 59(4), 425\u2013454 (2017)","journal-title":"J. Autom. Reason."},{"key":"9490_CR9","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: TACAS, LNCS, vol. 10205. Springer (2017)","DOI":"10.1007\/978-3-662-54577-5_7"},{"key":"9490_CR10","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Formally verifying the Boolean pythagorean triples conjecture. In: Eiter and Sands [15], pp. 509\u2013522","DOI":"10.29007\/jvdj"},{"key":"9490_CR11","first-page":"66","volume-title":"TPHOLs, LNCS","author":"L Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Wiedijk, F.: Hierarchical reflection. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs, LNCS, vol. 3223, pp. 66\u201381. Springer, Heidelberg (2004)"},{"key":"9490_CR12","doi-asserted-by":"crossref","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: ICTAC, LNCS, vol. 6255, pp. 260\u2013274. Springer (2010)","DOI":"10.1007\/978-3-642-14808-8_18"},{"key":"9490_CR13","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"9490_CR14","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L. (ed.): Automated Deduction\u2014CADE 26\u201426th International Conference on Automated Deduction, Gothenburg, Sweden, August 6\u201311, 2017, Proceedings, LNCS, vol. 10395. Springer (2017)","DOI":"10.1007\/978-3-319-63046-5"},{"key":"9490_CR15","unstructured":"Eiter, T., Sands, D. (eds.): LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7\u201312th May 2017, EPiC Series, vol.\u00a046. EasyChair (2017)"},{"key":"9490_CR16","first-page":"345","volume-title":"SAS, LNCS","author":"A Fouilh\u00e9","year":"2013","unstructured":"Fouilh\u00e9, A., Monniaux, D., P\u00e9rin, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS, LNCS, vol. 7935, pp. 345\u2013365. Springer, Heidelberg (2013)"},{"key":"9490_CR17","doi-asserted-by":"crossref","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10,886\u201310,891 (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"9490_CR18","first-page":"228","volume-title":"SAT, LNCS","author":"M Heule","year":"2016","unstructured":"Heule, M., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT, LNCS, vol. 9710, pp. 228\u2013245. Springer, Heidelberg (2016)"},{"key":"9490_CR19","first-page":"50","volume-title":"HVC, LNCS","author":"M Heule","year":"2012","unstructured":"Heule, M., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC, LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012)"},{"key":"9490_CR20","first-page":"129","volume-title":"TACAS, LNCS","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS, LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"9490_CR21","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of erd\u0151s discrepancy properties. Artif. Intell. 224, 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"key":"9490_CR22","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de\u00a0Moura [14], pp. 237\u2013254","DOI":"10.1007\/978-3-319-63046-5_15"},{"key":"9490_CR23","doi-asserted-by":"crossref","unstructured":"Landman, B.M., Robertson, A.: Ramsey Theory on the Integers. The Student Mathematical Library, vol.\u00a024. AMS (2004)","DOI":"10.1090\/stml\/024"},{"issue":"7","key":"9490_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9490_CR25","first-page":"359","volume-title":"CiE 2008, LNCS","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008, LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"key":"9490_CR26","unstructured":"Mijnders, S., de\u00a0Wilde, B., Heule, M.: Symbiosis of search and heuristics for random 3-SAT. In: Mitchell, D.G., Ternovska, E. (eds.) Proceedings of LaSh 2010 (2010)"},{"key":"9490_CR27","doi-asserted-by":"crossref","unstructured":"Philipp, T., Rebola-Pardo, A.: Towards a semantics of unsatisfiability proofs with inprocessing. In: Eiter and Sands [15], pp. 65\u201384","DOI":"10.29007\/7jgq"},{"key":"9490_CR28","doi-asserted-by":"crossref","unstructured":"Rebola-Pardo, A., Biere, A.: Two flavours of DRAT. In: Pragmatics of SAT 2018 (2018)","DOI":"10.29007\/nnqs"},{"key":"9490_CR29","unstructured":"Silva, J.P.M., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: ICTAI, pp. 467\u2013469. IEEE Computer Society (1996)"},{"key":"9490_CR30","doi-asserted-by":"crossref","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: C.\u00a0Benzm\u00fcller, B.W. Paleo (eds.) UITP, EPTCS, vol. 167, pp. 61\u201372 (2014)","DOI":"10.4204\/EPTCS.167.8"},{"key":"9490_CR31","first-page":"229","volume-title":"ITP, LNCS","author":"ND Wetzler","year":"2013","unstructured":"Wetzler, N.D., Heule, M.J., Hunt Jr., W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP, LNCS, vol. 7998, pp. 229\u2013244. Springer, Heidelberg (2013)"},{"key":"9490_CR32","doi-asserted-by":"crossref","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS, vol. 3600. Springer (2006)","DOI":"10.1007\/11542384"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9490-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9490-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9490-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T22:07:32Z","timestamp":1775254052000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9490-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,27]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["9490"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9490-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,27]]},"assertion":[{"value":"8 September 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 October 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 October 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}