{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T04:58:53Z","timestamp":1648529933885},"reference-count":31,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2001,5,1]],"date-time":"2001-05-01T00:00:00Z","timestamp":988675200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Applied Mathematics and Computation"],"published-print":{"date-parts":[[2001,5]]},"DOI":"10.1016\/s0096-3003(99)00249-0","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T18:08:01Z","timestamp":1027620481000},"page":"175-194","source":"Crossref","is-referenced-by-count":0,"title":["The application of automated reasoning to formal models of combinatorial optimization"],"prefix":"10.1016","volume":"120","author":[{"given":"Paul","family":"Helman","sequence":"first","affiliation":[]},{"given":"Robert","family":"Veroff","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0096-3003(99)00249-0_BIB1","series-title":"Applied Dynamic Programming","author":"Bellman","year":"1962"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB2","series-title":"A Computational Logic","author":"Boyer","year":"1979"},{"issue":"3","key":"10.1016\/S0096-3003(99)00249-0_BIB3","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","article-title":"Set theory in first-order logic: clauses for G\u00f6del's axioms","volume":"2","author":"Boyer","year":"1986","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB4","unstructured":"R. Boyer, J. Moore, Mechanized formal reasoning about programs and computing machines, in: R. Veroff (Ed.), Automated Reasoning and Its Applications, MIT Press, Cambridge, 1997, pp. 147\u2013176"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB5","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB6","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/BF01584082","article-title":"Matroids and the greedy algorithm","volume":"1","author":"Edmonds","year":"1971","journal-title":"Math. Programm."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB7","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0022-247X(86)90147-2","article-title":"The principle of optimality in the design of efficient algorithms","volume":"119","author":"Helman","year":"1986","journal-title":"J. Math. Anal. Appl."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB8","doi-asserted-by":"crossref","unstructured":"P. Helman, An algebra for search problems and their solutions, in: L. Kanal, V. Kumar (Eds.), Search in Artificial Intelligence, Springer Series on Symbolic Computation, Springer, New York, 1988, pp. 28\u201390","DOI":"10.1007\/978-1-4613-8788-6_2"},{"issue":"1","key":"10.1016\/S0096-3003(99)00249-0_BIB9","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/58562.59304","article-title":"A common schema for dynamic programming and branch and bound algorithms","volume":"36","author":"Helman","year":"1989","journal-title":"J. ACM"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB10","unstructured":"P. Helman, A theory of greedy structures based on K-ary dominance relations, Technical Report CS89-11, University of New Mexico, Department of Computer Science, Albuquerque, NM, 1989"},{"issue":"2","key":"10.1016\/S0096-3003(99)00249-0_BIB11","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1137\/0406021","article-title":"An exact characterization of greedy structures","volume":"6","author":"Helman","year":"1993","journal-title":"SIAM J. Discrete Math."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB12","unstructured":"P. Helman, R. Veroff, Automated proofs of some results in combinatorial optimization, Technical Report, University of New Mexico, Department of Computer Science, Albuquerque, NM, to appear"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB13","doi-asserted-by":"crossref","first-page":"642","DOI":"10.1016\/0022-247X(73)90283-7","article-title":"Solvable classes of discrete dynamic programming","volume":"43","author":"Ibaraki","year":"1973","journal-title":"J. Math. Anal. Appl."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB14","doi-asserted-by":"crossref","first-page":"618","DOI":"10.1016\/0022-247X(76)90096-2","article-title":"On the optimality of algorithms for finite state sequential decision processes","volume":"53","author":"Ibaraki","year":"1976","journal-title":"J. Math. Anal. Appl."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB15","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1145\/322003.322010","article-title":"The power of dominance relations in branch and bound algorithms","volume":"24","author":"Ibaraki","year":"1977","journal-title":"J. ACM"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0019-9958(78)90197-3","article-title":"Branch-and-bound procedure and state-space representation of combinatorial optimization problems","volume":"36","author":"Ibaraki","year":"1978","journal-title":"Inform. Control"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB17","doi-asserted-by":"crossref","first-page":"693","DOI":"10.1137\/0115060","article-title":"Finite-state processes and dynamic programming","volume":"15","author":"Karp","year":"1967","journal-title":"SIAM J. Appl. Math."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB18","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1137\/0605024","article-title":"Greedoids linear objective functions","volume":"5","author":"Korte","year":"1984","journal-title":"SIAM J. Algebra Discrete Meth."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB19","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0004-3702(83)80009-5","article-title":"A general branch and bound formulation for understanding and synthesizing and\/or tree search procedures","volume":"21","author":"Kumar","year":"1983","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","article-title":"Complexity and related enhancements for automated theorem-proving programs","volume":"2","author":"McCharen","year":"1976","journal-title":"Comput. Math. Appl."},{"key":"10.1016\/S0096-3003(99)00249-0_BIB21","doi-asserted-by":"crossref","unstructured":"W. McCune, OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, IL, 1994","DOI":"10.2172\/10129052"},{"issue":"3","key":"10.1016\/S0096-3003(99)00249-0_BIB22","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. Automated Reasoning"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB23","unstructured":"G. Robinson, L. Wos, Paramodulation and theorem-proving in first-order theories with equality, in: B. Meltzer, D. Michie (Eds.), Machine Intelligence 4, Edinburgh University Press, 1969, pp. 135\u2013150"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB24","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"Int. J. Comput. Math."},{"issue":"1","key":"10.1016\/S0096-3003(99)00249-0_BIB25","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"issue":"2","key":"10.1016\/S0096-3003(99)00249-0_BIB26","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00244283","article-title":"The linked inference principle I: the formal treatment","volume":"8","author":"Veroff","year":"1992","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"10.1016\/S0096-3003(99)00249-0_BIB27","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF00252178","article-title":"Using hints to increase the effectiveness of an automated reasoning program: case studies","volume":"16","author":"Veroff","year":"1996","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB28","unstructured":"R. Veroff, Reasoning at multiple levels of abstraction, to appear"},{"issue":"4","key":"10.1016\/S0096-3003(99)00249-0_BIB29","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","article-title":"Efficiency and completeness of the set of support strategy in theorem proving","volume":"12","author":"Wos","year":"1965","journal-title":"J. ACM"},{"issue":"4","key":"10.1016\/S0096-3003(99)00249-0_BIB30","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","article-title":"The concept of demodulation in theorem proving","volume":"14","author":"Wos","year":"1967","journal-title":"J. ACM"},{"key":"10.1016\/S0096-3003(99)00249-0_BIB31","doi-asserted-by":"crossref","unstructured":"L. Wos, R. Veroff, B. Smith, The linked inference principle, II: the user's viewpoint, in: W. McCune, R. Shostak (Eds.), Proceedings of the Seventh International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 170, Springer, New York, 1984, pp. 316\u2013332","DOI":"10.1007\/978-0-387-34768-4_19"}],"container-title":["Applied Mathematics and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0096300399002490?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0096300399002490?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,14]],"date-time":"2020-01-14T19:27:06Z","timestamp":1579030026000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0096300399002490"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,5]]},"references-count":31,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2001,5]]}},"alternative-id":["S0096300399002490"],"URL":"https:\/\/doi.org\/10.1016\/s0096-3003(99)00249-0","relation":{},"ISSN":["0096-3003"],"issn-type":[{"value":"0096-3003","type":"print"}],"subject":[],"published":{"date-parts":[[2001,5]]}}}