{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:08Z","timestamp":1776333428172,"version":"3.51.2"},"publisher-location":"Berlin\/Heidelberg","reference-count":15,"publisher":"Springer-Verlag","isbn-type":[{"value":"354019343X","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012847","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"415-434","source":"Crossref","is-referenced-by-count":143,"title":["SATCHMO: A theorem prover implemented in Prolog"],"prefix":"10.1007","author":[{"given":"Rainer","family":"Manthey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Bry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Bry, F. et. al., A Uniform Approach to Constraint Satisfaction and Constraint Satisfiability in Deductive Databases, ECRC Techn. Rep. KB-16, 1987 (to appear in Proc. Int. Conf. Extending Database Technology EDBT 88)","DOI":"10.1007\/3-540-19074-0_69"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Butler, R. et al., Paths to High-Performance Automated Theorem Proving, Proc. 8th CADE 1986, Oxford, 1986, 588\u2013597","DOI":"10.1007\/3-540-16780-3_123"},{"key":"28_CR3","first-page":"103","volume":"1","author":"E. Lusk","year":"1985","unstructured":"Lusk, E. and Overbeek, R., Non-Horn problems, Journal of Automated Reasoning 1 (1985), 103\u2013114","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Manthey, R. and Bry, F., A hyperresolution-based proof procedure and its implementation in PROLOG, Proc. of GWAI-87 (11th German Workshop on Artificial Intelligence), Geseke, 1987, 221\u2013230","DOI":"10.1007\/978-3-642-73005-4_24"},{"key":"28_CR5","unstructured":"McCune, B., A Proof of a Non-Obvious Theorem, AAR Newsletter No. 7, 1986, 5"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Nicolas, J.M., Logic for improving integrity checking in relational databases, Tech. Rep., ONERA-CERT, Toulouse, Feb. 1979 (also in Acta Informatica 18, 3, Dec. 1982)","DOI":"10.1007\/BF00263192"},{"key":"28_CR7","first-page":"327","volume":"1","author":"H.J. Ohlbach","year":"1985","unstructured":"Ohlbach, H.J. and Schmidt-Schauss, M., The Lion and the Unicorn, J. of Automated Reasoning 1 (1985), 327\u2013332","journal-title":"J. of Automated Reasoning"},{"key":"28_CR8","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"Pelletier, F.J., Seventy-five Problems for Testing Automatic Theorem Provers, J. of Automated Reasoning 2 (1986), 191\u2013216","journal-title":"J. of Automated Reasoning"},{"key":"28_CR9","unstructured":"Pelletier, F.J. and Rudnicki, P., Non-Obviousness, AAR Newsletter No. 6, 1986, 4\u20135"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Smullyan, R., First-Order Logic, Springer-Verlag, 1968","DOI":"10.1007\/978-3-642-86718-7"},{"key":"28_CR11","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF03037328","volume":"2","author":"M. Stickel","year":"1984","unstructured":"Stickel, M., A Prolog Technology Theorem Prover, New Generation Computing 2, (1984), 371\u2013383","journal-title":"New Generation Computing"},{"key":"28_CR12","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"M. Stickel","year":"1986","unstructured":"Stickel, M., Schubert's steamroller problem: formulations and solutions, J. of Automated Reasoning 2 (1986), 89\u2013101","journal-title":"J. of Automated Reasoning"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Walther, C., A mechanical solution of Schubert's steamroller by many-sorted resolution, Proc. of AAAI-84, Austin, Texas, 1984, 330\u2013334 (Revised version in Artificial Intelligence, 26, 1985, 217\u2013224)","DOI":"10.1016\/0004-3702(85)90029-3"},{"key":"28_CR14","unstructured":"Walther, C., An Obvious Solution for a Non-Obvious Problem, AAR Newsletter No. 9, Jan. 1988, 4\u20135"},{"key":"28_CR15","unstructured":"Wos, L. et. al., Automated Reasoning, Prentice Hall, 1984"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012847","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:24:06Z","timestamp":1586579046000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012847"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0012847","relation":{},"subject":[]}}