{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:35Z","timestamp":1761611195118},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_3","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T14:36:30Z","timestamp":1167402990000},"page":"32-46","source":"Crossref","is-referenced-by-count":6,"title":["Integrating Constraint Solving into Proof Planning"],"prefix":"10.1007","author":[{"given":"Erica","family":"Melis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Zimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Aiba, A., Hasegawa, R.: Constraint Logic Programming System - CAL, GDCC and Their Constraint Solvers. In: Proc. of the Conference on Fifth Generation Computer Systems, ICOT, pp. 113\u2013131 (1992)"},{"key":"3_CR2","volume-title":"Introduction to Real Analysis","author":"R.G. Bartle","year":"1982","unstructured":"Bartle, R.G., Sherbert, D.R.: Introduction to Real Analysis. John Wiley& Sons, New York (1982)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Benzmueller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Schaarschmidt, W., Siekmann, J., Sorge, V.: OMEGA: Towards a Mathematical Assistant. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63104-6_23"},{"key":"3_CR4","unstructured":"Boyer, R.S., Moore, J.S.: Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence (Logic and the Acquisition of Knowledge)\u00a011 (1988)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310. Springer, Heidelberg (1988)","DOI":"10.1007\/BFb0012826"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert, H.-J.: A Resolution Principle for Constrained Logics. Artifcial Intelligence\u00a066(2) (1994)","DOI":"10.1016\/0004-3702(94)90027-2"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Fr\u00fchwirth, T.: Constraint Handling Rules. In: Podelski, A. (ed.) Constraint Programming: Basics and Trends. LNCS, vol.\u00a0910. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-59155-9_6"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.-L.: Constraint Logic Programming. In: Proc. 14th ACM Symposium on Principles of Programming Languages (1987)","DOI":"10.1145\/41625.41635"},{"key":"3_CR9","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0004-3702(77)90007-8","volume":"8","author":"A.K. Mackworth","year":"1977","unstructured":"Mackworth, A.K.: Consistency in Networks of Relations. Artificial Intelligence\u00a08, 99\u2013118 (1977)","journal-title":"Artificial Intelligence"},{"key":"3_CR10","unstructured":"Melis, E.: AI-Techniques in Proof Planning. In: European Conference on Artificial Intelligence. Kluwer Academic, Dordrecht (1998)"},{"key":"3_CR11","unstructured":"Melis, E.: Combining Proof Planning with Constraint Solving. In: Proceedings of Calculemus and Types 1998. Electronic Proceedings (1998), http:\/\/www.win.tue.nl\/math\/dw\/pp\/calc\/proceedings.html"},{"issue":"1","key":"3_CR12","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0004-3702(99)00076-4","volume":"115","author":"E. Melis","year":"1999","unstructured":"Melis, E., Siekmann, J.H.: Knowledge-based Proof Planning. Artificial Intelligence\u00a0115(1), 65\u2013105 (1999)","journal-title":"Artificial Intelligence"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Melis, E., Sorge, V.: Employing External Reasoners in Proof Planning. In: Armando, A., Jebelean, T. (eds.) Calculemus 1999 (1999)","DOI":"10.1016\/S1571-0661(05)80614-0"},{"key":"3_CR14","unstructured":"Mittal, S., Falkenhainer, B.: Dynamic Constraint Satisfaction Problems. In: Proceedings of the 10th National Conference on Arti ficial Intelligence, AAAI 1990, Boston, MA, pp. 25\u201332 (1990)"},{"key":"3_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/BFb0055915","volume-title":"Artificial Intelligence and Symbolic Computation","author":"E. Monfroy","year":"1998","unstructured":"Monfroy, E., Ringeissen, C.: SoleX: a Domain-Independent Scheme for Constraint Solver Extension. In: Calmet, J., Plaza, J. (eds.) AISC 1998. LNCS (LNAI), vol.\u00a01476, p. 222. Springer, Heidelberg (1998)"},{"key":"3_CR16","unstructured":"The Mozart Consortium. The Mozart Programming System, http:\/\/www.mozart-oz.org\/"},{"key":"3_CR17","volume-title":"Natural Deduction - A Proof Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction - A Proof Theoretical Study. Almquist and Wiksell, Stockholm (1965)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Smolka, G.: The Oz programming model. In: van Leeuwen, J. (ed.) Current Trends in Computer Science. Springer, Hidleberg (1995)","DOI":"10.1007\/BFb0015252"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Stickel, M.K.: Automated Deduction by Theory Resolution. In: Proc. of the 9th International Joint Conference on Artificial Intelligence (1985)","DOI":"10.1007\/BF00244275"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Stolzenburg, F.: Membership Constraints and Complexity in Logic Programming with Sets. In: Baader, F., Schulz, U. (eds.) Frontiers in Combining Systems. Kluwer Academic, Dordrecht (1996)","DOI":"10.1007\/978-94-009-0349-4_15"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:34:40Z","timestamp":1556019280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/10720084_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}