{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:27Z","timestamp":1725456207866},"publisher-location":"Berlin\/Heidelberg","reference-count":43,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012833","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"197-217","source":"Crossref","is-referenced-by-count":5,"title":["Towards efficient \"knowledge-based\" automated theorem proving for non-standard logics"],"prefix":"10.1007","author":[{"given":"Michael A.","family":"McRobbie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul B.","family":"Thistlewaite","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Anderson, A.R. and Belnap, N.D. Jr. Entailment: The Logic of Relevance and Necessity, Vol. 1, Princeton U.P., Princeton, New Jersey, 1975."},{"key":"14_CR2","unstructured":"Beth, E.W. Formal Methods: An Introduction to Symbolic Logic and to the Study of Effective Operations in Arithmetic and Logic, Reidel, Dordrecht, 1962."},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel, W. \"Mating in Matrices\", Communications of the ACM, 26 (1983), 844\u2013852.","journal-title":"Communications of the ACM"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"Bledsoe, W.W. \"Non-Resolution Theorem Proving\", Artificial Intelligence, 9 (1977), 1\u201335.","journal-title":"Artificial Intelligence"},{"key":"14_CR5","volume-title":"The Computer Modelling of Mathematical Reasoning","author":"A. Bundy","year":"1983","unstructured":"Bundy, A. The Computer Modelling of Mathematical Reasoning, Academic Press, London, 1983."},{"key":"14_CR6","volume-title":"Foundations of Mathematical Logic","author":"H.B. Curry","year":"1963","unstructured":"Curry, H.B. Foundations of Mathematical Logic, McGraw-Hill, New York, 1963. (Corrected reprint, Dover, 1977.)"},{"key":"14_CR7","volume-title":"Elements of Intuitionism","author":"M. Dummett","year":"1977","unstructured":"Dummett, M. Elements of Intuitionism, Oxford U.P., Oxford, 1977."},{"key":"14_CR8","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-16780-3_100","volume-title":"Proceedings of the 8th International Conference on Automated Deduction","author":"N. Eisinger","year":"1986","unstructured":"Eisinger, N. \"What You Always Wanted to Know About Clause Graph Resolution\", 316\u2013336, in Proceedings of the 8th International Conference on Automated Deduction, ed. J. Siekmann, LNCS, Vol. 230, Springer, Berlin, 1986."},{"key":"14_CR9","unstructured":"Farinas del Cerro, L. and Orlowska, M. (eds.) Automated Reasoning in Non-Classical Logic, Special double issue of Logique et Analyse, 28 (1985), 115\u2013294."},{"volume-title":"Handbook of Philosophical Logic, Vol. 1","year":"1983","key":"14_CR10","unstructured":"Gabbay, D.M. and Guenthner, F. (eds.) Handbook of Philosophical Logic, Vol. 1, Reidel, Dordrecht, 1983. (Vol.2 was published in 1984 and Vol. 3 in 1985.)"},{"key":"14_CR11","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J.H. Gallier","year":"1986","unstructured":"Gallier, J.H. Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York, 1986."},{"key":"14_CR12","first-page":"153","volume-title":"Computers and Thought","author":"H. Gelernter","year":"1963","unstructured":"Gelernter, H. Hanson, J.R. and Loveland, D.W. \"Empirical Explorations of the Geometry Theorem-Proving Machine\", 153\u2013163, Computers and Thought, eds. E. Feigenbaum and J. Feldman, McGraw-Hill, New York, 1963."},{"key":"14_CR13","first-page":"65","volume":"69","author":"K. G\u00f6del","year":"1932","unstructured":"G\u00f6del, K. \"Zum intuitionistischen Aussagenkalk\u00fcl\", Anzeiger der Akademie der Wissenschaften Wien, mathematisch naturwissenschaftliche Klasse, 69 (1932), 65\u201366.","journal-title":"Anzeiger der Akademie der Wissenschaften Wien, mathematisch naturwissenschaftliche Klasse"},{"volume-title":"Theoretical Aspects of Reasoning About Knowledge: Proceedings of the 1986 Conference","year":"1986","key":"14_CR14","unstructured":"Halpern, J.Y. (ed.) Theoretical Aspects of Reasoning About Knowledge: Proceedings of the 1986 Conference, Morgan Kaufmann, Los Altos, California, 1986."},{"key":"14_CR15","doi-asserted-by":"crossref","first-page":"271","DOI":"10.2307\/2269618","volume":"30","author":"R. Harrop","year":"1965","unstructured":"Harrop, R. \"Some Structure Results for Propositional Calculus\", Journal of Symbolic Logic, 30 (1965), 271\u2013292.","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR16","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"Kleene, S. C. Introduction to Metamathematics, North-Holland, Amsterdam, 1952."},{"key":"14_CR17","volume-title":"Logic for Problem Solving","author":"R.E. Kowalski","year":"1979","unstructured":"Kowalski, R.E. Logic for Problem Solving, North-Holland, Amsterdam, 1979."},{"key":"14_CR18","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 1978."},{"volume-title":"IJCAI 87: Proceedings of the Tenth International Joint Conference on Artificial Intelligence, Vols. 1 and 2","year":"1987","key":"14_CR19","unstructured":"McDermott, J. (ed.) IJCAI 87: Proceedings of the Tenth International Joint Conference on Artificial Intelligence, Vols. 1 and 2, Morgan Kaufmann, Los Altos, 1987."},{"key":"14_CR20","unstructured":"McGovern, G. and McRobbie, M.A. \"On an Efficient Computer Implementation of A Decision Procedure for Intuitionistic Logic Using Matrix Models\", Manuscript, 1987."},{"key":"14_CR21","unstructured":"McRobbie, M.A. \"What is Relevant Resolution? A Simple Tutorial\", Manuscript, 1985. (Presented at the 1985 Conference of the Australasian Association for Logic.)"},{"key":"14_CR22","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BF00370441","volume":"38","author":"M.A. McRobbie","year":"1979","unstructured":"McRobbie, M.A. and Belnap, N.D. Jr. \"Relevant Analytic Tableaux\", Studia Logica, 38 (1979), 187\u2013200.","journal-title":"Studia Logica"},{"key":"14_CR23","first-page":"236","volume":"5","author":"M.A. McRobbie","year":"1982","unstructured":"McRobbie, M.A., Meyer, R.K. and Thistlewaite, P.B. \"Computer-Aided Investigations into the Decision Problem for Relevant Logics: The Search for a Free Associative Operation\", Australian Computer Science Communications, 5 (1982), 236\u2013267. (Proceedings of the 6th Australian Computer Science Conference, ed. L.M. Goldschlager, Basser Department of Computer Science, University of Sydney.)","journal-title":"Australian Computer Science Communications"},{"key":"14_CR24","unstructured":"McRobbie, M.A., Meyer, R.K. and Thistlewaite, P.B. \"A Challange\", Manuscript, 1987."},{"key":"14_CR25","first-page":"189","volume":"9","author":"M.A. McRobbie","year":"1980","unstructured":"McRobbie, M.A., Thistlewaite, P.B. and Meyer, R.K. \"A Mechanized Decision Procedure for Non-Classical Logic: The Program Kripke\", Bulletin of the Section of Logic, Polish Academy of Sciences, 9 (1980), 189\u2013192.","journal-title":"Bulletin of the Section of Logic, Polish Academy of Sciences"},{"key":"14_CR26","doi-asserted-by":"crossref","first-page":"717","DOI":"10.2307\/2273610","volume":"47","author":"M.A. McRobbie","year":"1982","unstructured":"McRobbie, M.A., Thistlewaite, P.B. and Meyer, R.K. \"A Mechanized Decision Procedure for Non-Classical Logic-the Program Kripke\", (Abstract), Journal of Symbolic Logic, 47 (1982), 717.","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR27","unstructured":"Malkin, P.K. and Martin, E.P. \"Logical Matrix Generation and Testing\", see these Proceedings."},{"key":"14_CR28","volume-title":"Principles of Artificial Intelligence","author":"N.J. Nilsson","year":"1980","unstructured":"Nilsson, N.J. Principles of Artificial Intelligence, Springer, Berlin, 1980."},{"key":"14_CR29","volume-title":"Natural Deduction: A Proof Theoretic Study","author":"D. Prawitz","year":"1985","unstructured":"Prawitz, D. Natural Deduction: A Proof Theoretic Study, Almqvist and Wiksell, Stockholm 1985."},{"key":"14_CR30","volume-title":"The Mathematics of Metamathematics","author":"H. Rasiowa","year":"1963","unstructured":"Rasiowa, H. and Sikorski, R. The Mathematics of Metamathematics, Polish Scientific Publishers (PWN), Warsaw, 1963. (3rd Edition, 1970.)","edition":"3rd Edition"},{"key":"14_CR31","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/TC.1976.1674613","volume":"C-25","author":"R. Reiter","year":"1976","unstructured":"Reiter, R. \"A Semantically Guided Deductive System for Automated Theorem Proving\", IEEE Transactions on Computers, C-25 (1976), 328\u2013334.","journal-title":"IEEE Transactions on Computers"},{"key":"14_CR32","volume-title":"Many-Valued Logic","author":"N. Rescher","year":"1969","unstructured":"Rescher, N. Many-Valued Logic, McGraw-Hill, New York, 1969."},{"key":"14_CR33","first-page":"317","volume":"17","author":"R. Routley","year":"1974","unstructured":"Routley, R. and Wolf, R.G. \"No Rational Logic Has a Finite Characteristic Matrix\", Logique et Analyse, 17 (1974), 317\u2013321.","journal-title":"Logique et Analyse"},{"key":"14_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10231-0","volume-title":"Using Sophisticated Models in Resolution Theorem Proving, LNCS, Vol. 90","author":"M.M. Sandford","year":"1980","unstructured":"Sandford, M.M. Using Sophisticated Models in Resolution Theorem Proving, LNCS, Vol. 90, Springer, Berlin, 1980."},{"key":"14_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof Theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"Sch\u00fctte, K. Proof Theory, trans. J. Crossley, Springer, Berlin, 1977."},{"key":"14_CR36","volume-title":"Deduktionssysteme: Automatisierung des logischen Denken","author":"J. Siekmann","year":"1987","unstructured":"Siekmann, J. \"Geschichte und Anwendungen\", in Deduktionssysteme: Automatisierung des logischen Denken, eds. K.H. Bl\u00e4sius and H.-J. B\u00fcrckert, Oldenbourg, Munich and Vienna, 1987."},{"key":"14_CR37","unstructured":"Slaney, J.K. Computers and Relevant Logics: A Project in Computing Matrix Model Structures for Propositional Logics, Ph.D. Thesis, Australian National University, 1980."},{"key":"14_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M. First-Order Logic, Springer, Berlin, 1968."},{"key":"14_CR39","first-page":"705","volume-title":"Proceedings of the 8th International Conference on Automated Deduction","author":"P.B. Thistlewaite","year":"1987","unstructured":"Thistlewaite, P.B., McRobbie, M.A. and Meyer, R.K. \"The Kripke Automated Theorem Proving System\", 705\u2013706 in Proceedings of the 8th International Conference on Automated Deduction, ed J. Siekmann, LNCS, Vol. 230, Springer, Berlin, 1987."},{"key":"14_CR40","series-title":"Research Notes in Theoretical Computer Science","volume-title":"Automated Theorem Proving in Non-Classical Logic","author":"P.B Thistlewaite","year":"1987","unstructured":"Thistlewaite, P.B, McRobbie, M.A. and Meyer, R.K. Automated Theorem Proving in Non-Classical Logic, Research Notes in Theoretical Computer Science, Pitman, London and Wiley, New York, 1987."},{"key":"14_CR41","first-page":"233","volume":"28","author":"P.B. Thistlewaite","year":"1985","unstructured":"Thistlewaite, P.B., Meyer, R.K. and McRobbie, M.A. \"Advanced Theorem Proving for Relevant Logics\", Logique et Analyse, 28 (1985), 233\u2013258.","journal-title":"Logique et Analyse"},{"key":"14_CR42","volume-title":"Logics for Artificial Intelligence","author":"R. Turner","year":"1984","unstructured":"Turner, R. Logics for Artificial Intelligence, Ellis Horwood, Chichester 1984."},{"key":"14_CR43","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-010-1161-7_7","volume-title":"Modern Uses of Multiple-Valued Logic","author":"R.G. Wolf","year":"1977","unstructured":"Wolf, R.G. \"A Survey of Many-Valued Logic\", 167\u2013323 in Modern Uses of Multiple-Valued Logic, ed. J.M. Dunn and G. Epstein, Reidel, Dordrecht, 1977."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012833.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:39Z","timestamp":1607353599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012833"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/bfb0012833","relation":{},"subject":[]}}