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, 2025 August 1989), ed. N.S. Sridharan, IJCAI Inc.,
1989, pp. 413418.
*[Madden 1992] P. Madden, Automatic program optimization through
proof transformation, Proc. 11th Intl. Conf. on Automated
Deduction (CADE11, Saratoga Springs, NY, USA, June 1992), ed. D.
Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 446460.
[Madlener 1987] K. Madlener, F. Otto, Groups presented by
certain classes of finite lengthreducing string rewriting
systems, Proc. 2nd Intl. Conf. on Rewriting Techniques and
Applications (Bordeaux, France, 2527 May 1987), ed. P. Lescanne,
LNCS 256, SpringerVerlag, Berlin, 1987, pp. 133144.
*[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, 24 November 1987, pp. 567567.
*[Malkin 1988] P.K. Malkin, E.P. Martin, Logical matrix
generation and testing, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
685693; 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,
Unificationfree execution of Horn clause programs, Proc. 2nd
Logic Symp., pp. 7886, 1985.
[Manna 1977] Z. Manna, R.J. Waldinger, Studies in Automatic
Programming Logic, NorthHolland, 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):90121.
[Manna 1981] Z. Manna, R.J. Waldinger, Deductive synthesis of
the unification algorithm, Science of Computer Programming
1(1981):548.
[Manna 1985a] Z. Manna, R. Waldinger, Special relations in
automated deduction, CS Report STANCS851051, Stanford Univ.,
1985; also Proc. 12th Colloquium Automata, Language and
Programming (Natplion, Greece, July 1985), ed. W. Brauer, LNCS
194, SpringerVerlag, Berlin, 1985, pp. 413423; also JACM
33(1):159, January 1986.
[Manna 1985b] Z. Manna, R. Waldinger, The logical basis for
computer programming, Vol. 1: Deductive reasoning, AddisonWesley,
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 (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 622640.
[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, SpringerVerlag, Berlin, 1985, pp.
212224.
[Manna 1987] Z. Manna, R. Waldinger, How to clear a block: A
theory of plans, J. of Automated Reasoning 3(4):343377, December
1987.
*[Manna 1992] Z. Manna, R. Waldinger, The specialrelation rules
are incomplete, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 492506.
*[Manna 1993] Z. Manna, R. Waldinger, The Deductive Foundations
of Computer Programming, AddisonWesley, 1993.
*[Manthey 1987] R. Manthey, F. Bry, A hyperresolutionbased
proof procedure and its implemention in PROLOG, Proc. 11th German
Workshop on Artificial Intelligence (GWAI87, Geseke, September
28October 2, 1987), ed. K. Morik, SpringerVerlag, Berlin, 1987,
pp. 221230.
*[Manthey 1988] R. Manthey, F. Bry, SATCHMO: A theorem prover
implemented in Prolog, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
415434.
*[Marcus 1988] L. Marcus, T. Redmond, Two automated methods in
implementation proofs, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
622542.
*[Marcus 1996a] L. Marcus, The Incorporation of Testing into
Formal Verification: Direct, Modular, and Hierarchical Correctness
Degrees, Formal Methods in System Design 9(3), 235262 (1996).
(source: Leo Marcus)
*[Marcus 1996b] L. Marcus, Syntactic and Semantic Dependence of
ArrayArithmetic Sentences, with an Application to Program
Verification, Fundamenta Informaticae 27, 77100 (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. 257271.
[Markov 1951] A. Markov, Impossibility of algorithms for
recognizing some properties of associative systems, Dokl. Ada.
Nauk SSSR 77(1951):953956.
[Martelli 1976] A. Martelli, U. Montanari, Unification in linear
time and space: A structured presentation, Nota interna B7616,
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):258282, 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, NorthHolland, 1984, pp.
202209.
*[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, 2225 September 1986),
pp. 180186.
*[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. AitKaci, M. Nivat, Academic Press, Inc., San
Diego, 1989, pp. 245274.
*[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. 5975.
*[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 2325), ed.
S.R. Petrick, ACM, NY, 1971, 305310; also JACM 18(4):549558,
1971.
[Martin 1986a] U. Martin, Doing algebra with REVE, UMCS86104,
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,
UMCS86112, 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 (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 506513.
[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, 2527 May 1987), ed. P. Lescanne,
LNCS 256, SpringerVerlag, Berlin, 1987, pp. 4253.
*[Martin 1988] U. Martin, T. Nipkow, Unification in Boolean
rings, J. Automated Reasoning 4(4):381396 , 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 (CADE10,
Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial
Intelligence 449, ed. M.E. Stickel, SpringerVerlag, Berlin, 1990,
pp. 366380.
[MartinLof 1970] P. MartinLof, Notes on Constructive
Mathematics, Almqvist & Wiksell, Stockhom, 1970.
[MartinLof 1984] P. MartinLof, 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):1720.
[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):295297, 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):12821285.
[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):2225; also
Automation Of Reasoning  Classical Papers On Computational Logic,
Vol. II, 19671970, ed. J. Siekmann And G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 4854.
[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):137146.
[Maslov 1969b] S. Yu Maslov, Invertible sequential variant of
constructive predicate calculus, Seminar in Mathematics 4, V.A.
Steklov Mathem. Institute, Leningrad, Consultants Bureau,
NYLondon, 1969, pp. 3642.
[Maslov 1971a] S. Maslov, Proofsearch strategies for methods of
the resolution type, Machine Intelligence 6, ed. B. Meltzer and D.
Michie, American Elsevier, NY, 1971, pp. 7789.
[Maslov 1971b] S. Yu Maslov, Deductionsearch 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, NYLondon, 1971, pp. 6468.
[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,
NYLondon, 1971, pp. 6973; also Automation Of Reasoning 
Classical Papers On Computational Logic, Vol. II, 19671970, ed.
J. Siekmann And G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
264272.
[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, 19571966, ed. J. Siekmann and G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 424483, pp. 2938.
[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):4049,
USSR, July 1978.
[Matulis 1963] V.A. Matulis, Variants of the Classical Predicate
Calculus with Unique Deduction Tree, Soviet Math. Dokl.
148(4):768770, 1963.
[Matwin 1985] S. Matwin, T. Pietrzykowski, Intelligent
backtracking in planbased deduction, IEEE Trans. on Pattern
Analysis and Machine Intelligence PAMI7(6):682692, November
1985.
[Mayfield 1988] B. Mayfield, The role of term symmetry in
equational unification and completion procedures, PhD
dissertation, Univ. of MissouriRolla, Rolla, MO, 1988.
[Mazaud 1987] M. Mazaud, R. Rakotozafy, A.
SzumachowskiDespland, Code generator generation based on
templatedriven target term rewriting, Proc. 2nd Intl. Conf. on
Rewriting Techniques and Applications (Bordeaux, France, 2527 May
1987), ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987,
pp. 105120.
[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. 10241026, 1981.
[McAllester 1982] D.A. McAllester, Reasoning utility package
user's manual, Version one, AI Lab. MIT, AIM667, April 1982; also
available on microfilm as N0001475C0643, 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 (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 742743.
[McAllester 1991a] D. McAllester, Grammar Rewriting, AIM1342,
MIT AI Lab., December 1991.
[McAllester 1991b] D. McAllester, J. Siskind, Lifting
transformations, AIM1343, MIT AI Lab., December 1991.
[McAllester 1991c] D. McAllester, Tractable inference relations,
AIM1344, MIT AI Lab., December 1991.
*[McAllester 1992] D. McAllester, Grammar rewriting, Proc. 11th
Intl. Conf. on Automated Deduction (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 124138.
[McCarthy 1960] J. McCarthy, Recursive functions of symbolic
expressions and their computations by machine, Part I, CACM 3(4),
1960, 184195.
[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. 219227.
[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. 410417.
[McCarthy 1963b] J. McCarthy, A basis for a mathematical theory
of computation, in Computer Programming and Formal Systems, ed. P.
Brafford and D. Hirschberg, NorthHolland, Amsterdam, 1963, pp.
3370.
[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. 403418.
[McCarthy 1969] J. McCarthy, Recursive functions of symbolic
expressions and their computations by machine, Part I, CACM
3(1969):184195.
[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
LRPTR18, 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):116.
[McCharen 1976b] J. McCharen, R. Overbeek, L. Wos, Problems and
experiments for and with automated theorem proving programs, IEEE
Trans. on Computers C25(8):773782, 1976.
[McCune 1981] W.W. McCune, An inference mechanism for
resolutionstyle theorem provers, M.A. thesis, Northwestern Univ.,
1981.
[McCune 1982] W. McCune, User guide for the Northwestern
University Theoremproving 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. 902908.
[McCune 1985] W.W. McCune, L.J. Henschen, Experiments with
semantic paramodulation, J. of Automated Reasoning 1(3):231261,
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):91107, March 1987.
[McCune 1987] W. McCune, Unskolemizing clause sets, Tech. Memo
ANL/MCSTM93, Argonne National Laboratory, 1987; also Information
Processing Letters 29(November 1988):257263.
*[McCune 1988] W. McCune, Challenge equality problems in lattice
theory, Proc. 9th Intl. Conf. on Automated Deduction (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 704709.
[McCune 1989] W. McCune, Otter 1.0 users' guide, Tech. Report
ANL8844, Argonne National Laboratory, Argonne, IL, January 1989.
[McCune 1990a] W. McCune, OTTER 2.0 users guide, Tech. Report
ANL90/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 (CADE10, Kaiserslautern, FRG,
July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 663664.
*[McCune 1990c] W. McCune, Skolem functions and equality in
automated deduction, Proc. 8th National Conf. on Artificial
Intelligence (AAAI90, July 29August 3, 1990), AAAI Press/MIT
Press, 1990, pp. 246251.
[McCune 1990d] W. McCune, Experiments with discrimination tree
indexing and path indexing for term retrieval, MCS Preprint
P1911190, 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 (CADE11, Saratoga Springs, NY, USA, June
1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 209223.
*[McCune 1996] W. McCune and R. Padmanabhan Automated Deduction
in Equational Logic and Cubic Curves Lecture Notes in AI, #1095,
LN in CS, SpringerVerlag, 1996.
(source: Dr. R. Padmanabhan) [McDermott 1979] J. McDermott,
Learning to use analogies, IJCAI79, 1979, pp. 568576.
*[McDermott 1987] D.V. McDermott, Logic, problem solving, and
deduction, Annual Review of Computer Science, Vol. 2, 1987. pp.
187229. [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. 89118, pp. 315360.
[McGovern 1984] G.J. McGovern, Automatic theoremproving for
some nonclassical 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.
368374.
[McKinsey 1943] J.C.C. McKinsey, The decision problem for some
classes of sentences without quantifiers, J. Symb. Logic
8(3):6176, 1943.
*[McMichael 1990] A.F. McMichael, ALIM: An automated reasoner
for equivalences, applied to set theory, Proc. 10th Intl. Conf. on
Automated Deduction (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 308321.
[McNulty 1976a] G. McNulty, The decision problem for equational
bases of algebras, Annals of Mathematical Logic 10(1976):193259.
[McNulty 1976b] G. McNulty, Undecidable properties of finite
sets of equations, JSL 41(3):180186, 1976.
*[McNulty 1989] G.F. McNulty, An equational logic sampler, Proc.
3rd Intl. Conf. Rewriting Techniques and Applications (Chapel
Hill, North Carolina, 35 April 1989), ed. N. Dershowitz,
SpringerVerlag, NY, 1989, pp. 234262.
[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:187200, 1979.
[McRobbie 1980] M.A. McRobbie, R.K. Meyer, P.B. Thistlewaite, A
mechanized decision procedure for nonclassical logic: The program
KRIPKE, Bulletin of the Section of Logic, Polish Academy of
Sciences, 9(1980):189192; Abstract, J. of Symbolic Logic
47(1982):717.
[McRobbie 1982] M.A. McRobbie, R.K. Meyer, P.B. Thistlewaite,
Computeraided investigations into the decision problem for
relevant logics: The search for a free associative connective,
Australian Computer Science Communications 5(1982):236267; 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 firstorder relevant orthologics, Bulletin
of the Section of Logic, Polish Academy of the Sciences
13:233240, 1984.
*[McRobbie 1987] M.A. McRobbie, Towards efficient
knowledgebased automated theorem proving for nonstandard logics,
SEKI Report SR8712, Universitat Kaiserslautern, 1987; also with
R.K. Meyer and P.B. Thistlewaite, in Proc. 9th Intl. Conf. on
Automated Deduction (CADE9, Argonne, Ilinois, May 1988), ed. E.
Lusk and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
197217.
*[McRobbie 1988] M.A. McRobbie, R.K. Meyer, P.B. Thistlewaite,
Towards efficient ``knowledgebased'' automated theorem proving
for nonstandard logics, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
197217.
*[McRobbie 1991] M.A. McRobbie, Automated reasoning and
nonclassical logics: Introduction, J. Automated Reasoning
7(4):447451, 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. 6379.
*[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, SpringerVerlag, NY, 1989, pp. 341386.
[Melle 1981] W.J. van Melle, System Aids in Constructing
Consultation Programs, UMI Research Press, Ann Arbor, Michigan,
1981.
[Meltzer 1965] B. Meltzer, Theoremproving 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):341343,
January 1966; also Automation of Reasoning  Classical Papers on
Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 493495.
[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):583595, 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. 6370.
[Meltzer 1968b] B. Meltzer, Some notes on resolution strategies,
Machine Intelligence 3, ed. Michie, American Elsevier, NY, 1968,
pp. 7176.
[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. 377382.
[Meltzer 1969] B. Meltzer, The use of symbolic logic in proving
mathematical theorems by means of a digital computer, Foundations
of Maths. pp. 3944, Springer, NY, 1969.
[Meltzer 1970b] B. Meltzer, Power amplification for
theoremprovers, Machine Intelligence 5, ed. B. Meltzer and D.
Michie, American Elsevier, NY, 1970, pp. 165179.
[Meltzer 1970c] B. Meltzer, The semantics of induction and the
possibility of complete systems of inductive inference, Artificial
Intelligence 1(3):189192, 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. 1533; also Department of Computational Logic Memo
DCL37, University of Edinburgh, 1971.
[Meltzer 1973a] B. Meltzer, The impossibility of perfect proof
procedures, AISB European Newsletter 15(November 1973):2829.
[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
manysorted rewrite rules, Report CSLI8542, Center for the Sutdy
of Language and Information, Stanford Univ., CA, 1985.
[Meseguer 1987] J. Meseguer, J. Goguen, G. Smolka, Ordersorted
unification, Report CSLI8786, Centre for the Study of Language
and Information, Stanford Univ., CA, March 1987.
[Metivier 1983] Y. Metivier, About the rewriting systems
produced by the KnuthBendix completion algorithm, Information
Processing Letters 16(1):3134, 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):597630, December 1991.
[Michalski 1973] R.S. Michalski, Discovering classification
rules using variablevalued logic system VL1, Proc. 3rd IJCAI,
Stanford Univ., Stanford, August 1973, pp. 162172.
[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):1922.
[Michie 1970] D. Michie, Notes on GDeduction, Memo MIPR93,
Univ. of Edinburgh, Edinburgh, 1970.
[Michie 1972] D. Michie, R. Ross, G.J. Shannan, Gdeduction,
Machine Intelligence 7, ed. B. Meltzer and D. Michie, Edinburgh
Univ. Press, 1972, pp. 141165.
*[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, 58
June 1989), IEEE, 1989, pp. 396401.
*[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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 263277.
[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, SpringerVerlag, Berlin, 1982, pp. 5069.
[Miller 1983] D.A. Miller, Proofs in higherorder logic, PhD
thesis, CarnegieMellon Univ., October 1983, available as Tech.
Report MSCIS8337, 1983.
[Miller 1984] D. Miller, Expansion tree proofs and their
conversion to natural deduction proofs, MSCIS846, Univ. of
Pennsylvania, February 1984; also Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 375393.
[Miller 1986] D. Miller, A. Felty, An integration of resolution
and natural deduction theorem proving, MSCIS8647, Univ. of
Pennsylvania, 1986; also in Proc. AAAI86, 5th Natl. Conf. on
Artificial Intelligence, ed. T. Kehler, S. Rosenschein, R. Filman,
and P.F. PatelSchneider, Philadelphia, PA, 1115 August 1986, pp.
198202.
[Miller 1987a] M. Miller, D. Perlis, Proving selfutterances, J.
of Automated Reasoning 3(3):329338, 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.
98105.
[Miller 1987c] D.A. Miller, A compact representation of proofs,
Studia Logica 46(4):347370, 1987. *[Miller 1988] S.A. Miller,
L.K. Schubert, Using specialists to accelerate general reasoning,
Proc. AAAI88, 7th National Conf. on Artificial Intelligence, Vol.
1, (St. Paul, Minnesota, 2126 August 1988), pp. 161165.
[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):111122.
[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. 5170.
[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
CSR15783, 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:411422, 1984;
also in Mathematical Logic and Programming Languages, ed. C.A.R.
Hoare and J.C. Shepherdson, PrenticeHall, 1985, pp. 7788.
*[Milner 1987] R. Milner, Dialogue with a proof system, Proc.
Intl. Joint Conf. on Theory and Practice of Software Development
(TAPSOFT'87, Pisa, Italy, 2327 March 1987), Vol. I, ed. H. Ehrig,
R. Kowalski, G. Levi, and U. Montanari, LNCS 249, SpringerVerlag,
Berlin, 1987, pp. 271275.
[Minicozzi 1972] E. Minicozzi, R. Reiter, A note on linear
resolution strategies in consequencefinding, Artificial
Intelligence 3(1972):175180.
[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. 3137.
[Minker 1973b] J. Minker, D.H. Fishman, J.R. McSkimin, MRPPS 
An interactive refutation proof procedure system for
questionanswering, TR228, 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.
TR736, February 1979.
[Minker 1982] J. Minker, G. Zanon, An extension to linear
resolution with selection function, Information Processing Letters
14(4):191194, Netherlands, June 1982.
[Minker 1983] J. Minker, J. Nicolas, On recursive axioms in
deductive databases, Information systems 8(1):113, 1983.
[Minker 1984] J. Minker, D. Perlis, Applications of protected
circumscription, Proc. 7th Intl. Conf. on Automated Deduction
(CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170,
SpringerVerlag, NY, 1984, pp. 414425.
*[Minker 1988] J. Minker, A. Rajasekar, Procedural
interpretation of nonHorn logic programs, Proc. 9th Intl. Conf.
on Automated Deduction (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 278293.
[Minksy 1956] M. Minsky, Notes on the Geometry Problem,
AIProject, 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,
NYLondon, 1969, pp. 5259.
*[Mints 1991] G. Mints, T. Tammet, Condensed detachment is
complete for relevance logic: A computeraided proof, J. Automated
Reasoning 7(4):587596, December 1991.
[Miranker 1987a] D.P. Miranker, TREAT: A new and efficient match
algorithm for AI production systems, TR8703, 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, 1317 July 1987, pp.
4247.
*[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
(AAAI90, July 29August 3, 1990, 1990), Vol. 2, AAAI Press/The
MIT Press, Menlo Park/Cambridge, pp. 685692.
[Mitra 1988] G. Mitra, M. Tamiz, J. Yadegar, Experimental
investigation of an interior search method within a simplex
framework, CACM 31(1988):4780.
[Mmicozzi 1972] E. Mmicozzi, R. Reiter, A note on linear
resolution strategies in consequencefinding, Artificial
Intelligence 3(1972):175180.
[Moggi 1989] E. Moggi, Computational lambdacalculus and monads,
Proc. 4th IEEE Symp. on Logic in Computer Science, 1989, pp.
1423.
[Mogilevski 1978] G.L. Mogilevski, D.A. Ostrouhov, On a
mechanical propositional calculus using Smullyan's analytic
tableau, Cybernetics 14:526529, 1978.
[Mohan 1986] C.K. Mohan, M.K. Srivas, Function definitions in
term rewritign and applicative programming, Information and
Control 171(3):186271, 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,
810 July 1987), ed. S. Kaplan and J.P. Jouannaud, LNCS 308,
SpringerVerlag, Berlin, 1988, pp. 161178.
*[Mohan 1988b] C.K. Mohan, Priority rewriting: semantics,
confluence, and conditionals, Tech. Rep. CIS886, Syracuse Univ.,
November 1988; also Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 278291.
[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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
292310.
[Monk 1975] L.G. Monk, Elementaryrecursive 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):445462, 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. AitKaci, M. Nivat, Academic Press, Inc., San
Diego, 1989, pp. 293319.
[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):328338,
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 CSL752, Xerox Palo Alto
Research Center, Palo Alto, CA, April 1975.
[Moore 1975c] R.C. Moore, Reasoning from incomplete knowledge in
a procedural deduction system, AITR347, 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):176181, November 1979.
*[Moore 1989a] J S. Moore, System verification, J. Automated
Reasoning 5(4):409410, December 1989.
*[Moore 1989b] J S. Moore, A mechanically verified language
implementation, J. Automated Reasoning 5(4):461492, December
1989.
[Mora 1985] F. Mora, Grobner bases for noncommutative
polynomial rings, In AAECC3 (Grenoble, 1985), LNCS 229,
SpringerVerlag, Berlin, pp. 353362.
[Morgan 1976a] C.G. Morgan, Methods for automated theorem
proving in nonclassical logics, IEEE Trans. on Computers
C25(8):852862, 1976.
[Morgan 1976b] C. Morgan, A resolution principle for a class of
manyvalued logics, Logique et Analyse n.s.19:311339, 1976.
[Morgan 1986] C.G. Morgan, AUTOLOGIC at University of Victoria,
Proc. 8th Intl. Conf. on Automated Deduction (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 699700.
[Moriconi 1977] M.S. Moriconi, A system for incrementally
designing and verifying programs, Certifiable Minicomputer
Project, Univ. of Texas at Austin, ICSCACMP9, 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, Eresolution: 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.
287294; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 273280.
[Morris 1977] J. Morris, B. Wegbreit, Subgoal induction, CACM
20(4):209222, 1977.
*[Moser 1988] L.E. Moser, A decision procedure for unquantified
formulas of graph theory, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
344357.
*[Moses 1971] J. Moses, Algebraic simplification: a guide for
the perplexed, Proc. 2nd Symp. on Symbolic and Algebraic
Manipulation (Los Angeles, CA, March 2325), ed. S.R. Petrick,
ACM, NY, 1971, pp. 282304; also CACM 14(8):527537, 1971.
[Mukai 1983] K. Mukai, A unification algorithm for infinite
trees, Proc. 8th Intl. Joint Conf. on Artificial Intelligence,
Karlsruhe, pp. 547549.
[Muller 1981] A. Muller, Implementation of a theorem prover
based on the connection method, Bericht ATP12XII81, Projekt
Beweisverfahren, Institut fur Informatik, Tech. Univ. Munchen,
1981.
*[Muller 1987] J. Muller, THEOPOGLES  A theorem prover based on
firstorder polynomials and a special KunthBenedix procedure,
Proc. 11th German Workshop on Artificial Intelligence (GWAI87,
Geseke, September 28October 2, 1987), ed. K. Morik, IFB 152,
SpringerVerlag, Berlin, 1987, pp. 241250.
*[Muller 1988a] J. Muller, R. SocherAmbrosius, Topics in
completion theorem proving, SEKI Report SR8813, Universitat
Kaiserslautern, Kaiserslautern, Germany, 1988.
*[Muller 1988b] J. Muller, R. SocherAmbrosius, On the
unnecessity of multiple overlaps in completion theorem proving,
Proc. Kunstliche Intelligenz (GWAI88, 12. Jahrestagung,
Eringerfeld, 1923 September 1988), InformatikFachberichte 181,
ed. W. Hoeppener, SpringerVerlag, Berlin, pp. 169178.
[Muller 1989a] J. Muller, ed., Abstracts of the 1st Workshop on
Term Rewriting, Theory and Applications, SEKI Report SR8902,
Fachbereich Informatik, Universitat Kaiserslautern,
Kaiserslautern, 1989.
*[Muller 1989b] J. Muller and R. SocherAmbrosuis, A resolution
calculus extended by equivalence, Proc. 13 German Workshop on
Artificial Intelligence (GWAI89, Eringerfeld, 1822 September
1989), ed. D. Metzing, SpringerVerlag, Berlin, 1989, pp. 102106.
*[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
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, p. 681.
[Mulmuley 1984] K. Mulmuley, The mechanization of existence
proofs of recursive predicates, Proc. 7th Intl. Conf. on Automated
Deduction (CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS
170, SpringerVerlag, NY, 1984, pp. 460475.
[Muluszynski 1982] J. Muluszynski, J.F. Nilsson, Grammatical
Unification, Information Processing Letters 15(4):150158, October
1982.
*[Munch 1988] K.H. Munch, A new reduction rule for the
connection graph proof procedure, J. Automated Reasoning
4(4):425444, December 1988.
[Munyer 1977] J.C. Munyer, Analogy as a heuristic for mechanical
theoremproving, Collected Abstracts of the Workshop on Automatic
Deduction, MIT, August 1977.
[Munyer 1981] J.C. Munyer, Analogy as a means of discovery in
problemsolving and learning, PhD thesis, Univ. California, Santa
Cruz, 1981.
[Murray 1978] N. Murray, A proofprocedure for nonclausal first
order logic, Research Report, Univ. of Syracuse, NY, 1978.
[Murray 1979] N. Murray, Linear and almostlinear methods for
the unification of first order expressions, PhD thesis, School of
Comp. Sci., Syracuse Univ., 1979.
[Murray 1982a] N.V. Murray, Competely nonclausal theorem
proving, Artificial Intelligence 18(1):6785, 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. 125131.
[Murray 1984] N.V. Murray, E. Rosenthal, Semantic graphs,
Technical Report 8412, 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, 13 April 1985), Vol. 2: Research
Contributions, ed. B.F. Caviness, LNCS 204, SpringerVerlag,
Berlin, pp. 5063.
[Murray 1985b] N.V. Murray, E. Rosenthal, Path resolution with
link deletion, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 1823
August 1985, pp. 11871193.
[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, 1519 July 1985), LNCS 229,
SpringerVerlag, pp. 404415.
[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):225254, April 1987.
[Murray 1986a] N.V. Murray, E. Rosenthal, Theory links, 863,
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
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 353364.
[Murray 1986c] N.V. Murray, E. Rosenthal, Path Dissolution for
propositional logic, 866, 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, 1317 July
1987, pp. 161166.
*[Murray 1987b] N.V. Murray, E. Rosenthal, Theory links:
applications to automated theorem proving, J. of Symbolic
Computation 4(2):173190, 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,
NorthHolland, 1987, pp. 416423.
*[Murray 1988a] N.V. Murray, E. Rosenthal, An implementation of
a dissolutionbased system employing theory links, Proc. 9th Intl.
Conf. on Automated Deduction (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 674658.
[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 (1214
October 1989, Charlotte, North Carolina), ed. Z.W. Ras, Elsevier
Science Publishing Co., NY, NY, 1989, pp. 477484.
*[Murray 1990a] N.V. Murray, E. Rosenthal, DISSOLVER: A
dissolutionbased theorem prover (abstract), Proc. 10th Intl.
Conf. on Automated Deduction (CADE10, Kaiserslautern, FRG, July
1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 665666.
*[Murray 1990b] N.V. Murray, E. Rosenthal, Reexamining
intractability of tableau methods, Proc. ISSAC '90 (Tokyo, Japan,
2024 August 1990), ACM, NY, NY, 1990, p. 5259.
*[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, 47 June 1990), IEEE Computer Society
Press, Los Alamitos, CA, 1990, pp. 257267.
[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. 154162.
[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, SpringerVerlag, pp. 7890.
[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. 5772.
[Musser 1985] D. Musser, Aids to hierarchical specification and
reusing theorems in Affirm85, 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, SpringerVerlag, NY, 1989, pp. 440464.
*[Myers 1990] K.L. Myers, Automatically generating universal
attachments through compilation, Proc. 8th National Conf. on
Artificial Intelligence (AAAI90, July 29August 3, 1990), AAAI
Press/MIT Press, 1990, pp. 252257.
[Mzali 1986] J. Mzali, Matching with distributivity, Proc. 8th
Intl. Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 496505.
[Nagle 1982] J. Nagle, S. Johnson, Practical program
verification, Automatic program proving for realtime embedded
software, WDLTR9859, Ford Aerospace and Communications
Corporation, December 1982.
[Nakajima 1983] R. Nakajima, T. Yuasa, The IOTA Programming
System, LNCS 160, SpringerVerlag, NY, 1983.
[Nakanishi 1975] M. Nakanishi, M. Nagata, Y. Iwamara,
Gentzentype formal system representing properties of function and
its implementation, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975,
pp. 5764.
[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. 636638.
*[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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 311325.
[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. 263265.
[Narain 1985] S. Narain, A technique for doing lazy evaluation
in logic, Proc. 1985 Symp. on Logic Programming, IEEE Society
Press, 1985, pp. 261269.
*[Narain 1989] S. Narain, Optimization by nondeterministic,
lazy rewriting, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 326342.
[Narendran 1984a] P. Narendran, R. Menanghton, The
undecidability of the preperfectness of Thue systems,
NorthHolland, Theoretical Computer Science 31(1984):165174.
[Narendran 1984b] P. Narendran, ChurchRosser 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. 217235.
*[Narendran 1990] P. Narendran, F. Otto, Some results on
equational unification, Proc. 10th Intl. Conf. on Automated
Deduction (CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes
in Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 276291.
*[Naughton 1989] J.F. Naughton, Y. Sagiv, Minimizing expansions
of recursions, In: Resolution of Equations in Algebraic
Structures: Vol 1, Algebraic Techniques, ed. H. AitKaci, M.
Nivat, Academic Press, Inc., San Diego, 1989, pp. 321349.
[Navarro 1984] M. Navarro, F. Orejas, On the equivalence of
hierarchical and nonhierarchical 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 lambdacalculus, Proc. 5th Conf. on
Automated Deduction (Les Arcs, France), ed. W. Bibel and R.
Kowalski, LNCS 87, SpringerVerlag, Berlin, 1980, pp. 182194.
[Nederpelt 1980b] R.P. Nederpelt, A system of natural reasoning
based on a typed lambdacalculus, Bull. Eur. Assoc. Theoret. Comp.
Sci. 11(1980): 130131.
[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. 141150.
[Nelson 1979] G. Nelson, D.C. Oppen, Simplification by
cooperating decision procedures, ACM Trans. on Programming
Languages and Systems 1(2):245257, October 1979.
[Nelson 1980] G. Nelson, D.C. Oppen, Fast decision procedures
based on congruence closure, STANCS77646, Stanford U,; also
JACM 27(2):356364, April 1980.
[Nelson 1981] G. Nelson, Techniques for program verification,
Xerox Palo Alto Research Center, CA, CSL8110, June 1981.
[Nelson 1983] G. Nelson, Verifying reachability invariants of
linked structures, Proc. 10th Principles of Programming Languages,
Austin, Texas, 1983, pp. 3847.
[Nevin 1972] A.J. Nevins, A human oriented logic for automatic
theoremproving, Mass. Inst. of Tech., Cambridge, MA, AI Memo No.
268, 1972; also JACM 21(4):606621, October 1974.
[Nevins 1975a] A.J. Nevins, Plane geometry theorem proving using
forward chaining, Artificial Intelligence 6(1):123, Spring 1975.
[Nevins 1975b] A.J. Nevins, A relaxation approach to splitting
in an automated theorem prover, Artificial Intelligence
6(2):2539, 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.,
CarnegieMellon Univ., July 1956.
[Newell 1956b] A. Newell, J.C. Shaw, H.A. Simon, The logic
theory machine, IRE Trans. Information Theory IT2(3):6179, 1956;
also Computers and Thought, McGrawHill, 1963.
[Newell 1957a] A. Newell, J.C. Shaw, Programming the logic
theory machine, Computer Science Dept., CarnegieMellon 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., CarnegieMellon 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., CarnegieMellon
Univ., March 1957.
[Newell 1958] A. Newell, J.C. Shaw, H.A. Simon, A report on a
general problemsolving program (GPS1), Rand Corp. Memo P1584,
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., CarnegieMellon Univ., July 1959.
[Newell 1960] A. Newell, J.C. Shaw, H.A. Simon, Comment: Toward
mechanical mathematics, Computer Science Dept., CarnegieMellon
Univ., February 1960.
[Newell 1961] A. Newell, J.C. Shaw, H.A. Simon, A program that
simulates human thought, Computer Science Dept., CarnegieMellon
Univ., April 1961.
[Newell 1963] A. Newell, A guide to the general problem solver
program GPS22, Computer Science Dept., CarnegieMellon Univ.,
February 1963.
[Newell 1963a] A. Newell, H. Simon, GPS a program that simulates
human thought, in Computers and Thought, ed. Feigenbaum and
Feldman, McGrawHill, NY, 1963, pp. 279296.
[Newell 1963b] A. Newell, J. Shaw, H. Simon, Empirical
explorations with the logic theory machine, in Computers and
Thought, ed. Feigenbaum and Feldman, McGrawHill, NY, 1963, pp.
109133; also Automation of Reasoning  Classical Papers on
Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 4973.
[Newell 1965] A. Newell, G. Ernst, The Search for Generality,
Proc. IFIP Congress 1965, Vol. 1, Spartan Books, Washington, D.C.,
1965, pp. 1724.
[Newell 1967] A. Newell, A general problemsolving program,
Computer Science Dept., CarnegieMellon Univ., June 1967.
[Newman 1942] M.H.A. Newman, On theories with a combinatorial
definition of equivalence, Annals of Math. 43(2):223243. 1942.
*[Ngair 1993] T.H. Ngair, A new algorithm for incremental prime
implicate generation, Proc. 13th IJCAI (Chambery, France, 28
August3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993,
pp. 4651.
[Nie 1989a] Xumin Nie, and D.A. Plaisted, Refinements to
depthfirst iterativedeepening search in automatic theorem
proving, Artificial Intelligence 41(1989/90):223235.
[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 (CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes
in Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 1627.
*[Nie 1992] X. Nie, and D.A. Plaisted, A semantic backward
chaining proof system, Artificial Intelligence 55(1):109128, May
1992.
*[Nieuwenhuis 1990] R. Nieuwenhuis, R. Orejas, A. Rubio, TRIP:
An implementation of clausal rewriting (abstract), Proc. 10th
Intl. Conf. on Automated Deduction (CADE10, Kaiserslautern, FRG,
July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 667668.
*[Nieuwenhuis 1992] R. Nieuwenhuis, A. Rubio, Theorem proving
with ordering constrained clauses, Proc. 11th Intl. Conf. on
Automated Deduction (CADE11, Saratoga Springs, NY, USA, June
1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 477491.
*[Niemela 1988] I. Niemela, Decision procedure for autoepistemic
logic, Proc. 9th Intl. Conf. on Automated Deduction (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 675684.
[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, McGrawHill, 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, 101128.
[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. 8792.
*[Nilsson 1989] J.F. Nilsson, A case study in knowledge
representation and reasoning with higherorder combinators, Proc.
Scandinavian Conf. on Artificial Intelligence  89 (SCAI '89,
Tapere, Finland, 1315 June 1989), ed. H. Haakkola and S.
Linnainmaa, IOS, Amsterdam, Netherlands, 1989, pp. 3748.
*[Nipkow 1989a] T. Nipkow, Combining matching algorithms: The
regular case, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 343358.
[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): 123149.
[Nipkow 1989e] T. Nipkow, Term rewriting and beyond  theorem
proving in Isabelle, Formal Aspects of Computer 1(1989): 320338.
*[Nipkow 1990a] T. Nipkow, Proof transformations for equational
theories, Proc. 5th Annual IEEE Symp. on Logic Computer Science
(Philadelphia, PA, 47 June 1990), IEEE Computer Society Press,
Los Alamitos, CA, 1990, pp. 278288.
[Nipkow 1990b] T. Nipkow, Unification in primal algebras, their
powers and their varieties, JACM 37(4):742776, October 1990.
*[Nipkow 1991a] T. Nipkow, Higherorder critical pairs, Proc.
6th Annual IEEE Symp. on Logic in Computer Science (Amsterdam, The
Netherlands, 1518 July 1991), IEEE Computer Society Press, Los
Alamitos, CA, 1991, pp. 342349.
*[Nipkow 1991b] T. Nipkow, Constructive rewriting, The Computer
Journal 34(1):3441, February 1991.
*[Nipkow 1992a] T. Nipkow, Z. Qian, Reduction and unification in
lambda calculi with subtypes, Proc. 11th Intl. Conf. on Automated
Deduction (CADE11, Saratoga Springs, NY, USA, June 1992), ed. D.
Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 6678.
*[Nipkow 1992b] T. Nipkow, L.C. Paulson, Isabelle91, Proc. 11th
Intl. Conf. on Automated Deduction (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 673676.
[Nipkow 1993] T. Nipkow, Orthogonal higherorder 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, Gentzentype 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. AitKaci, M. Nivat, Academic Press, Inc., San Diego, 1989,
pp. 351367.
[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, 811 July 1980), ed. W.
Bibel and R. Kowalski, LNCS 87, SpringerVerlag, Berlin, 1980, pp.
250263.
*[Nonnengart 1993] A. Nonnengart, Firstorder modal logic
theorem proving and functional simulation, Proc. 13th IJCAI
(Chambery, France, 28 August3 September 1993), Vol 1, ed. R.
Bajscy, IJCAI, Inc., 1993, pp. 8087.
[Nordstrom 1981] B. Nordstrom, Programming in constructive set
theory: Some examples, ACM Conf. on Functional Programming
Languages and Computer Architecture, Portsmouth, NH, 1981, pp.
141153.
[Norton 1966] L.M. Norton, ADEPT  A heuristic program for
proving theorems of group theory, PhD thesis, MIT, Boston, Report
MACTR33, Project Mac, MIT, September 1966, 176pp.
[Norton 1971] L.M. Norton, Experiments with a heuristic
theoremproving for the predicate calculus with equality,
Artificial Intelligence 2(3):261284, 1971.
[Norton 1972] L.M. Norton, Heuristic programming and theorem
proving, Trans. Am. Nucl. Soc. 15(2):777778, November 1972.
*[Norvig 1991] P. Norvig, Correcting a widespread error in
unification algorithms, Software  Practice and Experience
2(2):231233, 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):5164.
[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):1122.
*[Nutt 1987] W. Nutt, P. Rety, G. Smolka, Basic narrowing
revisited, SEKI Report SR8707, Universitat Kaiserslautern, West
Germany, July 1987.
[Nutt 1989] W. Nutt, The unification hierarchy is undecidable,
SEKI Report SR8906, Universitat Kaiserslautern, 1989.
*[Nutt 1990] W. Nutt, Unification in monoidal theories, Proc.
10th Intl. Conf. on Automated Deduction (CADE10, Kaiserslautern,
FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed.
M.E. Stickel, SpringerVerlag, Berlin, 1990, pp. 618632.
*[Nutt 1991] W. Nutt, The unification heirarchy is undecidable,
J. Automated Reasoning 7(3):369381, September 1991.
