{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T05:12:58Z","timestamp":1648617178024},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1995,10,1]],"date-time":"1995-10-01T00:00:00Z","timestamp":812505600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Appl Intell"],"published-print":{"date-parts":[[1995,10]]},"DOI":"10.1007\/bf00880011","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:26:53Z","timestamp":1104132413000},"page":"297-317","source":"Crossref","is-referenced-by-count":1,"title":["Formal reasoning in intelligent database systems"],"prefix":"10.1007","volume":"5","author":[{"given":"Shie-Jue","family":"Lee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-3384-5","volume-title":"Logic and Data Bases","author":"H. Gallaire","year":"1978","unstructured":"H. Gallaire and J. Minker,Logic and Data Bases, Plenum Press, New York, 1978."},{"key":"CR2","volume-title":"Expert Database Systems","author":"L. Kerschberg","year":"1987","unstructured":"L. Kerschberg,Expert Database Systems, The Benjamin\/Cummings Publishing Company, Menlo Park, CA, 1987."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"D.J. Israel, ?The role of logic in knowledge representation,?Computer, pp. 37?41, October, 1983.","DOI":"10.1109\/MC.1983.1654195"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"J.W. Lloyd,Foundations of Logic Programming, 2nd ed. Springer-Verlag, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"CR5","unstructured":"J.W. Lloyd, ?Logic as a foundation for deductive database systems,? inProceedings of IFIP Conference on Information Processing, San Francisco, August 1989, pp. 323?324."},{"key":"CR6","unstructured":"V. Lifschitz, ?Logical foundations of deductive databases,? inProceedings of IFIP Conference on Information Processing, San Francisco, August 1989."},{"key":"CR7","volume-title":"automated Theorem Proving: A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"D. Loveland,automated Theorem Proving: A Logical Basis, North-Holland, New York, 1978."},{"key":"CR8","unstructured":"D. Plaisted, ?An efficient relevance criterion for mechanical theorem proving,? inProceedings of the First Annual National Conference on Artificial Intelligence, pp. 79?83, 1980."},{"key":"CR9","unstructured":"S. Jefferson and D. Plaisted, ?Implementation of an improved relevance criterion,? inProceedings of the First Conference on Artificial Intelligence Applications, pp. 476?482, 1984."},{"key":"CR10","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"C. Chang and R. Lee,Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"D. Plaisted and S. Greenbaum, ?A structure-preserving clause form translation,?Journal of Symbolic Computation, 2:293?304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam, ?A computing procedure for quantification theory,?Journal of the Association for Computing Machinery, 7:201?215, 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"1","key":"CR13","first-page":"25","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"S.-J. Lee and D. Plaisted, ?Eliminating duplication with the hyper-linking strategy,?Journal of Automated Reasoning, 9(1):25?42, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. Robinson, and D. Carson, ?Efficiency and completeness of the set of support strategy in theorem proving,?Journal of the Association for Computing Machinery, 12:536?541, 1965.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"CR15","volume-title":"Otter 1.0 User's Guide","author":"W.W. McCune","year":"1989","unstructured":"W.W. McCune,Otter 1.0 User's Guide, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois, January 1989."},{"key":"CR16","unstructured":"J.D. Ullman,Database and Knowledge-Base Systems, Computer Science Press, 1988."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"S.-J. Lee and D. Plaisted, ?Problem solving by searching for models with a theorem prover,?Artificial Intelligence, to appear.","DOI":"10.1016\/0004-3702(94)90082-5"},{"key":"CR18","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1984","unstructured":"L. Wos, R. Overbeek, E. Lusk, and J. Boyle,Automated Reasoning: Introduction and Applications, Prentice Hall, Englewood Cliffs, N.J., 1984."},{"issue":"9","key":"CR19","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1145\/4284.4286","volume":"28","author":"F. Hayes-Roth","year":"1985","unstructured":"F. Hayes-Roth, ?Rule-based systems,?Communications of the Association for Computing Machinery, 28(9):921?932, 1985.","journal-title":"Communications of the Association for Computing Machinery"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M.E. Stickel","year":"1988","unstructured":"M.E. Stickel, ?A prolog technology theorem prover: Implementation by an extended prolog compiler,?Journal of Automated Reasoning, 4:353?380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"CR21","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"F.J. Pelletier, ?Seventy-five problems for testing automatic theorem provers,?Journal of Automated Reasoning, 2:191?216, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"CR22","volume-title":"Encyclopedia of Artificial Intelligence","author":"R.E. Korf","year":"1987","unstructured":"R.E. Korf, ?Search,? in S.C. Shapiro, editor,Encyclopedia of Artificial Intelligence, Wiley-Interscience, New York, 1987."},{"key":"CR23","unstructured":"X. Nie,Implementation Techniques in Automatic Theorem Proving, PhD. thesis, University of North Carolina at Chapel Hill, 1989."},{"key":"CR24","volume-title":"Problem-Solving Methods in Artificial Intelligence","author":"N.J. Nilsson","year":"1971","unstructured":"N.J. Nilsson,Problem-Solving Methods in Artificial Intelligence, McGraw-Hill, New York, 1971."},{"key":"CR25","unstructured":"S.-J. Lee and C.-H. Wu, ?Controlling storage consumption in mechanical theorem proving,? inProceedings of the 2nd International Conference on Automation Technology, Taipei, Taiwan, July 1992, pp. 201?207."},{"key":"CR26","volume-title":"Logic and Data Bases","author":"R. Reiter","year":"1978","unstructured":"R. Reiter, ?On closed world data bases,? in H. Gallaire and J. Minker, editors,Logic and Data Bases, Plenum Press, New York, 1978."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","volume":"13","author":"R. Reiter","year":"1980","unstructured":"R. Reiter, ?A logic for default reasoning,?Artificial Intelligence, 13:81?132, 1980.","journal-title":"Artificial Intelligence"},{"key":"CR28","unstructured":"D.W. Patterson,Introduction to Artificial Intelligence and Expert Systems, Prentice-Hall, Inc., 1990."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"T.M. Mitchell, R.M. Keller, and S.T. Kedar-Cabelli, ?Explanation-based generalization: A unifying view,?Machine Learning, 1(1), 1986.","DOI":"10.1007\/BF00116250"},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"G. DeJong and R. Mooney, ?Explanation-based learning: An alternative view,?Machine Learning, 1(2), 1986.","DOI":"10.1007\/BF00114116"},{"key":"CR31","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"D. Plaisted, ?Non-Horn clause logic programming without contrapositives,?Journal of Automated Reasoning, 4:287?325, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"J. Doyle, ?A truth maintenance system,?Artificial Intelligence, 12(3), 1979.","DOI":"10.1016\/0004-3702(79)90008-0"},{"key":"CR33","series-title":"Technical Report","volume-title":"An outlook on truth maintenance","author":"D. McAllester","year":"1980","unstructured":"D. McAllester, ?An outlook on truth maintenance,? Technical Report AIM-551, Artificial Intelligence Laboratory, MIT, Cambridge, MA, 1980."},{"key":"CR34","volume-title":"Artificial Intelligence","author":"E. Rich","year":"1991","unstructured":"E. Rich and K. Knight,Artificial Intelligence, McGraw-Hill, New York, 1991."},{"key":"CR35","volume-title":"A Computational Logic","author":"R. Boyer","year":"1979","unstructured":"R. Boyer and J.S. Moore,A Computational Logic, Academic Press, New York, 1979."},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"W. Bibel,Automated Theorem Proving, Vieweg, 1982.","DOI":"10.1007\/978-3-322-90100-2"},{"key":"CR37","volume-title":"International Workshop on Conditional Term-Rewriting Systems, Lecture Notes in Computer Science","author":"D.A. Plaisted","year":"1992","unstructured":"D.A. Plaisted, G. Alexander, H. Chu, and S.-J. Lee, ?Conditional term rewriting and first-order theorem proving,? inInternational Workshop on Conditional Term-Rewriting Systems, Lecture Notes in Computer Science, Pont-\u00e0-Mousson, France, July 1992."},{"key":"CR38","unstructured":"R.E. Korf, ?Real-time heuristic search: first results,? inProceedings of AAAI-87, Seattle, WA, 1987, pp. 133?138."},{"key":"CR39","unstructured":"B. Lipman, ?How to decide how to decide how to... limited rationality in decisions and games,? inProceedings of AAAI Symposium on AI and Limited Rationality, Stanford, CA, 1989."},{"key":"CR40","doi-asserted-by":"crossref","first-page":"1134","DOI":"10.1145\/1968.1972","volume":"18","author":"L.G. Valiant","year":"1984","unstructured":"L.G. Valiant, ?A theory of the learnable,?Communications of the ACM, 18:1134?1142, 1984.","journal-title":"Communications of the ACM"},{"key":"CR41","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0004-3702(88)90002-1","volume":"36","author":"D. Haussler","year":"1988","unstructured":"D. Haussler, ?Quantifying inductive bias: AI learning algorithms and Valiant's learning framework,?Artificial Intelligence, 36:177?221, 1988.","journal-title":"Artificial Intelligence"},{"key":"CR42","unstructured":"E.J. Horvitz, ?Reasoning under varying and uncertain resource constraints,? inProceedings of AAAI-88, St. Paul, MN, 1988, pp. 139?144."},{"key":"CR43","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/BF01531007","volume":"2","author":"O. Hansson","year":"1990","unstructured":"O. Hansson and A. Mayer, ?Probabilistic heuristic estimates,?Annuals of Mathematics and Artificial Intelligence, 2:209?220, 1990.","journal-title":"Annuals of Mathematics and Artificial Intelligence"},{"key":"CR44","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/0004-3702(91)90015-C","volume":"49","author":"S.J. Russel","year":"1989","unstructured":"S.J. Russel and E.H. Wefald, ?Principles of metareasoning,?Artificial Intelligence, 49:361?395, 1989.","journal-title":"Artificial Intelligence"},{"key":"CR45","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0004-3702(84)90026-2","volume":"22","author":"J.A. Barnett","year":"1984","unstructured":"J.A. Barnett, ?How much is control knowledge worth? A primitive example,?Artificial Intelligence, 22:77?89, 1984.","journal-title":"Artificial Intelligence"},{"key":"CR46","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0004-3702(80)90043-0","volume":"15","author":"R. Davis","year":"1980","unstructured":"R. Davis, ?Meta-rules: reasoning about control,?Artificial Intelligence, 15:179?222, 1980.","journal-title":"Artificial Intelligence"},{"key":"CR47","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1111\/j.1467-8640.1988.tb00284.x","volume":"4","author":"M. Bratman","year":"1988","unstructured":"M. Bratman, D. Israel, and M. Pollack, ?Plans and resource-bounded practical reasoning,?Computational Intelligence, 4:349?355, 1988.","journal-title":"Computational Intelligence"},{"key":"CR48","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0004-3702(89)90035-0","volume":"38","author":"D. Pastre","year":"1989","unstructured":"D. Pastre, ?MUSCADET: an automatic theorem proving system using knowledge and metaknowledge in mathematics,?Artificial Intelligence, 38:257?318, 1989.","journal-title":"Artificial Intelligence"},{"key":"CR49","unstructured":"S.-J. Lee and D. Plaisted, ?Use of replace rules in theorem proving,?Methods of Logic in Computer Science, to appear."},{"key":"CR50","doi-asserted-by":"crossref","unstructured":"S.A. Cook, ?The complexity of theorem-proving procedures,? inProceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151?158, 1971.","DOI":"10.1145\/800157.805047"},{"key":"CR51","unstructured":"M. Buro and U.K. B\u00fcning, ?Report on a SAT competition,? Technical report, Mathematik\/Informatik, Universit\u00e4t Paderborn, 1992."},{"key":"CR52","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1016\/0022-0000(84)90010-2","volume":"29","author":"D. Plaisted","year":"1984","unstructured":"D. Plaisted, ?Complete problems in the first-order predicate calculus,?Journal of Computer and System Sciences, 29:8?35, 1984.","journal-title":"Journal of Computer and System Sciences"},{"key":"CR53","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H. Lewis","year":"1980","unstructured":"H. Lewis, ?Complexity results for classes of quantificational formulas,?Journal of Computer and System Sciences, 21:317?353, 1980.","journal-title":"Journal of Computer and System Sciences"},{"key":"CR54","volume-title":"C-Prolog User's Manual","author":"F. Pereira","year":"1984","unstructured":"F. Pereira,C-Prolog User's Manual, SRI International, Menlo Park, California, August 1984."},{"key":"CR55","volume-title":"The Art of Prolog","author":"L. Sterling","year":"1986","unstructured":"L. Sterling and E. Shapiro,The Art of Prolog, The MIT Press, Cambridge, Massachusetts, 1986."}],"container-title":["Applied Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00880011.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00880011\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00880011","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:53:40Z","timestamp":1586044420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00880011"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,10]]},"references-count":55,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,10]]}},"alternative-id":["BF00880011"],"URL":"https:\/\/doi.org\/10.1007\/bf00880011","relation":{},"ISSN":["0924-669X","1573-7497"],"issn-type":[{"value":"0924-669X","type":"print"},{"value":"1573-7497","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,10]]}}}