{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:07:43Z","timestamp":1725487663880},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660866"},{"type":"electronic","value":"9783540487548"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48754-9_23","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:20:56Z","timestamp":1184588456000},"page":"263-277","source":"Crossref","is-referenced-by-count":1,"title":["Generating Minimal Herbrand Models Step by Step"],"prefix":"10.1007","author":[{"given":"Heribert","family":"Sch\u00fctz","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,11]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Krzysztof R. Apt, Howard A. Blair, and Adrian Walker. Towards a theory of declarative knowledge. In Jack Minker, editor, Foundations of Deductive Databases and Logic Programming, chapter 2, pages 89\u2013148. Morgan Kaufmann, 1988.","DOI":"10.1016\/B978-0-934613-40-8.50006-3"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Peter Baumgartner, Peter Fr\u00f6hlich, Ulrich Furbach, and Wolfgang Nejdl. Semantically guided theorem proving for diagnosis applications. In 15th International Joint Conference on Artificial Intelligence (IJCAI 97), Nagoya, 1997.","DOI":"10.1007\/BFb0027406"},{"key":"23_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0027406","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX\u2019 97)","author":"P. Baumgartner","year":"1997","unstructured":"Peter Baumgartner, Peter Fr\u00f6hlich, Ulrich Furbach, and Wolfgang Nejdl. Tableaux for diagnosis applications. In Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX\u2019 97), Springer LNCS 1227, pages 76\u201390, Pont-\u00e0-Mousson, Prance, May 13\u201316 1997."},{"key":"23_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop (TABLEAUX\u2019 96)","author":"F. Bry","year":"1996","unstructured":"Fran\u00e7ois Bry and Adnan H. Yahya. Minimal model generation with positive unit hyper-resolution tableaux. In Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop (TABLEAUX\u2019 96), Springer LNCS 1071, Terrasini, Palermo, Italy, May 15\u201317 1996."},{"key":"23_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/3-540-63104-6_18","volume-title":"14th International Conference on Automated Deduction (CADE-14)","author":"R. Hasegawa","year":"1997","unstructured":"Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, and Miyuki Koshimura. Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving. In 14th International Conference on Automated Deduction (CADE-14), Springer LNCS 1249, pages 176\u2013190, Townsville, North Queensland, Australia, July 13\u201317 1997."},{"issue":"2","key":"23_CR6","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00881861","volume":"14","author":"D. W. Loveland","year":"1995","unstructured":"Donald W. Loveland, David W. Reed, and Debra Sue Wilson. SATCHMORE: SATCHMO with relevancy. Journal of Automated Reasoning, 14(2):325\u2013351, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction (CADE-9)","author":"R. Manthey","year":"1988","unstructured":"Rainer Manthey and Fran\u00e7ois Bry. Satchmo: A theorem prover implemented in Prolog. In 9th International Conference on Automated Deduction (CADE-9), Springer LNCS 310, pages 415\u2013434, Argonne, Illinois, USA, 1988."},{"key":"23_CR8","unstructured":"Wolfgang Nejdl and Peter Fr\u00f6hlich. Minimal model semantics for diagnosis \u2014 techniques and first benchmarks. In 7th International Workshop on Principles of Diagnosis, Val Morin, 1996."},{"key":"23_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-61208-4_18","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop (TABLEAUX\u2019 96)","author":"I. Niemel\u00e4","year":"1996","unstructured":"Ilkka Niemel\u00e4. A tableau calculus for minimal model reasoning. In Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop (TABLEAUX\u2019 96), Springer LNCS 1071, pages 278\u2013294, Terrasini, Palermo, Italy, May 15\u201317 1996."},{"key":"23_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BFb0054270","volume-title":"15th International Conference on Automated Deduction (CADE-15)","author":"Y. Ohta","year":"1998","unstructured":"Yoshihiko Ohta, Katsumi Inoue, and Ryuzo Hasegawa. On the relationship between non-Horn magic sets and relevancy testing. In 15th International Conference on Automated Deduction (CADE-15), Springer LNCS 1421, pages 333\u2013348, Lindau, Germany, July 5\u201310 1998."},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Teodor C. Przymusinski. On the declarative semantics of deductive databases and logic programs. In Jack Minker, editor, Foundations of Deductive Databases and Logic Programming, chapter 5, pages 193\u2013216. Morgan Kaufmann, 1988.","DOI":"10.1016\/B978-0-934613-40-8.50009-9"},{"issue":"1","key":"23_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23\u201341, January 1965.","journal-title":"Journal of the ACM"},{"issue":"1","key":"23_CR13","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/S0743-1066(96)00116-1","volume":"32","author":"D. Seipel","year":"1997","unstructured":"Dietmar Seipel, Jack Minker, and Carolina Ruiz. Model generation and state generation for disjunctive logic programs. Journal of Logic Programming, 32(1):48\u201369, 1997.","journal-title":"Journal of Logic Programming"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48754-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:29:53Z","timestamp":1556666993000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48754-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660866","9783540487548"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48754-9_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}