ORA Canada

ORA Canada
Home
Contact us
What's new?
Products and services
Z/EVES
EVES
Ada'95
Reports and Collections
ORA Canada
Bibliography
Automated Deduction
Bibliography
    A-B
    C-E
    F-G
    H-J
    K-L
    M-N
    O-R
    S-T
    U-Z

ORA Canada Bibliography of Automated Deduction: Authors M to N

[Madden 1988] P. Madden, The specialization of constructive existence proofs, DAI Research Paper no. 406, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1988.

*[Madden 1989] P. Madden, The specialization and transformation of constructive existence proofs, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 413-418.

*[Madden 1992] P. Madden, Automatic program optimization through proof transformation, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 446-460.

[Madlener 1987] K. Madlener, F. Otto, Groups presented by certain classes of finite length-reducing string rewriting systems, Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 133-144.

*[Maier 1988] D. Maier, D.S. Warren, Computing with Logic: Logic Programming with Prolog, The Benjamin/Cummings Publ. Co, Inc., Menlo Park, CA, 1988.

*[Malkin 1987] P.K. Malkin, E.P. Martin, MGT interactive, automated logical matrix testing and generation, Proc. Australian Joint Artificial Intelligence Conf. (AI'87), Syndney Masonic Centre, 2-4 November 1987, pp. 567-567.

*[Malkin 1988] P.K. Malkin, E.P. Martin, Logical matrix generation and testing, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 685-693; also available from Automated Reasoning Project, Australian National Univ., Canberra, ACT.2601, Australia.

[Maluszynski 1982] J. Maluszynski, J.F. Nilsson, Grammatical unification, Information Processing Letters 15(4), Netherlands, October 1982.

[Maluszynski 1985] J. Maluszynski, H.J. Komorowski, Unification-free execution of Horn clause programs, Proc. 2nd Logic Symp., pp. 78-86, 1985.

[Manna 1977] Z. Manna, R.J. Waldinger, Studies in Automatic Programming Logic, North-Holland, Amsterdam, 1977.

[Manna 1980] Z. Manna, R.J. Waldinger, A deductive approach to program synthesis, ACM Transactions of Programming Languages and Systems 2(January 1980):90-121.

[Manna 1981] Z. Manna, R.J. Waldinger, Deductive synthesis of the unification algorithm, Science of Computer Programming 1(1981):5-48.

[Manna 1985a] Z. Manna, R. Waldinger, Special relations in automated deduction, CS Report STAN-CS-85-1051, Stanford Univ., 1985; also Proc. 12th Colloquium Automata, Language and Programming (Natplion, Greece, July 1985), ed. W. Brauer, LNCS 194, Springer-Verlag, Berlin, 1985, pp. 413-423; also JACM 33(1):1-59, January 1986.

[Manna 1985b] Z. Manna, R. Waldinger, The logical basis for computer programming, Vol. 1: Deductive reasoning, Addison-Wesley, Reading, MA, 1985.

[Manna 1986a] Z. Manna, R. Waldinger, How to clear a block: plan formulation in situational logic, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 622-640.

[Manna 1986b] Z. Manna, R. Waldinger, Deduction with relation matching, Proc. 5th Conf. Foundations of Software Technology and Theoretical Computer Science (New Delhi, India, December 1985), ed. S.N. Maheshwari, LNCS 206, Springer-Verlag, Berlin, 1985, pp. 212-224.

[Manna 1987] Z. Manna, R. Waldinger, How to clear a block: A theory of plans, J. of Automated Reasoning 3(4):343-377, December 1987.

*[Manna 1992] Z. Manna, R. Waldinger, The special-relation rules are incomplete, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 492-506.

*[Manna 1993] Z. Manna, R. Waldinger, The Deductive Foundations of Computer Programming, Addison-Wesley, 1993.

*[Manthey 1987] R. Manthey, F. Bry, A hyperresolution-based proof procedure and its implemention in PROLOG, Proc. 11th German Workshop on Artificial Intelligence (GWAI-87, Geseke, September 28-October 2, 1987), ed. K. Morik, Springer-Verlag, Berlin, 1987, pp. 221-230.

*[Manthey 1988] R. Manthey, F. Bry, SATCHMO: A theorem prover implemented in Prolog, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 415-434.

*[Marcus 1988] L. Marcus, T. Redmond, Two automated methods in implementation proofs, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 622-542.

*[Marcus 1996a] L. Marcus, The Incorporation of Testing into Formal Verification: Direct, Modular, and Hierarchical Correctness Degrees, Formal Methods in System Design 9(3), 235-262 (1996).
(source: Leo Marcus)

*[Marcus 1996b] L. Marcus, Syntactic and Semantic Dependence of Array-Arithmetic Sentences, with an Application to Program Verification, Fundamenta Informaticae 27, 77-100 (1996).
(source: Leo Marcus)

*[Marien 1991] A. Marien, B. Demoen, A new scheme for unification in WAM, In Logic Programming: Proc. 1991 Intl. Symp., ed. V. Saraswat and K. Ueda, The MIT Press, Cambridge, MA, 1991, pp. 257-271.

[Markov 1951] A. Markov, Impossibility of algorithms for recognizing some properties of associative systems, Dokl. Ada. Nauk SSSR 77(1951):953-956.

[Martelli 1976] A. Martelli, U. Montanari, Unification in linear time and space: A structured presentation, Nota interna B76-16, Instituto di Elaborazione della Informazione, Consiglio Nazionale delle Ricerche, Univ. of Pisa, Pisa, Italy, July 1976.

[Martelli 1977] A. Martelli, U. Montanari, Theorem proving with structure sharing and efficient unification, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, p. 543.

[Martelli 1982] A. Martelli, U. Montanari, An efficient unification algorithm, Tech. Report, Univ. of Pisa, 1979; also ACM Trans. on Programming Languages and Systems 4(2):258-282, April 1982.

[Martelli 1984] A. Martelli, G.F. Rossi, Efficient unification with infinite terms in logic programming, Proc. Intl. Conf. on Future Generations Computer Systems, North-Holland, 1984, pp. 202-209.

*[Martelli 1986] A. Martelli, C. Moiso, G. Rossi, An algorithm for unification in equational theories, Proc. 3rd IEEE Symp. on Logic Programming (Salt Lake City, Utah, 22-25 September 1986), pp. 180-186.

*[Martelli 1989] A. Martelli, C. Moiso, G.F. Rossi, Lazy unification algorithms for canonical rewrite systems, In: Resolution of Equations in Algebraic Structures: Vol 2, Rewriting Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 245-274.

*[Martin 1989] U. Martin, T. Nipkow, Ordered rewriting and confluence, Technical Report No. 170, University of Cambridge Computer Laboratory, May 1989.

[Martin 1971a] W.A. Martin, R.J. Fateman, The MACSYMA system, Proc. Second Symp. on Symbolic Manipulation, ed. S.R. Petrick, Los Angeles, 1971, pp. 59-75.

*[Martin 1971b] W.A. Martin, Determining the equivalence of algebraic expressions by hash coding, Proc. 2nd Symp. on Symbolic and Algebraic Manipulation (Los Angeles, CA, March 23-25), ed. S.R. Petrick, ACM, NY, 1971, 305-310; also JACM 18(4):549-558, 1971.

[Martin 1986a] U. Martin, Doing algebra with REVE, UMCS-86-10-4, Dept. of Computer Science, Univ. of Manchester, June 1986.

[Martin 1986b] U. Martin, Unification in Boolean rings and unquantified formulae of first order predicate calculus, UMCS-86-11-2, Dept. of Computer Science, Univ. of Manchester, November 1986.

[Martin 1986c] U. Martin, T. Nipkow, Unification in Boolean rings, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 506-513.

[Martin 1987] U. Martin, How to choose the weights in the Knuth Bendix ordering, Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 42-53.

*[Martin 1988] U. Martin, T. Nipkow, Unification in Boolean rings, J. Automated Reasoning 4(4):381-396 , December 1988.

*[Martin 1989] U. Martin, T. Nipkow, Ordered rewriting and confluence, Tech. Report 170, Computer Lab., Univ., of Cambridge, May 1989; Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 366-380.

[Martin-Lof 1970] P. Martin-Lof, Notes on Constructive Mathematics, Almqvist & Wiksell, Stockhom, 1970.

[Martin-Lof 1984] P. Martin-Lof, Intuitionistic type theory, Studies in Proof Theory Lecture Notes, Bibliopolis, 1984.

[Maslov 1964] S. Yu Maslov, An inverse method for establishing deductability in classical predicate calculus, in Dokl. Akad. Nauk, SSSR 159(1964):17-20.

[Maslov 1965] S. Yu Maslov, G.E. Mints, V.P. Orevkov, Unsolvability in the constructive predicate calculus of certain classes of formulas containing only monadic predicate variables, Soviet Math. Dokl. 163(2):295-297, 1965.

[Maslov 1966] S. Yu Maslov, Application of the inverse method of establishing deducibility to the theory of decidable fragments of classical predicate calculus (translated), in Dokl. Akad. Nauk SSSR 171(1966):1282-1285.

[Maslov 1967] S. Yu Maslov, An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus (translated), in Dokl. Akad. Nauk SSSR 172(1967):22-25; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 48-54.

[Maslov 1968] S.J. Maslov, The inverse method for establishing deducibility for logical calculi, Proc. Steklov Inst. Math. 98, 1968; also Trudy Instituta Matematiki, vol. 67, 1968.

[Maslov 1969a] S. Yu Maslov, A connection between tactics of the resolution and inverse methods, Zapiski Nauchnyh Seminarov Loni 16(1969):137-146.

[Maslov 1969b] S. Yu Maslov, Invertible sequential variant of constructive predicate calculus, Seminar in Mathematics 4, V.A. Steklov Mathem. Institute, Leningrad, Consultants Bureau, NY-London, 1969, pp. 36-42.

[Maslov 1971a] S. Maslov, Proof-search strategies for methods of the resolution type, Machine Intelligence 6, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1971, pp. 77-89.

[Maslov 1971b] S. Yu Maslov, Deduction-search tactics based on unification of the order of members in a favourable set, Seminars in Mathematics 16, V.A. Steklov Mathem. Institute, Leningrad, Consultants Bureau, NY-London, 1971, pp. 64-68.

[Maslov 1971c] S. Yu Maslov, Relationship between tactics of the inverse method and the resolution method, Seminars in Mathematics 16, V.A. Steklov Mathem. Institute Leningrad, Consultants Bureau, NY-London, 1971, pp. 69-73; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 264-272.

[Maslov 1983] S.Y. Maslov, G.E. Mints, V.P. Orevkov, Mechanical proof search and the theory of logical deduction in the USSR, in Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 424-483, pp. 29-38.

[Mathlab 1977] The Mathlab Group, MACSYMA Reference Manual, Lab. for Computer Science, MIT, December 1977.

[Matrosov 1978] V.M. Matrosov, S.N. Vasil'Yev, A comparison principle for theorem deducing II, Tekh. Kibernetika 14(4):40-49, USSR, July 1978.

[Matulis 1963] V.A. Matulis, Variants of the Classical Predicate Calculus with Unique Deduction Tree, Soviet Math. Dokl. 148(4):768-770, 1963.

[Matwin 1985] S. Matwin, T. Pietrzykowski, Intelligent backtracking in plan-based deduction, IEEE Trans. on Pattern Analysis and Machine Intelligence PAMI-7(6):682-692, November 1985.

[Mayfield 1988] B. Mayfield, The role of term symmetry in equational unification and completion procedures, PhD dissertation, Univ. of Missouri-Rolla, Rolla, MO, 1988.

[Mazaud 1987] M. Mazaud, R. Rakotozafy, A. Szumachowski-Despland, Code generator generation based on template-driven target term rewriting, Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 105-120.

[McAllester 1980a] D.A. McAllester, The use of equality in deduction and knowledge representation, Master's Thesis, Technical Report 550, MIT Artificial Intelligence Lab., January 1980.

[McAllester 1980b] D.A. McAllester, An outlook on truth maintenance, Memorandum 551, MIT Artificial Intelligence Lab., August 1980.

[McAllester 1981] D.A. McAllester, Algebraic approximation, Proc. 7th IJCAI, pp. 1024-1026, 1981.

[McAllester 1982] D.A. McAllester, Reasoning utility package user's manual, Version one, AI Lab. MIT, AIM-667, April 1982; also available on microfilm as N00014-75-C-0643, Massachusetts Institute of Technology, April 1982,

[McAllester 1987] D.A. McAllester, ONTIC: A knowledge representation system for mathematics, PhD thesis, MIT AI Lab. Tech. Report 979, July 1987.

[McAllester 1988] D.A. McAllester, ONTIC: A knowledge representation system for mathematics (abstract), Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 742-743.

[McAllester 1991a] D. McAllester, Grammar Rewriting, AIM-1342, MIT AI Lab., December 1991.

[McAllester 1991b] D. McAllester, J. Siskind, Lifting transformations, AIM-1343, MIT AI Lab., December 1991.

[McAllester 1991c] D. McAllester, Tractable inference relations, AIM-1344, MIT AI Lab., December 1991.

*[McAllester 1992] D. McAllester, Grammar rewriting, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 124-138.

[McCarthy 1960] J. McCarthy, Recursive functions of symbolic expressions and their computations by machine, Part I, CACM 3(4), 1960, 184-195.

[McCarthy 1962a] J. McCarthy, Computer programs for checking mathematical proofs, Proc. Symposia in Pure Mathematics, Vol. 5, Recursive Function Theory, American Mathematical Society, Providence, RI, 1962, pp. 219-227.

[McCarthy 1962b] J. McCarthy, Towards a mathematical science of computation, Proc. IFIP Congress, Amsterdam, 1962.

[McCarthy 1963a] J. McCarthy, Situations, actions and causal laws, Stanford AI Project, Memo No. 2, 1963; also Reprinted in Semantic Information Processing, ed. M. Minsky, MIT Press, Cambridge, MA, 1968, pp. 410-417.

[McCarthy 1963b] J. McCarthy, A basis for a mathematical theory of computation, in Computer Programming and Formal Systems, ed. P. Brafford and D. Hirschberg, North-Holland, Amsterdam, 1963, pp. 33-70.

[McCarthy 1964] J. McCarthy, A tough nut for proof procedures, Stanford Artificial Intelligence Project, Memo 16, Stanford Univ., 1964.

[McCarthy 1968] J. McCarthy, Programs with common sense, in Semantic Information Processing, ed. Minsky, MIT Press, Cambridge, MA, 1968, pp. 403-418.

[McCarthy 1969] J. McCarthy, Recursive functions of symbolic expressions and their computations by machine, Part I, CACM 3(1969):184-195.

[McCarthy 1980] J. McCarthy, C. Talcott, LISP: Programming and proving, to appear, available as Stanford CS206 Course Notes, Fall 1980.

[McCarty 1986] L.T. McCarty, Fixed point semantics and tableau proof procedures for a clausal intuitionistic logic, Tech. Report LRP-TR-18, Dept. of Computer Science, Rutgers, 1986.

[McCharen 1976a] J.D. McCharen, R.A. Overbeek, L. Wos, Complexity and related enhancements for automated theorem proving programs, Computers and Mathematics with Applications 2(1976):1-16.

[McCharen 1976b] J. McCharen, R. Overbeek, L. Wos, Problems and experiments for and with automated theorem proving programs, IEEE Trans. on Computers C-25(8):773-782, 1976.

[McCune 1981] W.W. McCune, An inference mechanism for resolution-style theorem provers, M.A. thesis, Northwestern Univ., 1981.

[McCune 1982] W. McCune, User guide for the Northwestern University Theorem-proving System (NUTS), 1982.

[McCune 1983] W.W. McCune, L.J. Henschen, Semantic paramodulation for Horn sets, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 902-908.

[McCune 1985] W.W. McCune, L.J. Henschen, Experiments with semantic paramodulation, J. of Automated Reasoning 1(3):231-261, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[McCune 1987a] W. McCune, L. Wos, A case study in automated theorem proving: Finding sages in combinatory logic, J. of Automated Reasoning 3(1):91-107, March 1987.

[McCune 1987] W. McCune, Un-skolemizing clause sets, Tech. Memo ANL/MCS-TM-93, Argonne National Laboratory, 1987; also Information Processing Letters 29(November 1988):257-263.

*[McCune 1988] W. McCune, Challenge equality problems in lattice theory, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 704-709.

[McCune 1989] W. McCune, Otter 1.0 users' guide, Tech. Report ANL-88-44, Argonne National Laboratory, Argonne, IL, January 1989.

[McCune 1990a] W. McCune, OTTER 2.0 users guide, Tech. Report ANL-90/9, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, March 1990.

*[McCune 1990b] W. McCune, OTTER 2.0 (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 663-664.

*[McCune 1990c] W. McCune, Skolem functions and equality in automated deduction, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 246-251.

[McCune 1990d] W. McCune, Experiments with discrimination tree indexing and path indexing for term retrieval, MCS Preprint P191-1190, Mathematics and Computer Science Division, Argonne National Laboratory, 1990; to appear in J. Automated Reasoning.

*[McCune 1992] W. McCune, L. Wos, Experiments in automated deduction with coondensed detachment, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 209-223.

*[McCune 1996] W. McCune and R. Padmanabhan Automated Deduction in Equational Logic and Cubic Curves Lecture Notes in AI, #1095, LN in CS, Springer-Verlag, 1996.
(source: Dr. R. Padmanabhan) [McDermott 1979] J. McDermott, Learning to use analogies, IJCAI-79, 1979, pp. 568-576.

*[McDermott 1987] D.V. McDermott, Logic, problem solving, and deduction, Annual Review of Computer Science, Vol. 2, 1987. pp. 187-229. [McDonald 1984] J. McDonald, P. Suppes, Student use of an interactive theorem prover, In: Automated Theorem Proving: After 25 Years, ed. W.W. Bledsoe and D. Loveland, Contemporary Mathematics Series 19, American Math. Society, Providence, RI, 1984, pp. 89-118, pp. 315-360.

[McGovern 1984] G.J. McGovern, Automatic theorem-proving for some non-classical logics, M.A. thesis, La Trobe Univ., 1984.

[McKay 1981] D.P. McKay, S. Shapiro, Using active connection graphs for reasoning with recursive rules, Proc. 7th Intl. Joint Conf. on Artificial Intelligence, Vancouver, BC, 1981, pp. 368-374.

[McKinsey 1943] J.C.C. McKinsey, The decision problem for some classes of sentences without quantifiers, J. Symb. Logic 8(3):61-76, 1943.

*[McMichael 1990] A.F. McMichael, ALIM: An automated reasoner for equivalences, applied to set theory, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 308-321.

[McNulty 1976a] G. McNulty, The decision problem for equational bases of algebras, Annals of Mathematical Logic 10(1976):193-259.

[McNulty 1976b] G. McNulty, Undecidable properties of finite sets of equations, JSL 41(3):180-186, 1976.

*[McNulty 1989] G.F. McNulty, An equational logic sampler, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 234-262.

[McRobbie 1979a] M.A. McRobbie, A proof theoretic investigation of relevant and modal logics, PhD thesis, Australian National Univ., Canberra, 1979.

[McRobbie 1979b] M.A. McRobbie, N.D. Belnap Jr., Relevant analytic tableaux, Studia Logica 38:187-200, 1979.

[McRobbie 1980] M.A. McRobbie, R.K. Meyer, P.B. Thistlewaite, A mechanized decision procedure for non-classical logic: The program KRIPKE, Bulletin of the Section of Logic, Polish Academy of Sciences, 9(1980):189-192; Abstract, J. of Symbolic Logic 47(1982):717.

[McRobbie 1982] M.A. McRobbie, R.K. Meyer, P.B. Thistlewaite, Computer-aided investigations into the decision problem for relevant logics: The search for a free associative connective, Australian Computer Science Communications 5(1982):236-267; also Proc. 6th Australian Computer Science Conf., ed. L.M. Goldschlager, Basser Dept. of Computer Science, Univ. of Sydney, 1983.

[McRobbie 1984] M.A. McRobbie, N.D. Belnap Jr., Proof tableau formulations of some first-order relevant ortho-logics, Bulletin of the Section of Logic, Polish Academy of the Sciences 13:233-240, 1984.

*[McRobbie 1987] M.A. McRobbie, Towards efficient knowledge-based automated theorem proving for non-standard logics, SEKI Report SR-87-12, Universitat Kaiserslautern, 1987; also with R.K. Meyer and P.B. Thistlewaite, in Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Ilinois, May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 197-217.

*[McRobbie 1988] M.A. McRobbie, R.K. Meyer, P.B. Thistlewaite, Towards efficient ``knowledge-based'' automated theorem proving for non-standard logics, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 197-217.

*[McRobbie 1991] M.A. McRobbie, Automated reasoning and nonclassical logics: Introduction, J. Automated Reasoning 7(4):447-451, December 1991.

*[Meier 1990] M. Meier, Compilation of compound terms in Prolog, Logic Programming: Proc. of the 1990 North American Conf., ed. S. Debray and M. Hermenegildo, The MIT Press, Cambridge, MA, 1990, pp. 63-79.

*[Melham 1989] T.F. Melham Automating recursive type definitions in higher order logic, In Current Trends in Hardware Verification and Automated Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, NY, 1989, pp. 341-386.

[Melle 1981] W.J. van Melle, System Aids in Constructing Consultation Programs, UMI Research Press, Ann Arbor, Michigan, 1981.

[Meltzer 1965] B. Meltzer, Theorem-proving for computers, Memo 24, Metamathematics Unit, Univ. of Edinburgh, Edinburgh, 1965.

[Meltzer 1966a] B. Meltzer, Theorem proving for computers: Some results on resolution and renaming, Computer J. 8(4):341-343, January 1966; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 493-495.

[Meltzer 1966b] B. Meltzer, P. Poggi, An improved complete strategy for TP by resolution report, Metamathematics Unit, Univ. of Edinburgh, Edinburgh, 1966.

[Meltzer 1967a] B. Meltzer, Logic and the formalization of mathematics, Science Progress 55(1967):583-595, Oxford.

[Meltzer 1967b] B. Meltzer, Mathematics, logic and undecidability, Memo No. 9, Metamathematics Unit, Univ. of Edinburgh, Edinburgh, 1967.

[Meltzer 1968a] B. Meltzer, A new look a mathematics and its mechanization, Machine Intelligence 3, ed. Michie, American Elsevier, NY, 1968, pp. 63-70.

[Meltzer 1968b] B. Meltzer, Some notes on resolution strategies, Machine Intelligence 3, ed. Michie, American Elsevier, NY, 1968, pp. 71-76.

[Meltzer 1968c] B. Meltzer, Some recent developments in complete strategies for theorem proving by computers, Zeitschr. fur Math. Logik und Grundl. der Math., Ed. 14, 1968, pp. 377-382.

[Meltzer 1969] B. Meltzer, The use of symbolic logic in proving mathematical theorems by means of a digital computer, Foundations of Maths. pp. 39-44, Springer, NY, 1969.

[Meltzer 1970b] B. Meltzer, Power amplification for theorem-provers, Machine Intelligence 5, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1970, pp. 165-179.

[Meltzer 1970c] B. Meltzer, The semantics of induction and the possibility of complete systems of inductive inference, Artificial Intelligence 1(3):189-192, 1970.

[Meltzer 1970d] B. Meltzer, Generation of hypothesis and theories, Nature 225(1970):972, London.

[Meltzer 1971a] B. Meltzer, The programming of deduction and induction, DCL memo 45, Dept. of Computational Logic, Univ. of Edinburgh, 1971; also Proc. NATO Symp. on Human Thinking, Comp. Tech., 1971.

*[Meltzer 1971b] B. Meltzer, Prolegomena to a theory of efficiency of proof procedures, Artificial Intelligence and Heuristic Programming, ed. Findler and Meltzer, American Elsevier, NY, 1971, pp. 15-33; also Department of Computational Logic Memo DCL-37, University of Edinburgh, 1971.

[Meltzer 1973a] B. Meltzer, The impossibility of perfect proof procedures, AISB European Newsletter 15(November 1973):28-29.

[Meltzer 1973b] B. Meltzer, Proof, abstraction and semantics in mathematics and artificial intelligence, DCL Memo No. 85, Edinburgh Univ., Edinburgh, 1973.

[Mendelson 1964] E. Mendelson, Introduction to Mathematical Logic, Van Nostrand, Princeton, 1964.

[Meseguer 1985] J. Meseguer, J.A. Goguen, Deduction with many-sorted rewrite rules, Report CSLI-85-42, Center for the Sutdy of Language and Information, Stanford Univ., CA, 1985.

[Meseguer 1987] J. Meseguer, J. Goguen, G. Smolka, Order-sorted unification, Report CSLI-87-86, Centre for the Study of Language and Information, Stanford Univ., CA, March 1987.

[Metivier 1983] Y. Metivier, About the rewriting systems produced by the Knuth-Bendix completion algorithm, Information Processing Letters 16(1):31-34, 24 January 1983.

[Mey 1990] D. Mey, A predicate calculus with control of derivations, to be published in Proc. 3rd Computer Science Logic Workshop, LNCS, 1990.

*[Meyer 1991] R.K. Meyer, M.W. Bunder, L. Powers, Implementing the `Fools's Model' of combinatory logic, J. Automated Reasoning 7(4):597-630, December 1991.

[Michalski 1973] R.S. Michalski, Discovering classification rules using variable-valued logic system VL1, Proc. 3rd IJCAI, Stanford Univ., Stanford, August 1973, pp. 162-172.

[Michalski 1983] R.S. Michalski, J.C. Carbonell, T.M. Mitchell, Machine Learning (Vol. 1), Tioga Press, Palo Alto, 1983.

[Michalski 1986] R.S. Michalski, J.C. Carbonell, T.M. Mitchell, Machine Learning (Vol. 2), Tioga Press, Palo Alto, 1986.

[Michie 1968] D. Michie, "Memo" functions and machine learning, Nature 218(1968):19-22.

[Michie 1970] D. Michie, Notes on G-Deduction, Memo MIP-R-93, Univ. of Edinburgh, Edinburgh, 1970.

[Michie 1972] D. Michie, R. Ross, G.J. Shannan, G-deduction, Machine Intelligence 7, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, 1972, pp. 141-165.

*[Middeldorp 1989a] A. Middeldorp, A sufficient condition for the termination of the direct sum of term rewriting systems, Proc. 4th Annual Symp. Logic in Computer Science (Pacific Grove, CA, 5-8 June 1989), IEEE, 1989, pp. 396-401.

*[Middeldorp 1989b] A. Middeldorp, Modular aspects of properties of term rewriting systems related to normal forms, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 263-277.

[Miller 1982] D.A. Miller, E. Cohen, P.B. Andrews, A look at TPS, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 50-69.

[Miller 1983] D.A. Miller, Proofs in higher-order logic, PhD thesis, Carnegie-Mellon Univ., October 1983, available as Tech. Report MS-CIS-83-37, 1983.

[Miller 1984] D. Miller, Expansion tree proofs and their conversion to natural deduction proofs, MS-CIS-84-6, Univ. of Pennsylvania, February 1984; also Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 375-393.

[Miller 1986] D. Miller, A. Felty, An integration of resolution and natural deduction theorem proving, MS-CIS-86-47, Univ. of Pennsylvania, 1986; also in Proc. AAAI-86, 5th Natl. Conf. on Artificial Intelligence, ed. T. Kehler, S. Rosenschein, R. Filman, and P.F. Patel-Schneider, Philadelphia, PA, 11-15 August 1986, pp. 198-202.

[Miller 1987a] M. Miller, D. Perlis, Proving self-utterances, J. of Automated Reasoning 3(3):329-338, September 1987.

[Miller 1987b] D. Miller, G. Nadathur, A. Scedrov, Hereditary Harrop formulas and uniform proofs systems, Proc. 2nd Annual Symp. on Logic in Computer Science, Cornell Univ., June 1987, pp. 98-105.

[Miller 1987c] D.A. Miller, A compact representation of proofs, Studia Logica 46(4):347-370, 1987. *[Miller 1988] S.A. Miller, L.K. Schubert, Using specialists to accelerate general reasoning, Proc. AAAI-88, 7th National Conf. on Artificial Intelligence, Vol. 1, (St. Paul, Minnesota, 21-26 August 1988), pp. 161-165.

[Mills nd] C. Mills, Introduction to ORACLE/Caliban, Internal Memo, Odyssey Research Associates, Ithaca, NY 14850.

[Millstein 1968] R. Millstein, The Logic Theorist in LISP.Intern, J. Computer Math. 2(April 1968):111-122.

[Milner 1972a] R. Milner, R. Weyhrauch, Proving computer correctness in mechanized logic, In Machine Intelligence 7, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, Scotland, 1972, pp. 51-70.

[Milner 1972b] R. Milner, Implementation and application of Scott's logic for computable functions, Proc. ACM Conf. on Proving Assertions about Programs, SIGPLAN Notice 7(1972).

[Milner 1983] R. Milner, A proposal for standard ML, Report CSR-157-83, Computer Science Dept., Univ. Edinburgh, 1983, also in Conf. Record of 1984 ACM Symp. on LISP and Functional Programming, Austin, TX, August 1984.

[Milner 1984] R. Milner, The use of machines to assist in rigorous proof, Philos. Trans. Roy. Soc. London 312:411-422, 1984; also in Mathematical Logic and Programming Languages, ed. C.A.R. Hoare and J.C. Shepherdson, Prentice-Hall, 1985, pp. 77-88.

*[Milner 1987] R. Milner, Dialogue with a proof system, Proc. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'87, Pisa, Italy, 23-27 March 1987), Vol. I, ed. H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, LNCS 249, Springer-Verlag, Berlin, 1987, pp. 271-275.

[Minicozzi 1972] E. Minicozzi, R. Reiter, A note on linear resolution strategies in consequence-finding, Artificial Intelligence 3(1972):175-180.

[Minker 1973a] J. Minker, D.H. Fishman, J.R. McSkimin, The Q* algorithm - a search strategy for a deductive question answering system, Proc. 3rd IJCAI, Stanford Univ., Stanford, August 1973, pp. 31-37.

[Minker 1973b] J. Minker, D.H. Fishman, J.R. McSkimin, MRPPS - An interactive refutation proof procedure system for question-answering, TR-228, Computer Sci. Cent., Univ. of Maryland, College Park, 1973.

[Minker 1979] J. Minker, G. Zanon, LUSH resolution: resolution with arbitrary selection function, Univ. of Maryland, Tech. Rep. TR-736, February 1979.

[Minker 1982] J. Minker, G. Zanon, An extension to linear resolution with selection function, Information Processing Letters 14(4):191-194, Netherlands, June 1982.

[Minker 1983] J. Minker, J. Nicolas, On recursive axioms in deductive databases, Information systems 8(1):1-13, 1983.

[Minker 1984] J. Minker, D. Perlis, Applications of protected circumscription, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 414-425.

*[Minker 1988] J. Minker, A. Rajasekar, Procedural interpretation of non-Horn logic programs, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 278-293.

[Minksy 1956] M. Minsky, Notes on the Geometry Problem, AI-Project, Dartmouth College, Hanover, 1956.

[Minor 1979] J.T. Minor, Proving a subset of second order logic with first order proof procedures, PhD, Dept. Math. Univ. of Texas at Austin, 1979.

[Mints 1969] G.E. Mints, Variation in the Deduction Search Tactics in Sequential Calculi, Seminars in Mathematics 4, V.A. Steklov Mathem. Institute, Leningrad, Consultants Bureau, NY-London, 1969, pp. 52-59.

*[Mints 1991] G. Mints, T. Tammet, Condensed detachment is complete for relevance logic: A computer-aided proof, J. Automated Reasoning 7(4):587-596, December 1991.

[Miranker 1987a] D.P. Miranker, TREAT: A new and efficient match algorithm for AI production systems, TR-87-03, Univ. of Texas at Austin, Department of Computer Sciences, 1987.

*[Miranker 1987b] D.P. Miranker, TREAT: A better match algorithm for AI production systems, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, pp. 42-47.

*[Miranker 1990] D.P. Miranker, D.A. Brant, B. Lofaso, D. Gadbois, On the performance of lazy matching in production systems, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990, 1990), Vol. 2, AAAI Press/The MIT Press, Menlo Park/Cambridge, pp. 685-692.

[Mitra 1988] G. Mitra, M. Tamiz, J. Yadegar, Experimental investigation of an interior search method within a simplex framework, CACM 31(1988):47-80.

[Mmicozzi 1972] E. Mmicozzi, R. Reiter, A note on linear resolution strategies in consequence-finding, Artificial Intelligence 3(1972):175-180.

[Moggi 1989] E. Moggi, Computational lambda-calculus and monads, Proc. 4th IEEE Symp. on Logic in Computer Science, 1989, pp. 14-23.

[Mogilevski 1978] G.L. Mogilevski, D.A. Ostrouhov, On a mechanical propositional calculus using Smullyan's analytic tableau, Cybernetics 14:526-529, 1978.

[Mohan 1986] C.K. Mohan, M.K. Srivas, Function definitions in term rewritign and applicative programming, Information and Control 171(3):186-271, Academic Press, New York, December 1986.

[Mohan 1987] C.K. Mohan, M.K. Srivas, D. Kapur, On proofs in system of equations and inequations, Report 87/02, Dept. of Computer Science, SUNY at Stony Brook, January 1987.

*[Mohan 1988a] C.K. Mohan, M.K. Srivas, Conditional specifications with inequational assumptions, Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems (Orsay, France, 8-10 July 1987), ed. S. Kaplan and J.-P. Jouannaud, LNCS 308, Springer-Verlag, Berlin, 1988, pp. 161-178.

*[Mohan 1988b] C.K. Mohan, Priority rewriting: semantics, confluence, and conditionals, Tech. Rep. CIS-88-6, Syracuse Univ., November 1988; also Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 278-291.

[Mohan 1988c] C.K. Mohan, Negation in equational reasoning and conditional specifications, PhD Thesis, State Univ. of New York at Stony Brook, 1988.

*[Mohan 1989] C.K. Mohan, M.K. Srivas, Negation with logical variables in condtional rewriting, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 292-310.

[Monk 1975] L.G. Monk, Elementary-recursive decision procedures, PhD thesis, Dept. of Mathematics, Univ. of California, Berkeley, 1975.

[Monk 1988] L.G. Monk, Inference rules using local contexts, J. Automated Reasoning 4(4):445-462, December 1988.

[Montague 1956] R. Montague, L. Henkin, On the definition of formal deduction, The J. of Symbolic Logic 21, 1956.

*[Montanari 1989] U. Montanari, M. Sgamma, Canonical representatives for observational equivalence classes, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 293-319.

[Moore 1973] J Strother Moore, Computational logic: Structure sharing and proof of program properties, PhD thesis, Univ. of Edinburgh, Edinburgh, 1973.

[Moore 1975a] J Strother Moore, Introducing interaction into the pure LISP theorem prover, IEEE Trans. Software Eng. 1(3):328-338, 1975.

[Moore 1975b] J Strother Moore, Computational logic: structure sharing and proof of program properties, Part II, PhD thesis Univ. of Edinburgh, DCL Memo 68, 1974; also CSL-75-2, Xerox Palo Alto Research Center, Palo Alto, CA, April 1975.

[Moore 1975c] R.C. Moore, Reasoning from incomplete knowledge in a procedural deduction system, AI-TR-347, Artificial Intelligence Lab., MIT, Cambridge, 1975.

[Moore 1979] J S. Moore, A mechanical proof of the termination of Takeuchi's function, Information Processing Letters 9(4):176-181, November 1979.

*[Moore 1989a] J S. Moore, System verification, J. Automated Reasoning 5(4):409-410, December 1989.

*[Moore 1989b] J S. Moore, A mechanically verified language implementation, J. Automated Reasoning 5(4):461-492, December 1989.

[Mora 1985] F. Mora, Grobner bases for non-commutative polynomial rings, In AAECC-3 (Grenoble, 1985), LNCS 229, Springer-Verlag, Berlin, pp. 353-362.

[Morgan 1976a] C.G. Morgan, Methods for automated theorem proving in non-classical logics, IEEE Trans. on Computers C-25(8):852-862, 1976.

[Morgan 1976b] C. Morgan, A resolution principle for a class of many-valued logics, Logique et Analyse n.s.19:311-339, 1976.

[Morgan 1986] C.G. Morgan, AUTOLOGIC at University of Victoria, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 699-700.

[Moriconi 1977] M.S. Moriconi, A system for incrementally designing and verifying programs, Certifiable Minicomputer Project, Univ. of Texas at Austin, ICSCA-CMP-9, December 1977.

[Morris 1969a] J.B. Morris, Working paper on a proofchecker for set theory, Univ. of Texas Memo, Dept. of Math., May 1969.

[Morris 1969b] J. Morris, E-resolution: Extensions of resolution to include the equality relation, Proc. 1st IJCAI (Washington, D.C.), ed. D.E. Walker and L.M. Norton, Kaufmann Inc., 1969, pp. 287-294; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 273-280.

[Morris 1977] J. Morris, B. Wegbreit, Subgoal induction, CACM 20(4):209-222, 1977.

*[Moser 1988] L.E. Moser, A decision procedure for unquantified formulas of graph theory, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 344-357.

*[Moses 1971] J. Moses, Algebraic simplification: a guide for the perplexed, Proc. 2nd Symp. on Symbolic and Algebraic Manipulation (Los Angeles, CA, March 23-25), ed. S.R. Petrick, ACM, NY, 1971, pp. 282-304; also CACM 14(8):527-537, 1971.

[Mukai 1983] K. Mukai, A unification algorithm for infinite trees, Proc. 8th Intl. Joint Conf. on Artificial Intelligence, Karlsruhe, pp. 547-549.

[Muller 1981] A. Muller, Implementation of a theorem prover based on the connection method, Bericht ATP-12-XII-81, Projekt Beweisverfahren, Institut fur Informatik, Tech. Univ. Munchen, 1981.

*[Muller 1987] J. Muller, THEOPOGLES - A theorem prover based on first-order polynomials and a special Kunth-Benedix procedure, Proc. 11th German Workshop on Artificial Intelligence (GWAI-87, Geseke, September 28-October 2, 1987), ed. K. Morik, IFB 152, Springer-Verlag, Berlin, 1987, pp. 241-250.

*[Muller 1988a] J. Muller, R. Socher-Ambrosius, Topics in completion theorem proving, SEKI Report SR-88-13, Universitat Kaiserslautern, Kaiserslautern, Germany, 1988.

*[Muller 1988b] J. Muller, R. Socher-Ambrosius, On the unnecessity of multiple overlaps in completion theorem proving, Proc. Kunstliche Intelligenz (GWAI-88, 12. Jahrestagung, Eringerfeld, 19-23 September 1988), Informatik-Fachberichte 181, ed. W. Hoeppener, Springer-Verlag, Berlin, pp. 169-178.

[Muller 1989a] J. Muller, ed., Abstracts of the 1st Workshop on Term Rewriting, Theory and Applications, SEKI Report SR-89-02, Fachbereich Informatik, Universitat Kaiserslautern, Kaiserslautern, 1989.

*[Muller 1989b] J. Muller and R. Socher-Ambrosuis, A resolution calculus extended by equivalence, Proc. 13 German Workshop on Artificial Intelligence (GWAI-89, Eringerfeld, 18-22 September 1989), ed. D. Metzing, Springer-Verlag, Berlin, 1989, pp. 102-106.

*[Muller 1990] J. Muller, F. Baader, B. Nebel, W. Nutt, G. Smolka, Reasoning and representation with concept languages (tutorial abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, p. 681.

[Mulmuley 1984] K. Mulmuley, The mechanization of existence proofs of recursive predicates, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 460-475.

[Muluszynski 1982] J. Muluszynski, J.F. Nilsson, Grammatical Unification, Information Processing Letters 15(4):150-158, October 1982.

*[Munch 1988] K.H. Munch, A new reduction rule for the connection graph proof procedure, J. Automated Reasoning 4(4):425-444, December 1988.

[Munyer 1977] J.C. Munyer, Analogy as a heuristic for mechanical theorem-proving, Collected Abstracts of the Workshop on Automatic Deduction, MIT, August 1977.

[Munyer 1981] J.C. Munyer, Analogy as a means of discovery in problem-solving and learning, PhD thesis, Univ. California, Santa Cruz, 1981.

[Murray 1978] N. Murray, A proof-procedure for non-clausal first order logic, Research Report, Univ. of Syracuse, NY, 1978.

[Murray 1979] N. Murray, Linear and almost-linear methods for the unification of first order expressions, PhD thesis, School of Comp. Sci., Syracuse Univ., 1979.

[Murray 1982a] N.V. Murray, Competely non-clausal theorem proving, Artificial Intelligence 18(1):67-85, January 1982.

[Murray 1982b] N.V. Murray, An experimental theorem prover using fast unification and vertical path ordering, Proc. 4th Natl Conf. Canadian Society of Computational Studies of Intelligence (CSCSI/SCEIO), Univ. of Saskatchewan, Saskatoon, Saskatchewan, May 1982, pp. 125-131.

[Murray 1984] N.V. Murray, E. Rosenthal, Semantic graphs, Technical Report 84-12, Dept. Computer Science, SUNY at Albany, November 1984.

*[Murray 1985a] N.V. Murray, E. Rosenthal, Path resolution and semantic graphs, Proc. European Conf. on Computer Algebra (EUROCAL '85, Linz, Austria, 1-3 April 1985), Vol. 2: Research Contributions, ed. B.F. Caviness, LNCS 204, Springer-Verlag, Berlin, pp. 50-63.

[Murray 1985b] N.V. Murray, E. Rosenthal, Path resolution with link deletion, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985, pp. 1187-1193.

[Murray 1985c] N.V. Murray, E. Rosenthal, On deleting links in semantic graphs, Proc. 3rd Intl. Conf. on Applied Algebra, Algebraic Algorithms, Symbolic Computation and Error Correcting Codes (Grenoble, France, 15-19 July 1985), LNCS 229, Springer-Verlag, pp. 404-415.

[Murray 1985d] N.V. Murray, E. Rosenthal, Inference with path resolution and semantic graphs, State Univ. of New York at Albany, 1985; also JACM 34(2):225-254, April 1987.

[Murray 1986a] N.V. Murray, E. Rosenthal, Theory links, 86-3, State Univ. of New York at Albany, Department of Computer Science, January 1986.

[Murray 1986b] N.V. Murray, E. Rosenthal, Theory links in semantic graphs, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 353-364.

[Murray 1986c] N.V. Murray, E. Rosenthal, Path Dissolution for propositional logic, 86-6, State Univ. of New York at Albany, Department of Computer Science, 1986.

*[Murray 1987a] N.V. Murray, E. Rosenthal, Path dissolution: A strongly complete rule of inference, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, pp. 161-166.

*[Murray 1987b] N.V. Murray, E. Rosenthal, Theory links: applications to automated theorem proving, J. of Symbolic Computation 4(2):173-190, October 1987.

[Murray 1987c] N.V. Murray, E. Rosenthal, Inferencing on an arbitrary set of links, Proc. 2nd Intl. Symp. on Methodologies for Intelligent Systems, Charlotte, NC, October 1987; in Methodologies for Intelligent Systems, ed. Z. Ras and M. Zemankova, North-Holland, 1987, pp. 416-423.

*[Murray 1988a] N.V. Murray, E. Rosenthal, An implementation of a dissolution-based system employing theory links, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 674-658.

[Murray 1988b] N.V. Murray, E. Rosenthal, Short proofs of pigeonhole formulas using path dissolution and semantic graphs, Tech. Report, Dept. of Computer Science, SUNY at Albany, 1988.

*[Murray 1989] N.V. Murray, E. Rosenthal, Improving tableau proofs, Proc. 4th Methodologies for Intelligent Systems (12-14 October 1989, Charlotte, North Carolina), ed. Z.W. Ras, Elsevier Science Publishing Co., NY, NY, 1989, pp. 477-484.

*[Murray 1990a] N.V. Murray, E. Rosenthal, DISSOLVER: A dissolution-based theorem prover (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 665-666.

*[Murray 1990b] N.V. Murray, E. Rosenthal, Reexamining intractability of tableau methods, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, p. 52-59.

*[Murthy 1990] C.R. Murthy, J.R. Russell, A constructive proof of Higman's lemma, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 257-267.

[Musser 1978] D.R. Musser, A data type verification system based on rewrite rules, USC Information Sciences Institute, CA, June 20 1978; also 6th Texas Conf. on Computing Systems, Austin, Texas, November 1978.

[Musser 1980] D.R. Musser, On proving inductive properties of abstract data types, Report, USC Information Sciences Institute, 1980; also Proc. 7th ACM Symp. on Principles of Programming Languages, Las Vegas, NA, January 1980, pp. 154-162.

[Musser 1982] D.R. Musser, D. Kapur, Rewrite rule theory and abstract data type analysis, Proc. Computer Algebra, EUROSAM 1982 (April 1982), ed. J. Calmet, LNCS 144, Springer-Verlag, pp. 78-90.

[Musser 1984] D.R. Musser, The L programming language preliminary reference manual, Proc. of an NSF Workshop on the Rewrite Rule Laboratory (September 1983), ed. J.V. Guttag, D. Kapur, and D.R. Musser, General Electric, Information Systems Laboratory, Schenectady, NY, No. 84GEN008, April 1984, pp. 57-72.

[Musser 1985] D. Musser, Aids to hierarchical specification and reusing theorems in Affirm-85, Software Engineering News, August 1985.

*[Musser 1989] D.R. Musser, Automated theorem proving for analysis and synthesis, In Current Trends in Hardware Verification and Automated Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, NY, 1989, pp. 440-464.

*[Myers 1990] K.L. Myers, Automatically generating universal attachments through compilation, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 252-257.

[Mzali 1986] J. Mzali, Matching with distributivity, Proc. 8th Intl. Conf. on Automated Deduction (CADE-8, Oxford, England, July 27-August 1, 1986), ed. J.H. Siekmann, LNCS 230, Springer-Verlag, Berlin, 1986, pp. 496-505.

[Nagle 1982] J. Nagle, S. Johnson, Practical program verification, Automatic program proving for real-time embedded software, WDL-TR9859, Ford Aerospace and Communications Corporation, December 1982.

[Nakajima 1983] R. Nakajima, T. Yuasa, The IOTA Programming System, LNCS 160, Springer-Verlag, NY, 1983.

[Nakanishi 1975] M. Nakanishi, M. Nagata, Y. Iwamara, Gentzen-type formal system representing properties of function and its implementation, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975, pp. 57-64.

[Nakanishi 1979] M. Nakanishi, M. Nagata, K. Ueda, An automatic theorem prover generating a proof in natural language, Proc. 6th IJCAI, Tokyo, August 1979, pp. 636-638.

*[Naoi 1989] T. Naoi, Y. Inagaki, Algebraic semantics and complexity of term rewriting systems, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 311-325.

[Naqvi 1980] S.A. Nauvi, L.J. Henschen, Performing inferences over recursive data bases, Proc. 1st Natl Conf. on Artificial Intelligence, Stanford, CA, 1980, pp. 263-265.

[Narain 1985] S. Narain, A technique for doing lazy evaluation in logic, Proc. 1985 Symp. on Logic Programming, IEEE Society Press, 1985, pp. 261-269.

*[Narain 1989] S. Narain, Optimization by non-deterministic, lazy rewriting, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 326-342.

[Narendran 1984a] P. Narendran, R. Menanghton, The undecidability of the preperfectness of Thue systems, North-Holland, Theoretical Computer Science 31(1984):165-174.

[Narendran 1984b] P. Narendran, Church-Rosser and related Thue systems, Doctoral Dissertation, Rensselar Polytechnic Institute, Troy, NY, 1984.

[Narendran 1988] P. Narendran, J. Stillman, Hardware verification in the interactive VHDL workstation, in VLSI Specification, Verification and Synthesis, ed. Birtwistle and Subrahmanyam, Kluwer Academic Publishers, 1988, pp. 217-235.

*[Narendran 1990] P. Narendran, F. Otto, Some results on equational unification, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 276-291.

*[Naughton 1989] J.F. Naughton, Y. Sagiv, Minimizing expansions of recursions, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 321-349.

[Navarro 1984] M. Navarro, F. Orejas, On the equivalence of hierarchical and non-hierarchical rewriting on conditional term rewriting systems, EUROSAM '84, Oxford.

[Nederpelt 1970] R.P. Nederpelt, AUTOMATH, A Language for Checking Mathematics with a Computer, Report, Tech. Hochschule Eindhoven, 1970.

[Nederpelt 1980a] R.P. Nederpelt, An approach to theorem proving on the basis of a types lambda-calculus, Proc. 5th Conf. on Automated Deduction (Les Arcs, France), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 182-194.

[Nederpelt 1980b] R.P. Nederpelt, A system of natural reasoning based on a typed lambda-calculus, Bull. Eur. Assoc. Theoret. Comp. Sci. 11(1980): 130-131.

[Negrete 1991] S. Negrete, Proof plans with hints, Master's thesis, Dept. of Artificial Intelligence, Edinburgh, 1991.

[Nelson 1978] G. Nelson, D.C. Oppen, A simplifier based on efficient decision algorithms, Proc. 5th ACM Symp. on Principles of Programming Languages, 1978, pp. 141-150.

[Nelson 1979] G. Nelson, D.C. Oppen, Simplification by cooperating decision procedures, ACM Trans. on Programming Languages and Systems 1(2):245-257, October 1979.

[Nelson 1980] G. Nelson, D.C. Oppen, Fast decision procedures based on congruence closure, STAN-CS-77-646, Stanford U,; also JACM 27(2):356-364, April 1980.

[Nelson 1981] G. Nelson, Techniques for program verification, Xerox Palo Alto Research Center, CA, CSL-81-10, June 1981.

[Nelson 1983] G. Nelson, Verifying reachability invariants of linked structures, Proc. 10th Principles of Programming Languages, Austin, Texas, 1983, pp. 38-47.

[Nevin 1972] A.J. Nevins, A human oriented logic for automatic theorem-proving, Mass. Inst. of Tech., Cambridge, MA, AI Memo No. 268, 1972; also JACM 21(4):606-621, October 1974.

[Nevins 1975a] A.J. Nevins, Plane geometry theorem proving using forward chaining, Artificial Intelligence 6(1):1-23, Spring 1975.

[Nevins 1975b] A.J. Nevins, A relaxation approach to splitting in an automated theorem prover, Artificial Intelligence 6(2):25-39, 1975.

[Newborn 1989] M. Newborn, The great theorem prover, Newborn Software, Westmount, Quebec, 1989.

[Newell 1956a] A. Newell, H.A. Simon, The logic theory machine: A complex information processing system, Computer Science Dept., Carnegie-Mellon Univ., July 1956.

[Newell 1956b] A. Newell, J.C. Shaw, H.A. Simon, The logic theory machine, IRE Trans. Information Theory IT-2(3):61-79, 1956; also Computers and Thought, McGraw-Hill, 1963.

[Newell 1957a] A. Newell, J.C. Shaw, Programming the logic theory machine, Computer Science Dept., Carnegie-Mellon Univ., February 1957.

[Newell 1957b] A. Newell, J.C. Shaw, H.A. Simon, Empirical explorations with the logic theory machine: A case study in heuristics, Computer Science Dept., Carnegie-Mellon Univ., March 1957.

[Newell 1957c] A. Newell, J.C. Shaw, H.A. Simon, Note: Improvement in the proof of a theorem in the elementary propositional calculus, Computer Science Dept., Carnegie-Mellon Univ., March 1957.

[Newell 1958] A. Newell, J.C. Shaw, H.A. Simon, A report on a general problem-solving program (GPS-1), Rand Corp. Memo P-1584, December 1958.

[Newell 1959] A. Newell, J.C. Shaw, H.A. Simon, A variety of intelligent learning in a general problem solver, Computer Science Dept., Carnegie-Mellon Univ., July 1959.

[Newell 1960] A. Newell, J.C. Shaw, H.A. Simon, Comment: Toward mechanical mathematics, Computer Science Dept., Carnegie-Mellon Univ., February 1960.

[Newell 1961] A. Newell, J.C. Shaw, H.A. Simon, A program that simulates human thought, Computer Science Dept., Carnegie-Mellon Univ., April 1961.

[Newell 1963] A. Newell, A guide to the general problem solver program GPS-2-2, Computer Science Dept., Carnegie-Mellon Univ., February 1963.

[Newell 1963a] A. Newell, H. Simon, GPS a program that simulates human thought, in Computers and Thought, ed. Feigenbaum and Feldman, McGraw-Hill, NY, 1963, pp. 279-296.

[Newell 1963b] A. Newell, J. Shaw, H. Simon, Empirical explorations with the logic theory machine, in Computers and Thought, ed. Feigenbaum and Feldman, McGraw-Hill, NY, 1963, pp. 109-133; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 49-73.

[Newell 1965] A. Newell, G. Ernst, The Search for Generality, Proc. IFIP Congress 1965, Vol. 1, Spartan Books, Washington, D.C., 1965, pp. 17-24.

[Newell 1967] A. Newell, A general problem-solving program, Computer Science Dept., Carnegie-Mellon Univ., June 1967.

[Newman 1942] M.H.A. Newman, On theories with a combinatorial definition of equivalence, Annals of Math. 43(2):223-243. 1942.

*[Ngair 1993] T.-H. Ngair, A new algorithm for incremental prime implicate generation, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 46-51.

[Nie 1989a] Xumin Nie, and D.A. Plaisted, Refinements to depth-first iterative-deepening search in automatic theorem proving, Artificial Intelligence 41(1989/90):223-235.

[Nie 1989b] X. Nie, Implementation technique in automatic theorem proving, PhD thesis, Univ. of North Carolina at Chapel Hill, 1989.

*[Nie 1990] Xumin Nie, and D.A. Plaisted, A complete semantic back chaining proof system, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 16-27.

*[Nie 1992] X. Nie, and D.A. Plaisted, A semantic backward chaining proof system, Artificial Intelligence 55(1):109-128, May 1992.

*[Nieuwenhuis 1990] R. Nieuwenhuis, R. Orejas, A. Rubio, TRIP: An implementation of clausal rewriting (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 667-668.

*[Nieuwenhuis 1992] R. Nieuwenhuis, A. Rubio, Theorem proving with ordering constrained clauses, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 477-491.

*[Niemela 1988] I. Niemela, Decision procedure for autoepistemic logic, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 675-684.

[Nilsson 1969] N.J. Nilsson, Predicate Calculus Theorem Proving, Stanford Research Inst., Menlo Park, CA, 1969.

[Nilsson 1971] N. Nilsson, Problem Solving Methods in Artificial Intelligence, McGraw-Hill, NY, 1971.

[Nilsson 1977] N.J. Nilsson, A production system for automatic deduction, Tech. Note 148, SRI International, Menlo Park, CA, July 1977; also Machine Intelligence 9, ed. Hayes, Michie, and Mikulich, Ellis Harwood Ltd., Chichester, 1979, 101-128.

[Nilsson 1980] N.J. Nilsson, Principles of Artificial Intelligence, Tioga Publishing Co., Palo Alto, CA, 1980.

[Nilsson 1981] N.J. Nilsson, B.L. Webber, eds., Readings in Artificial Intelligence, Tioga Publishing Co., Palo Alto, CA, 1981.

[Nilsson 1984] M. Nilsson, The world's shortest Prolog interpreter? in Implementations of Prolog, ed. J.A. Campbell, Ellis Horwood, Chishester, England, 1984, pp. 87-92.

*[Nilsson 1989] J.F. Nilsson, A case study in knowledge representation and reasoning with higher-order combinators, Proc. Scandinavian Conf. on Artificial Intelligence -- 89 (SCAI '89, Tapere, Finland, 13-15 June 1989), ed. H. Haakkola and S. Linnainmaa, IOS, Amsterdam, Netherlands, 1989, pp. 37-48.

*[Nipkow 1989a] T. Nipkow, Combining matching algorithms: The regular case, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 343-358.

[Nipkow 1989b] T. Nipkow, Proof transformations for equational theories, Tech. report 181, Univ. of Cambridge, Computer Laboratory, September 1989; also in LICS 90.

[Nipkow 1989c] T. Nipkow, Proof transformations for some simple equational theories, extended abstract, Proc. UNIF'89, 3rd Intl. Workshop on Unification, ed. H.-J. Burckert and W. Nutt,Lambrecht (FR Germany), June 1989.

[Nipkow 1989d] T. Nipkow, Equational reasoning in Isabelle, Science of Computer Programming 12(1989): 123-149.

[Nipkow 1989e] T. Nipkow, Term rewriting and beyond - theorem proving in Isabelle, Formal Aspects of Computer 1(1989): 320-338.

*[Nipkow 1990a] T. Nipkow, Proof transformations for equational theories, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 278-288.

[Nipkow 1990b] T. Nipkow, Unification in primal algebras, their powers and their varieties, JACM 37(4):742-776, October 1990.

*[Nipkow 1991a] T. Nipkow, Higher-order critical pairs, Proc. 6th Annual IEEE Symp. on Logic in Computer Science (Amsterdam, The Netherlands, 15-18 July 1991), IEEE Computer Society Press, Los Alamitos, CA, 1991, pp. 342-349.

*[Nipkow 1991b] T. Nipkow, Constructive rewriting, The Computer Journal 34(1):34-41, February 1991.

*[Nipkow 1992a] T. Nipkow, Z. Qian, Reduction and unification in lambda calculi with subtypes, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 66-78.

*[Nipkow 1992b] T. Nipkow, L.C. Paulson, Isabelle-91, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 673-676.

[Nipkow 1993] T. Nipkow, Orthogonal higher-order rewrite systems are confluent, To appear in Proc. Int. Conf. Typed Lambda Calculi and Applications, LNCS, 1993.

[Nishimura 1975] T. Nishimura, M. Nakanishi, M. Nagata, Y. Iwamaru, Gentzen-type formal systems representing properties of function and its implementation, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975.

*[Nivat 1989] M. Nivat, A. Podelski, Tree monoids and recognizability of sets of finite trees, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 351-367.

[Noel 1989] P.A.J. Noel, Experimenting with Isabelle in ZF set theory, Tech. Report 177, Computer Laboratory, Univ. of Cambridge, September 1989.

[Noll 1980] H. Noll, A note on resolution: How to get rid of factoring without losing completeness, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 250-263.

*[Nonnengart 1993] A. Nonnengart, First-order modal logic theorem proving and functional simulation, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 80-87.

[Nordstrom 1981] B. Nordstrom, Programming in constructive set theory: Some examples, ACM Conf. on Functional Programming Languages and Computer Architecture, Portsmouth, NH, 1981, pp. 141-153.

[Norton 1966] L.M. Norton, ADEPT - A heuristic program for proving theorems of group theory, PhD thesis, MIT, Boston, Report MAC-TR-33, Project Mac, MIT, September 1966, 176pp.

[Norton 1971] L.M. Norton, Experiments with a heuristic theorem-proving for the predicate calculus with equality, Artificial Intelligence 2(3):261-284, 1971.

[Norton 1972] L.M. Norton, Heuristic programming and theorem proving, Trans. Am. Nucl. Soc. 15(2):777-778, November 1972.

*[Norvig 1991] P. Norvig, Correcting a widespread error in unification algorithms, Software -- Practice and Experience 2(2):231-233, February 1991.

[Nossum 1982] R. Nossum, Algebraic simplification in the prover system, Report 67, Inst. of Informatics, Univ. of Oslo, April 1982.

[Nossum 1983] R. Nossum, A proof technique based on simplification, Univ. of Oslo, Research Report 76, 1983.

[Nossum 1984] R. Nossum, Decision algorithms for program verification, Institute of Informatics, Univ. of Oslo, 1984.

[Nossum 1985] R. Nossum, Automated theorem proving methods, BIT 25(1985):51-64.

[Novikov 1958] P.S. Novikov, On the algorithmic unsolvability of the word problem in group theory, Amer. Math. Soc. Translation Series 2, vol. 9(1958):1-122.

*[Nutt 1987] W. Nutt, P. Rety, G. Smolka, Basic narrowing revisited, SEKI Report SR-87-07, Universitat Kaiserslautern, West Germany, July 1987.

[Nutt 1989] W. Nutt, The unification hierarchy is undecidable, SEKI Report SR-89-06, Universitat Kaiserslautern, 1989.

*[Nutt 1990] W. Nutt, Unification in monoidal theories, Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 618-632.

*[Nutt 1991] W. Nutt, The unification heirarchy is undecidable, J. Automated Reasoning 7(3):369-381, September 1991.


URL: http://www.oracanada.com/biblio/biblio-prover-m-n.html
Revised: July 31, 1998