{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:29Z","timestamp":1749124049442},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/bf00881955","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:38:56Z","timestamp":1104133136000},"page":"189-210","source":"Crossref","is-referenced-by-count":23,"title":["Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction"],"prefix":"10.1007","volume":"13","author":[{"given":"Mark E.","family":"Stickel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","volume-title":"Investigations in model elimination based theorem proving","author":"O. L. Astrachan","year":"1992","unstructured":"Astrachan, O. L., ?Investigations in model elimination based theorem proving?, Ph.D. dissertation, Department of Computer Science, Duke University, Durham, North Carolina (1992)."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Stickel, M. E., ?Caching and lemmaizing in model elimination theorem provers?,Proceedings of the 11th International Conference on Automated Deduction, Sarasota Springs, N.Y. (June 1992).","DOI":"10.1007\/3-540-55602-8_168"},{"key":"CR3","series-title":"Technical Report","volume-title":"Magic set computation for stratified databases","author":"I. Balbin","year":"1987","unstructured":"Balbin, I., Port, G. S. and Ramamohanarao, K., ?Magic set computation for stratified databases?,Technical Report 87\/11, Department of Computer Science, University of Melbourne, Melbourne, Australia (1987)."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Bancilhon, F., Maier, D., Sagiv, Y. and Ullman, J., ?Magic sets and other strange ways to implement logic programs?,Proceedings of the Fifth ACM Symposium on Principles of Database Systems, pp. 53?56 (1986).","DOI":"10.1145\/6012.15399"},{"key":"CR5","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D., ?Proving theorems with the modification method?,SIAM J. Computing 4, 412?430 (1975).","journal-title":"SIAM J. Computing"},{"key":"CR6","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., ?Query evaluation in recursive databases: Bottom-up and top-down reconciled?,Data & Knowledge Engineering 5, 289?312 (1990).","journal-title":"Data & Knowledge Engineering"},{"key":"CR7","unstructured":"Charniak, E. and Husain, S., ?A new admissable heuristic for minimal-cost proofs?,Proceedings of the AAAI-91 National Conference on Artificial Intelligence, Anaheim, California (July 1991)."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Charniak, E. and Goldman, R., ?A logic for semantic interpretation?,Proceedings of the 26th Annual Meeting of the Association for Computational Linguistics, Buffalo, New York, pp. 87?94 (June 1988).","DOI":"10.3115\/982023.982034"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Cox, P. T. and Pietrzykowski, T., ?Causes for events: their computation and applications?,Proceedings of the 8th Conference on Automated Deduction, Oxford, England, pp. 608?621 (July 1986).","DOI":"10.1007\/3-540-16780-3_125"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0004-3702(86)90080-9","volume":"28","author":"J. deKleer","year":"1986","unstructured":"deKleer, J., ?An assumption-based TMS?,Artificial Intelligence 28, 127?162 (1986).","journal-title":"Artificial Intelligence"},{"key":"CR11","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/0004-3702(86)90081-0","volume":"28","author":"J. deKleer","year":"1986","unstructured":"deKleer, J., ?Extending the ATMS?,Artificial Intelligence 28, 163?196 (1986).","journal-title":"Artificial Intelligence"},{"key":"CR12","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., ?An efficient strategy for non-Horn deductive databases?,Theoretical Computer Science 78, 245?259 (1991).","journal-title":"Theoretical Computer Science"},{"key":"CR13","unstructured":"Dietrich, S. W., ?Extension tables: Memo relations in logic programming?,Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, pp. 264?272 (August 1987)."},{"key":"CR14","unstructured":"Elkan, C., ?Conspiracy numbers and caching for searching and\/or trees and theorem proving?,Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, Detroit, Michigan, pp. 341?346 (August 1989)."},{"key":"CR15","unstructured":"Fern\u00e1ndez, J. A. and Minker, J., ?Bottom-up evaluation of hierarchical disjunctive deductive databases?,Proceedings of the Eighth International Conference on Logic Programming, Paris, France, pp. 660?675 (1991)."},{"key":"CR16","volume-title":"Exploiting constraints in design synthesis","author":"J. J. Finger","year":"1987","unstructured":"Finger, J. J., ?Exploiting constraints in design synthesis?, Ph.D. dissertation, Department of Computer Science, Stanford University, Stanford, California (February 1987)."},{"key":"CR17","unstructured":"Hasegawa, R. and Fujita, M., ?Parallel theorem provers and their applications?,Proceedings of the International Conference on Fifth Generation Computer Systems 1992, Tokyo, Japan, pp. 132?154 (June 1992)."},{"key":"CR18","unstructured":"Hobbs, J. R., Stickel, M., Appelt, D. and Martin, P., ?Interpretation as abduction?,Technical Note 499, Artificial Intelligence Center, SRI International (December 1990). Revised version to appear inArtificial Intelligence."},{"key":"CR19","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/0004-3702(92)90030-2","volume":"56","author":"K. Inoue","year":"1992","unstructured":"Inoue, K., ?Linear resolution for consequence finding?,Artificial Intelligence 56, 301?353 (1992).","journal-title":"Artificial Intelligence"},{"key":"CR20","unstructured":"Kemp, D. B., Stuckey, P. J. and Srivastava, D., ?Magic sets and bottom-up evaluation of well-founded models?,Proceedings of the 1991 International Symposium on Logic Programming, San Diego, California, pp. 337?354 (1991)."},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"Kowalski, R. A., ?Problems and promises of computational logic?,Proceedings of the First Symposium on Computational Logic, pp. 1?36 (1990).","DOI":"10.1007\/978-3-642-76274-1_1"},{"key":"CR22","unstructured":"Kumar, V. and Lin, Y.-J., ?An intelligent backtracking scheme for Prolog?,Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, pp. 406?414 (August?September 1987)."},{"key":"CR23","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D. W. Loveland","year":"1969","unstructured":"Loveland, D. W., ?A simplified format for the model elimination procedure?,J. ACM 16, 349?363 (1969).","journal-title":"J. ACM"},{"key":"CR24","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.,Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam, the Netherlands (1978)."},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Manthey, R. and Bry, F., ?Satchmo: A theorem prover implemented in Prolog?,Proceedings of the 9th International Conference on Automated Deduction, Argonne, Illinois, pp. 415?434 (May 1988).","DOI":"10.1007\/BFb0012847"},{"key":"CR26","series-title":"Technical Report","volume-title":"Otter 2.0 Users' Guide","author":"W. McCune","year":"1990","unstructured":"McCune, W., ?Otter 2.0 Users' Guide?,Technical Report ANL-90\/9, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois (March 1990)."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(90)90043-5","volume":"9","author":"V. S. Neiman","year":"1990","unstructured":"Neiman, V. S., ?Refutation search for Horn sets by a subgoal-extraction method?,J. Logic Programming 9, 267?284 (1990).","journal-title":"J. Logic Programming"},{"key":"CR28","unstructured":"Ng, N. T. and Mooney, R. J., ?An efficient first-order abduction system based on the ATMS?,Proceedings of the AAAI-91 National Conference on Artificial Intelligence, Anaheim, California (July 1991)."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"Nie, X. and Plaisted, D. A., ?A complete semantic back chaining proof system?,Proceedings of the 10th International Conference on Automated Deduction, Kaiserslautern, Germany, pp. 16?27 (July 1990).","DOI":"10.1007\/3-540-52885-7_76"},{"key":"CR30","unstructured":"Norvig, P., ?Inference in text understanding?,Proceedings of the AAAI-87 National Conference on Artificial Intelligence, Seattle, Washington (July 1987)."},{"key":"CR31","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1109\/TSMC.1987.4309027","volume":"2","author":"Y. Peng","year":"1987","unstructured":"Peng, Y. and Reggia, J. A., ?A probabilistic causal model for diagnostic problem solving ? Part I: Integrating symbolic causal inference with numeric probabilistic inference?,IEEE Transactions on Systems, Man, and Cybernetics SMC-17,2, 146?162 (1987).","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics SMC-17"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1109\/TSMC.1987.4309056","volume":"3","author":"Y. Peng","year":"1987","unstructured":"Peng, Y. and Reggia, J. A., ?A probabilistic causal model for diagnostic problem solving ? Part II: Diagnostic strategy?,IEEE Transactions on Systems, Man, and Cybernetics SMC-17,3, 395?406 (1987).","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics SMC-17"},{"key":"CR33","first-page":"150","volume-title":"Philosophical Writings of Charles Sanders Pierce","author":"C. S. Pierce","year":"1955","unstructured":"Pierce, C. S., ?Abduction and induction?, in Buchler, J. (ed.),Philosophical Writings of Charles Sanders Pierce, Dover Books, New York, pp. 150?156 (1955)."},{"issue":"3","key":"CR34","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. A. Plaisted","year":"1988","unstructured":"Plaisted, D. A., ?Non-Horn clause logic programming without contrapositive?,J. Automated Reasoning 4(3), 287?325 (1988).","journal-title":"J. Automated Reasoning"},{"issue":"4","key":"CR35","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF00244355","volume":"6","author":"D. A. Plaisted","year":"1990","unstructured":"Plaisted, D. A., ?A sequent-style model elimination strategy and a positive refinement?,J. Automated Reasoning 6(4), 389?402 (1990).","journal-title":"J. Automated Reasoning"},{"key":"CR36","unstructured":"Plaisted, D. A. and Greenbaum, S., ?Problem representations for chaining and equality in resolution theorem proving?,Proceedings of the First Conference on Artificial Intelligence Applications, Denver, Colorado, pp. 417?423 (December 1984)."},{"key":"CR37","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1111\/j.1467-8640.1989.tb00319.x","volume":"5","author":"D. Poole","year":"1989","unstructured":"Poole, D., ?Explanation and prediction: An architecture for default and abductive reasoning?,Computational Intelligence 5, 97?110 (1989).","journal-title":"Computational Intelligence"},{"key":"CR38","unstructured":"Pople, H. E., Jr, ?On the mechanization of abductive logic?,Proceedings of the Third International Joint Conference on Artificial Intelligence, Stanford, California, pp. 147?152 (August 1973)."},{"issue":"1","key":"CR39","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0004-3702(89)90067-2","volume":"38","author":"T. C. Przymusinski","year":"1989","unstructured":"Przymusinski, T. C., ?An algorithm to compute circumscription?,Artificial Intelligence 38(1), 49?73 (1989).","journal-title":"Artificial Intelligence"},{"issue":"3","key":"CR40","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00249019","volume":"7","author":"A. Ramsey","year":"1991","unstructured":"Ramsey, A., ?Generating relevant models?,J. Automated Reasoning 7(3), 359?368 (1991).","journal-title":"J. Automated Reasoning"},{"key":"CR41","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A., ?Automated deduction with hyper-resolution?,Int. J. Computer Mathematics 1, 227?234 (1965).","journal-title":"Int. J. Computer Mathematics"},{"key":"CR42","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF03037407","volume":"4","author":"J. Rohmer","year":"1986","unstructured":"Rohmer, J., Lescoeur, R. and Kerisit, J. M., ?The Alexander method ? a technique for the processing of recursive axioms in deductive databases?,New Generation Computing 4, 273?285 (1986).","journal-title":"New Generation Computing"},{"key":"CR43","doi-asserted-by":"crossref","unstructured":"Seki, H., ?On the power of Alexander templates?,Proceedings of the Eighth ACM SIGACT-SIGMODSIGART Symposium on Principles of Database Systems, Philadelphia, Pennsylvania, 150?159 (March 1989).","DOI":"10.1145\/73721.73737"},{"issue":"1","key":"CR44","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R. E. Shostak","year":"1976","unstructured":"Shostak, R. E., ?Refutation graphs?,Artificial Intelligence 7(1), 51?64 (1976).","journal-title":"Artificial Intelligence"},{"key":"CR45","unstructured":"Siegel, P.,Repr\u00e9sentation et Utilisation de la Connaissance en Calcul Propositionnel, Th\u00e8se d'Etat, Universit\u00e9 de Aix-Marseille, II, Marseille, France (1987)."},{"issue":"4","key":"CR46","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E., ?A Prolog technology theorem prover: Implementation by an extended Prolog compiler?,J. Automated Reasoning 4(4), 353?380 (1988).","journal-title":"J. Automated Reasoning"},{"key":"CR47","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF01531174","volume":"4","author":"M. E. Stickel","year":"1991","unstructured":"Stickel, M. E., ?A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation?,Annals of Mathematics and Artificial Intelligence 4, 89?106 (1991).","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"CR48","doi-asserted-by":"crossref","unstructured":"Tamaki, H. and Sato, T., ?OLD resolution with tabulation?,Proceedings of the Third International Conference on Logic Programming, London, England, pp. 84?98 (1986).","DOI":"10.1007\/3-540-16492-8_66"},{"key":"CR49","volume-title":"Principles of Database and Knowledge-Base Systems","author":"J. D. Ullman","year":"1989","unstructured":"Ullman, J. D.,Principles of Database and Knowledge-Base Systems, Computer Science Press, Rockville, Maryland (1989)."},{"key":"CR50","series-title":"Technical Report","volume-title":"Incorporating relevancy testing inSatchmo","author":"D. S. Wilson","year":"1989","unstructured":"Wilson, D. S. and Loveland, D. W., ?Incorporating relevancy testing inSatchmo?,Technical Report CS-1989-24, Department of Computer Science Duke University, Durham, North Carolina (November 1989)."},{"key":"CR51","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1992","unstructured":"Wos, L., Overbeek, R., Lusk, E. and Boyle, J.,Automated Reasoning: Introduction and Applications, 2nd edn, McGraw-Hill, New York (1992).","edition":"2nd edn"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881955.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881955\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881955","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:54:18Z","timestamp":1586044458000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881955"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":51,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881955"],"URL":"https:\/\/doi.org\/10.1007\/bf00881955","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}