{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T22:54:09Z","timestamp":1649112849872},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["New Gener Comput"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1007\/bf03037473","type":"journal-article","created":{"date-parts":[[2009,4,24]],"date-time":"2009-04-24T03:04:57Z","timestamp":1240542297000},"page":"177-207","source":"Crossref","is-referenced-by-count":3,"title":["SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy"],"prefix":"10.1007","volume":"21","author":[{"given":"Donald W.","family":"Loveland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan H.","family":"Yahya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF03037473_CR1","doi-asserted-by":"crossref","unstructured":"Bancilhon, F., Sagiv, Y. and Ullman, J., \u201cMagic Sets and Other Strange Ways to Implement Logic Programs,\u201d inProc. of the Fifth ACM SIGMOD-SIGART Symposium on Principles of Database Systems (PODS), pp. 1\u201315, 1986.","DOI":"10.1145\/6012.15399"},{"issue":"1","key":"BF03037473_CR2","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1023\/A:1006291616338","volume":"25","author":"F. Bry","year":"2000","unstructured":"Bry, F. and Yahya, A., \u201cMinimal Model Generation with Positive Unit Hyper-Resolution tableaux,\u201dJournal of Automated Reasoning, 25, 1, pp. 35\u201382, 2000.","journal-title":"Journal of Automated Reasoning"},{"key":"BF03037473_CR3","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0169-023X(90)90017-8","volume":"5","author":"F. Bry","year":"1990","unstructured":"Bry, F., \u201cQuery Evaluation in Recursive Databases: Bottom-up and Top-down Reconciled,\u201dData and Knowledge Engineering, 5, pp. 289\u2013312, 1990.","journal-title":"Data and Knowledge Engineering"},{"key":"BF03037473_CR4","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"Chang, C. L. and Lee, K. C.,Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"BF03037473_CR5","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0304-3975(51)90010-2","volume":"78","author":"R. Demolombe","year":"1991","unstructured":"Demolombe, R., \u201cAn Efficient Strategy for Non-horn Deductive Databases,\u201dTheoretical Computer Science, 78, pp. 245\u2013259, 1991.","journal-title":"Theoretical Computer Science"},{"key":"BF03037473_CR6","doi-asserted-by":"crossref","unstructured":"Eiter, T. and Gottlob, G., \u201cComplexity Aspects of Various Semantics for Disjunctive Databases,\u201d inProc. of the Twelfth ACM SIGACT SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-93), pp. 158\u2013167, 1993.","DOI":"10.1145\/153850.153864"},{"key":"BF03037473_CR7","doi-asserted-by":"crossref","unstructured":"Hasegawa, R., Inoue, K., Ohta, Y. and Koshimura, M., \u201cNonhorn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving,\u201d inProc. of the seventeenth Conference on automated deduction (CADE097), pp. 176\u2013190, 1997.","DOI":"10.1007\/3-540-63104-6_18"},{"issue":"3","key":"BF03037473_CR8","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1023\/A:1017594402123","volume":"27","author":"L. He","year":"2001","unstructured":"He, L., \u201cI-SATCHMO: An Improvement of SATCHMO,\u201dJournal of Automated Reasoning, 27, 3, pp. 313\u2013322, 2001.","journal-title":"Journal of Automated Reasoning"},{"key":"BF03037473_CR9","unstructured":"He, L., \u201cUNSEARCHMO: Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving,\u201d inProc. of the International Joint Conference on Artificial Intelligence (IJCAI-2001), pp. 618\u2013623, 2001."},{"issue":"1","key":"BF03037473_CR10","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/BF03037320","volume":"16","author":"L. He","year":"1998","unstructured":"He, L., Chao, Y., Shimajiri, T., Seki, H. and Itoh, H., \u201cA-SATCHMORE: SATCHMORE with Availability Checking,\u201dNew Generation Computing, 16, 1, pp. 55\u201374, 1998.","journal-title":"New Generation Computing"},{"issue":"6","key":"BF03037473_CR11","first-page":"1125","volume":"15","author":"L. He","year":"2000","unstructured":"He, L., Chao, Y., Nakamura, T. and Itoh, H., \u201cAn Improvement of Theorem Prover A-SATCHMORE,\u201dJournal of the Japanese Society for Artificial Intelligence, 15, 6, pp. 1125\u20131129, 2000.","journal-title":"Journal of the Japanese Society for Artificial Intelligence"},{"key":"BF03037473_CR12","unstructured":"Johnson, C. A., \u201cTop-down Deduction in Indefinite Deductive Databases,\u201dJournees Bases de Donnees Avances, pp. 119\u2013138, 1993."},{"key":"BF03037473_CR13","doi-asserted-by":"crossref","unstructured":"Lloyd, J.,Foundations of Logic Programming (2nd Ed.), Springer Verlag, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"BF03037473_CR14","doi-asserted-by":"crossref","unstructured":"Lobo, J., Minker, J. and Rajasekar, A.,Foundations of Disjunctive Logic Programming, MIT Press, 1992.","DOI":"10.1016\/B978-0-12-450010-5.50022-0"},{"key":"BF03037473_CR15","doi-asserted-by":"crossref","unstructured":"Loveland, D. W., \u201cNear-Horn Prolog,\u201d inProc. of the 4th International Conference on Logic Programming, MIT Press, pp. 456\u2013469, 1987.","DOI":"10.21236\/ADA185172"},{"key":"BF03037473_CR16","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00881861","volume":"14","author":"D. W. Loveland","year":"1995","unstructured":"Loveland, D. W., Reed, D. and Wilson, D., \u201cSATCHMORE: SATCHMO with RElevancy,\u201dJournal of Automated Reasoning, 14, pp. 325\u2013351, July 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"BF03037473_CR17","doi-asserted-by":"crossref","unstructured":"Manthey, R. and Bry, F., \u201cSATCHMO: a Theorem Prover Implemented in Prolog,\u201d inProc. of the 9 th Conference on Automated DEduction (CADE-9), Springer Verlag, pp. 415\u2013434, 1988.","DOI":"10.1007\/BFb0012847"},{"key":"BF03037473_CR18","doi-asserted-by":"crossref","unstructured":"Ohta, Y., Inoue, K. and Hasegawa, R., \u201cOn the Relationship Between Non-Horn Magic Sets and Relevancy Testing,\u201d inProc. of the Fifteenth International Conference on Automated Deduction (CADE-15), Springer Verlag, pp. 333\u2013348, 1998.","DOI":"10.1007\/BFb0054270"},{"key":"BF03037473_CR19","unstructured":"Plaisted, D., \u201cAn Efficient Relevance Criterion for Mechanical Theorem Proving,\u201dProceedings of the First National Conference on Artificial Intelligence (AAAI-1980), pp. 79\u201383, 1980."},{"key":"BF03037473_CR20","doi-asserted-by":"crossref","unstructured":"Plaisted, D. and Yahya, A. \u201cA Relevance Restriction Strategy for Automated Deduction,\u201d inArtificial Intelligence, 144, 1\u20132, pp. 59\u201393, 2003.","DOI":"10.1016\/S0004-3702(02)00368-5"},{"key":"BF03037473_CR21","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF01530824","volume":"14","author":"A. Rajasekar","year":"1995","unstructured":"Rajasekar, A. and Yusuf, H., \u201cDwam\u2014A WAM Model Extension for Disjunctive Logic Programming,\u201dAnnals of Mathematics and Artificial Intelligence, 14, pp. 275\u2013308, 1995.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"BF03037473_CR22","unstructured":"Ramakrishnan, R. and Sudarshan, S., \u201cTop-down vs. Bottom-up Revisited,\u201d inProc. of the International Symposium on Logic Programming (ISLP\u201991), 1991."},{"key":"BF03037473_CR23","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00249019","volume":"7","author":"A. Ramsay","year":"1991","unstructured":"Ramsay, A., \u201cGenerating Relevant Models,\u201dJournal of Automated Reasoning, 7, pp. 359\u2013368, 1991.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"BF03037473_CR24","first-page":"349","volume":"13","author":"M. Stickel","year":"1994","unstructured":"Stickel, M., \u201cUpside-down Meta-Interpretation of the Model Elimination Theorem Proving Procedure for Deduction and Abduction,\u201dJournal of Automated Reasoning, 13, 3, pp. 349\u2013363, 1994.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"BF03037473_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1020109502432","volume":"28","author":"A. Yahya","year":"2002","unstructured":"Yahya, A., \u201cDuality for Goal-Driven Query Processing in Disjunctive Deductive Databases,\u201dJournal of Automated Reasoning, 28, 1, pp. 1\u201334, 2002.","journal-title":"Journal of Automated Reasoning"}],"container-title":["New Generation Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03037473.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF03037473\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03037473","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T00:52:38Z","timestamp":1558572758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF03037473"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["BF03037473"],"URL":"https:\/\/doi.org\/10.1007\/bf03037473","relation":{},"ISSN":["0288-3635","1882-7055"],"issn-type":[{"value":"0288-3635","type":"print"},{"value":"1882-7055","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}