{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:02:25Z","timestamp":1725454945883},"reference-count":54,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2015,7,1]],"date-time":"2015-07-01T00:00:00Z","timestamp":1435708800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2019,7,1]],"date-time":"2019-07-01T00:00:00Z","timestamp":1561939200000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[2015,7]]},"DOI":"10.1016\/j.artint.2015.03.004","type":"journal-article","created":{"date-parts":[[2015,4,2]],"date-time":"2015-04-02T17:16:01Z","timestamp":1427994961000},"page":"103-118","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":26,"special_numbering":"C","title":["Computer-aided proof of Erd\u0151s discrepancy properties"],"prefix":"10.1016","volume":"224","author":[{"given":"Boris","family":"Konev","sequence":"first","affiliation":[]},{"given":"Alexei","family":"Lisitsa","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/j.artint.2015.03.004_br0010","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","article-title":"Solution of the Robbins problem","volume":"19","author":"McCune","year":"1997","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.artint.2015.03.004_br0020","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","article-title":"Every map is four colourable","volume":"82","author":"Appel","year":"1976","journal-title":"Bull. Am. Math. Soc."},{"issue":"3","key":"10.1016\/j.artint.2015.03.004_br0030","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","article-title":"A proof of the Kepler conjecture","volume":"162","author":"Hales","year":"2005","journal-title":"Ann. Math."},{"issue":"1","key":"10.1016\/j.artint.2015.03.004_br0040","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10472-011-9248-8","article-title":"Automated theorem provers: a practical tool for the working mathematician?","volume":"61","author":"Bundy","year":"2011","journal-title":"Ann. Math. Artif. Intell."},{"issue":"4","key":"10.1016\/j.artint.2015.03.004_br0050","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/2591012","article-title":"Formally verified mathematics","volume":"57","author":"Avigad","year":"2014","journal-title":"Commun. ACM"},{"issue":"6","key":"10.1016\/j.artint.2015.03.004_br0060","doi-asserted-by":"crossref","first-page":"1117","DOI":"10.4153\/CJM-1989-049-4","article-title":"The nonexistence of finite projective planes of order 10","volume":"41","author":"Lam","year":"1989","journal-title":"Can. J. Math."},{"issue":"2","key":"10.1016\/j.artint.2015.03.004_br0070","doi-asserted-by":"crossref","first-page":"57","DOI":"10.2307\/2025976","article-title":"The four-color problem and its philosophical significance","volume":"6","author":"Tymoczko","year":"1979","journal-title":"J. Philos."},{"issue":"1","key":"10.1016\/j.artint.2015.03.004_br0080","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/jctb.1997.1750","article-title":"The four-colour theorem","volume":"70","author":"Robertson","year":"1997","journal-title":"J. Comb. Theory, Ser. B"},{"issue":"11","key":"10.1016\/j.artint.2015.03.004_br0090","first-page":"1382","article-title":"Formal proof\u2014the four-color theorem","volume":"55","author":"Gonthier","year":"2008","journal-title":"Not. Am. Math. Soc."},{"issue":"1","key":"10.1016\/j.artint.2015.03.004_br0100","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00454-009-9148-4","article-title":"A revision of the proof of the Kepler conjecture","volume":"44","author":"Hales","year":"2010","journal-title":"Discrete Comput. Geom."},{"key":"10.1016\/j.artint.2015.03.004_br0110","series-title":"Proceedings of the 4th International Conference on Interactive Theorem Proving","first-page":"163","article-title":"A machine-checked proof of the odd order theorem","volume":"vol. 7998","author":"Gonthier","year":"2013"},{"key":"10.1016\/j.artint.2015.03.004_br0120","series-title":"Irregularities of Distribution","author":"Beck","year":"1987"},{"key":"10.1016\/j.artint.2015.03.004_br0130","series-title":"The Discrepancy Method: Randomness and Complexity","author":"Chazelle","year":"2000"},{"key":"10.1016\/j.artint.2015.03.004_br0140","article-title":"Geometric Discrepancy: An Illustrated Guide","volume":"vol. 18","author":"Matou\u0161ek","year":"1999"},{"key":"10.1016\/j.artint.2015.03.004_br0150","series-title":"Handbook of Combinatorics, vol. 2","first-page":"1405","article-title":"Discrepancy theory","author":"Beck","year":"1995"},{"key":"10.1016\/j.artint.2015.03.004_br0160","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1016\/0166-218X(92)90121-P","article-title":"Transmitting in the n-dimensional cube","volume":"37\u201338","author":"Alon","year":"1992","journal-title":"Discrete Appl. Math."},{"key":"10.1016\/j.artint.2015.03.004_br0170","series-title":"Proceedings of the 44th Symposium on Theory of Computing","first-page":"1285","article-title":"Optimal private halfspace counting via discrepancy","author":"Muthukrishnan","year":"2012"},{"key":"10.1016\/j.artint.2015.03.004_br0180","article-title":"A Panorama of Discrepancy Theory","volume":"vol. 2107","author":"Chen","year":"2014"},{"issue":"1","key":"10.1016\/j.artint.2015.03.004_br0190","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1090\/S0894-0347-96-00175-0","article-title":"Discrepancy in arithmetic progressions","volume":"9","author":"Matou\u0161ek","year":"1996","journal-title":"J. Am. Math. Soc."},{"key":"10.1016\/j.artint.2015.03.004_br0200","doi-asserted-by":"crossref","first-page":"257","DOI":"10.4064\/aa-9-3-257-260","article-title":"Remark concerning integer sequence","volume":"9","author":"Roth","year":"1964","journal-title":"Acta Arith."},{"key":"10.1016\/j.artint.2015.03.004_br0210","series-title":"A Panorama of Discrepancy Theory","first-page":"71","article-title":"Roth's orthogonal function method in discrepancy theory and some new connections","volume":"vol. 2107","author":"Bilyk","year":"2014"},{"issue":"3","key":"10.1016\/j.artint.2015.03.004_br0220","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1307\/mmj\/1028997963","article-title":"Some unsolved problems","volume":"4","author":"Erd\u0151s","year":"1957","journal-title":"Mich. Math. J."},{"key":"10.1016\/j.artint.2015.03.004_br0230","first-page":"11","article-title":"Theory of the characters of number semigroups","volume":"20","author":"\u010cudakov","year":"1956","journal-title":"J. Indian Math. Soc."},{"key":"10.1016\/j.artint.2015.03.004_br0240","author":"Nikolov"},{"key":"10.1016\/j.artint.2015.03.004_br0250","author":"Gowers"},{"issue":"12","key":"10.1016\/j.artint.2015.03.004_br0260","doi-asserted-by":"crossref","first-page":"6279","DOI":"10.1090\/S0002-9947-2010-05235-3","article-title":"Completely multiplicative functions taking values in {1,\u22121}","volume":"362","author":"Borwein","year":"2010","journal-title":"Trans. Am. Math. Soc."},{"key":"10.1016\/j.artint.2015.03.004_br0270","series-title":"Combinatorics, Geometry and Probability: Proceedings of the Conference Dedicated to Paul Erd\u0151s on the Occasion of His 80th Birthday","article-title":"On a conjecture of Erd\u0151s and \u010cudakov","author":"Mathias","year":"1993"},{"key":"10.1016\/j.artint.2015.03.004_br0280","author":"Polymath"},{"key":"10.1016\/j.artint.2015.03.004_br0290","author":"Gowers"},{"key":"10.1016\/j.artint.2015.03.004_br0300","author":"Konev"},{"key":"10.1016\/j.artint.2015.03.004_br0310","series-title":"Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing","first-page":"219","article-title":"A SAT attack on the Erd\u0151s discrepancy conjecture","volume":"vol. 8561","author":"Konev","year":"2014"},{"key":"10.1016\/j.artint.2015.03.004_br0320","series-title":"Proceeding of the 20th International Conference on Principles and Practice of Constraint Programming","first-page":"440","article-title":"On the Erd\u0151s discrepancy problem","volume":"vol. 8656","author":"Le Bras","year":"2014"},{"key":"10.1016\/j.artint.2015.03.004_br0330","article-title":"Introduction to Analytic Number Theory","author":"Apostol","year":"1976"},{"key":"10.1016\/j.artint.2015.03.004_br0340","series-title":"A Concise Introduction to Mathematical Logic","author":"Rautenberg","year":"2010"},{"key":"10.1016\/j.artint.2015.03.004_br0350","series-title":"Handbook of Satisfiability","volume":"vol. 185","year":"2009"},{"key":"10.1016\/j.artint.2015.03.004_br0360","series-title":"Proceedings of Design, Automation and Test in Europe Conference and Exposition","first-page":"10886","article-title":"Verification of proofs of unsatisfiability for CNF formulas","author":"Goldberg","year":"2003"},{"key":"10.1016\/j.artint.2015.03.004_br0370","series-title":"Proceedings of Formal Methods in Computer-Aided Design","first-page":"181","article-title":"Trimming while checking clausal proofs","author":"Heule","year":"2013"},{"key":"10.1016\/j.artint.2015.03.004_br0380","series-title":"Handbook of Satisfiability","first-page":"695","article-title":"Pseudo-Boolean and cardinality constraints","volume":"vol. 185","author":"Roussel","year":"2009"},{"key":"10.1016\/j.artint.2015.03.004_br0390","series-title":"Principles and Practice of Constraint Programming, Proceedings of 11th International Conference","first-page":"827","article-title":"Towards an optimal CNF encoding of Boolean cardinality constraints","volume":"vol. 3709","author":"Sinz","year":"2005"},{"key":"10.1016\/j.artint.2015.03.004_br0400","series-title":"Studies in Constructive Mathematics and Mathematical Logic, Part 2","first-page":"115","article-title":"On the complexity of derivation in propositional calculus","author":"Tseitin","year":"1970"},{"key":"10.1016\/j.artint.2015.03.004_br0410","series-title":"Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning","first-page":"148","article-title":"Symmetry-breaking predicates for search problems","author":"Crawford","year":"1996"},{"issue":"2\u20133","key":"10.1016\/j.artint.2015.03.004_br0420","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/s10601-006-8059-8","article-title":"Symmetry definitions for constraint satisfaction problems","volume":"11","author":"Cohen","year":"2006","journal-title":"Constraints"},{"key":"10.1016\/j.artint.2015.03.004_br0430","series-title":"Proceedings of the 5th International Conference on Principles and Practice of Constraint Programming","first-page":"73","article-title":"Excluding symmetries in constraint-based search","volume":"vol. 1713","author":"Backofen","year":"1999"},{"key":"10.1016\/j.artint.2015.03.004_br0440","series-title":"Handbook of Constraint Programming","first-page":"329","article-title":"Symmetry in constraint programming","author":"Gent","year":"2006"},{"key":"10.1016\/j.artint.2015.03.004_br0450","series-title":"Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence","article-title":"Symmetry in solutions","author":"Heule","year":"2010"},{"issue":"3","key":"10.1016\/j.artint.2015.03.004_br0460","doi-asserted-by":"crossref","first-page":"P16","DOI":"10.37236\/2611","article-title":"Symmetry in gardens of eden","volume":"20","author":"Hartman","year":"2013","journal-title":"Electron. J. Comb."},{"key":"10.1016\/j.artint.2015.03.004_br0470","series-title":"Proceedings of the 10th International Conference on Principles and Practice of Constraint Programming","first-page":"274","article-title":"Streamlined constraint reasoning","volume":"vol. 3258","author":"Gomes","year":"2004"},{"key":"10.1016\/j.artint.2015.03.004_br0480","series-title":"Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing","first-page":"143","article-title":"Resolution tunnels for improved SAT solver performance","volume":"vol. 3569","author":"Kouril","year":"2005"},{"key":"10.1016\/j.artint.2015.03.004_br0490","series-title":"Proceedings of SAT Competition 2013","first-page":"51","article-title":"Lingeling, plingeling and treengeling entering the SAT competition 2013","author":"Biere","year":"2013"},{"key":"10.1016\/j.artint.2015.03.004_br0500","series-title":"Proceedings of SAT Competition 2013","year":"2013"},{"key":"10.1016\/j.artint.2015.03.004_br0510","series-title":"Proceedings of SAT Competition 2013","first-page":"42","article-title":"Glucose 2.3 in the SAT 2013 competition","author":"Audemard","year":"2013"},{"key":"10.1016\/j.artint.2015.03.004_br0520","series-title":"Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing","first-page":"502","article-title":"An extensible sat-solver","volume":"vol. 2919","author":"E\u00e9n","year":"2003"},{"issue":"3","key":"10.1016\/j.artint.2015.03.004_br0530","doi-asserted-by":"crossref","first-page":"448","DOI":"10.2307\/1990319","article-title":"On highly composite and similar numbers","volume":"56","author":"Alaoglu","year":"1944","journal-title":"Trans. Am. Math. Soc."},{"key":"10.1016\/j.artint.2015.03.004_br0540","author":"Polymath"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370215000429?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370215000429?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T07:10:20Z","timestamp":1598857820000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0004370215000429"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7]]},"references-count":54,"alternative-id":["S0004370215000429"],"URL":"https:\/\/doi.org\/10.1016\/j.artint.2015.03.004","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[2015,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Computer-aided proof of Erd\u0151s discrepancy properties","name":"articletitle","label":"Article Title"},{"value":"Artificial Intelligence","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.artint.2015.03.004","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2015 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}