{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,7]],"date-time":"2024-12-07T05:04:31Z","timestamp":1733547871833,"version":"3.30.1"},"reference-count":47,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4915,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2000,2]]},"DOI":"10.1016\/s0304-3975(99)00170-x","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T00:48:18Z","timestamp":1027644498000},"page":"55-90","source":"Crossref","is-referenced-by-count":6,"title":["Search algorithms in type theory"],"prefix":"10.1016","volume":"232","author":[{"given":"James L","family":"Caldwell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian P","family":"Gent","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Judith","family":"Underwood","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(99)00170-X_BIB1","unstructured":"A.B. Baker, Intelligent backtracking on constraint satisfaction problems: experimental and theoretical results, Technical Report CIS-TR-95-08, Computer and Information Sciences, University of Oregon, 1995."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB2","unstructured":"F. Barbanera, S. Berardi, Witness extraction in classical logic through normalization, in: G. Huet, G. Plotkin (Eds.), Logical Environments, Cambridge University Press, Cambridge, 1993."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB3","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0025","article-title":"A symmetric lambda calculus for classical program extraction","volume":"125","author":"Barbanera","year":"1996","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB4","doi-asserted-by":"crossref","unstructured":"R.J. Bayardo Jr., R.C. Schrag, Using CSP look-back techniques to solve exceptionally hard SAT instances, in: E.C. Freuder (Ed.), Principles and Practice of Constraint Programming \u2013 CP96, Springer, Berlin, 1996, pp. 46\u201360.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB5","unstructured":"R.J. Bayardo Jr., R.C. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proceedings of the Fourteenth National Conference on Artificial Intelligence, AAAI Press, Menlo Park, CA, 1997, pp. 203\u2013208."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB6","doi-asserted-by":"crossref","unstructured":"U. Berger, H. Schwichtenberg, Program extraction from classical proofs, in: D. Leivant (Ed.), Logic and Computational Complexity, Springer, Berlin, 1994, pp. 77\u201397.","DOI":"10.1007\/3-540-60178-3_80"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB7","unstructured":"M.B. Burstein, D.R. Smith, Itas: a portable interactive transportation scheduling tool using a search engine generated from formal specifications, in: Proceedings of the Third International Conference on Artificial Intelligence Planning Systems (AIPS-96), Edinburgh, Scotland, 1996."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB8","doi-asserted-by":"crossref","unstructured":"J.L. Caldwell, Moving proofs-as-programs into practice, in: Proceedings of the 12th IEEE International Conference on Automated Software Engineering, IEEE Computer Society, Silver Spring, MD, 1997.","DOI":"10.1109\/ASE.1997.632819"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB9","doi-asserted-by":"crossref","unstructured":"J.L. Caldwell, Classical propositional decidability via Nuprl proof extraction, in: J. Grundy, M. Newey (Eds.), TPHOLs\u201998 The 11th International Conference on Theorem Proving in Higher Order Logics, Springer, Berlin, 1998, pp. 105\u2013122.","DOI":"10.1007\/BFb0055132"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB10","unstructured":"J.L. Caldwell, Decidability extracted: extracting tableau procedures for classical and intuitionistic propositional logic from formal proofs, Ph.D. Thesis, Cornell University, 1998, to appear."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB11","unstructured":"P. Cheeseman, B. Kanefsky, W.M. Taylor, Where the really hard problems are, in: J. Mylopoulos, R. Reiter (Eds.), Proceedings of the Twelfth International Conference on Artificial Intelligence, Morgan Kauffman, San Mateo, CA, 1991, pp. 331\u2013337."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB12","doi-asserted-by":"crossref","unstructured":"W. Clinger, J. Rees, The revised4 report on the algorithmic language scheme, ACM LISP Pointers 4(3) (1991).","DOI":"10.1145\/1317265.1317268"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB13","unstructured":"R.L. Constable, D.J. Howe, Implementing metamathematics as an approach to automatic theorem proving, in: R.B. Banerji (Ed.), Formal Techniques in Artificial Intelligence: A Source Book, Elsevier Science Publishers, North-Holland, 1990, pp. 45\u201376."},{"year":"1986","series-title":"Implementing Mathematics with The Nuprl Development System","author":"Constable","key":"10.1016\/S0304-3975(99)00170-X_BIB14"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB15","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1998","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB16","doi-asserted-by":"crossref","unstructured":"O. Danvy, A. Filinski, Abstracting Control, in: Lisp and Functional Programming, ACM Press, New York, 1990, pp. 151\u2013160.","DOI":"10.1145\/91556.91622"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB17","doi-asserted-by":"crossref","unstructured":"R.K. Dybvig, R. Hieb, Continuations and concurrency, in: Proceedings of the Second ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 1990, pp. 128\u2013136. Also Indiana University Computer Science Department Technical Report #256.","DOI":"10.1145\/99163.99178"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB18","doi-asserted-by":"crossref","unstructured":"D.P. Friedman, C.T. Haynes, E.E. Kohlbecker, Programming with Continuations, in: P. Pepper (Ed.), Program Transformation and Programming Environments, Springer, Berlin, 1984, pp. 263\u2013274.","DOI":"10.1007\/978-3-642-46490-4_23"},{"year":"1979","series-title":"Computers and intractability: a guide to the theory of NP-completeness","author":"Garey","key":"10.1016\/S0304-3975(99)00170-X_BIB19"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB20","unstructured":"J. Gaschnig, Performance measurement and analysis of certain search algorithms, Technical Report CMU-CS-79-124, Carnegie-Mellon University, 1979."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB21","doi-asserted-by":"crossref","unstructured":"I.P. Gent, J. Underwood, The logic of search algorithms: Theory and applications, in: G. Smolka (Ed.), Principles and Practice of Constraint Programming \u2013 CP97, Springer, Berlin, 1997, pp. 77\u201391.","DOI":"10.1007\/BFb0017431"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB22","first-page":"1993","volume":"J. Artificia Intelligence Res.","author":"Ginsberg","journal-title":"Dynamic backtracking"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB23","unstructured":"S.A. Grant, B.M. Smith, The phase transition behaviour of maintaining arc consistency, in: W. Wahlster (Ed.), Proceedings of the 12th European Conference on Artificial Intelligence, Wiley, Chichester, 1996, pp. 175\u2013179."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB24","doi-asserted-by":"crossref","unstructured":"T. Griffin, A formulas-as-types notion of control, in: Proceedings of the Seventeeth Annual Symposium on Principles of Programming Languages, Association for Computing Machinery, New York, 1990, pp. 47\u201358.","DOI":"10.1145\/96709.96714"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB25","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0004-3702(80)90051-X","article-title":"Increasing tree search efficiency for constraint satisfaction problems","volume":"14","author":"Haralick","year":"1980","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB26","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1017\/S095679680000085X","article-title":"Typing first-class continuations in ML","volume":"3","author":"Harper","year":"1993","journal-title":"J. Functional Programming"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB27","doi-asserted-by":"crossref","unstructured":"D.J. Howe, Reasoning about functional programs in Nuprl, in: P.F. Lauer (Ed.), Functional Programming, Concurrency, Simulation and Automated Reasoning, Springer, Berlin, 1993, pp. 145\u2013164.","DOI":"10.1007\/3-540-56883-2_9"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB28","unstructured":"Paul Jackson, The Nuprl proof developemnt system, version 4.2 reference manual and user's guide, Computer Science Department, Cornell University, Ithaca, N.Y. Manuscript available at http:\/\/www.cs.cornell.edu\/Info\/Projects\/NuPrl\/July 1995."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB29","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1016\/S0004-3702(96)00027-6","article-title":"A theoretical evaluation of selected backtracking algorithms","volume":"89","author":"Kondrak","year":"1997","journal-title":"Artificial Intelligence"},{"year":"1994","series-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Luo","key":"10.1016\/S0304-3975(99)00170-X_BIB30"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB31","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/356022.356030","article-title":"An enumerative algorithm for finding Hamiltonian circuits in a directed graph","volume":"9","author":"Martello","year":"1983","journal-title":"ACM Trans. Math. Software"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB32","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f, Constructive mathematics and computer programming, in: Sixth International Congress for Logic, Methodology, and Philosophy of Science, North-Holland, Amsterdam, 1982, pp. 153\u2013175.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB33","doi-asserted-by":"crossref","unstructured":"C.R. Murthy, Extracting Constructive Content from Classical Proofs, Ph.D. Thesis, Cornell University, 1990. Also Department of Computer, Science, Technical Report TR90-1151.","DOI":"10.1109\/LICS.1990.113752"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB34","doi-asserted-by":"crossref","unstructured":"C.R. Murthy, An evaluation semantics for classical proofs, in: Proceedings 6th Annual IEEE Symp. on Logic in Computer Science, IEEE, Los Alamitos, CA, 1991, pp. 96\u2013107.","DOI":"10.1109\/LICS.1991.151634"},{"year":"1992","series-title":"Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp, Morgan Kauffman","author":"Norvig","key":"10.1016\/S0304-3975(99)00170-X_BIB35"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB36","doi-asserted-by":"crossref","unstructured":"M. Parigot, \u03bb\u03bc-Calculus: an Algorithmic Interpretation of classical natural deduction, in: A. Voronkov (Ed.), Proceedings International Conference on Logic Programming and Automated Reasoning, LPAR\u201992, Springer, Berlin, 1992, pp. 190\u2013201.","DOI":"10.1007\/BFb0013061"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB37","unstructured":"P. Pepper, D.R. Smith, A high-level derivation of global search algorithms (with constraint propagation), Science of Computer Programming, Special Issue on FMTA(Formal Methods: Theory and Applications, 1996."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB38","unstructured":"R. Pollack, The theory of Lego, Ph.D. Thesis, University of Edinburgh, 1995. Available as Report ECS-LFCS-95-323."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB39","unstructured":"P. Prosser, Distributed Asynchronous Scheduling, Ph.D. Thesis, Strathclyde University, 1990."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB40","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","article-title":"Hybrid algorithms for the constraint satisfaction problem","volume":"9","author":"Prosser","year":"1993","journal-title":"Comput. Intelligence"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB41","doi-asserted-by":"crossref","unstructured":"J.-F. Puget, Applications of constraint programming, in: U. Montanari, F. Rossi (Eds.), Principles and Practice of Constraint Programming \u2013 CP95, Springer, Berlin, 1995, pp. 647\u2013650.","DOI":"10.1007\/3-540-60299-2_43"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB42","doi-asserted-by":"crossref","unstructured":"D. Sabin, E.C. Freuder, Contradicting conventional wisdom in constraint satisfaction, in: Proceedings of ECAI-94, Wiley, Chichester, 1994, pp. 125\u2013129.","DOI":"10.1007\/3-540-58601-6_86"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB43","unstructured":"B.M. Smith, S.A. Grant, Sparse constraint graphs and exceptionally hard problems, in: C.S. Mellish (Ed.), Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, Morgan Kauffman, San Mateo, CA, 1995, pp. 646\u2013651."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB44","unstructured":"D.R. Smith, E.A. Parra, S.J. Westfold, Synthesis of planning and scheduling software, in: A. Tate (Ed.), Advanced Planning Technology, AAAI Press, Menlo Park, CA, 1996."},{"year":"1968","series-title":"First Order Logic","author":"Smullyan","key":"10.1016\/S0304-3975(99)00170-X_BIB45"},{"key":"10.1016\/S0304-3975(99)00170-X_BIB46","unstructured":"J.L. Underwood, The tableau algorithm for intuitionistic propositional calculus as a constructive completeness proof, in: Proceedings of the Workshop on Theorem Proving with Analytic Tableaux, Marseille, France, 1993, pp. 245\u2013248. Available as Technical Report MPI-I-93-213 Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany."},{"key":"10.1016\/S0304-3975(99)00170-X_BIB47","unstructured":"J.L. Underwood, Aspects of the computational content of proofs, Ph.D. Thesis, Cornell University, 1994. Also Department of Computer Science Technical Report TR94-1460."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439759900170X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439759900170X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,6]],"date-time":"2024-12-06T05:52:51Z","timestamp":1733464371000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S030439759900170X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,2]]},"references-count":47,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,2]]}},"alternative-id":["S030439759900170X"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00170-x","relation":{},"ISSN":["0304-3975"],"issn-type":[{"type":"print","value":"0304-3975"}],"subject":[],"published":{"date-parts":[[2000,2]]}}}