[O'Donnell 1987] M.J. O'Donnell, Term-rewriting implementation of equational logic programming, 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. 1-12.

[Ogawa 1979] H. Ogawa, T. Kitahashi, K. Tanaka, The theorem prover using a parallel processing system, Proc. 6th IJCAI, Tokyo, August 1979, pp. 665-667.

*[O'Hearn 1989a] P. O'Hearn, Z. Stachniak, A resolution framework for finitely-valued first-order logics, 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. 69-81; also J. Symbolic Comput. 13(3):235-254, March 1992.

[O'Hearn 1989b] P. O'Hearn, Z. Stachniak, A note on theorem proving strategies for resolution counterparts of finitely-valued logic, Proc. Internat. Symp. on Symbolic and Algebraic Computation, Portland, pp. 364-372, 1989.

[Ohlbach 1982] H.J. Ohlbach, The Markgraf Karl refutation procedure: The logic engine, Interner Bericht 24/82, Memo SEKI-82-11, Inst. fur Informatik I, Univ. Karlsruhe, 1982.

[Ohlbach 1983a] H.J. Ohlbach, The Markgraf Karl refutation procedure, the Terminator module, Interner Bericht, Univ. of Karlsruhe, 1983.

[Ohlbach 1983b] H.J. Ohlbach, G. Wrightson, Solving a problem in relevance logic with an automated theorem prover, Interner Bericht 11/83, Memo SEKI-83-V, Institut fur Informatik I, Universitat Karlsruhe, W. Germany, 1983. 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. 496-508.

[Ohlbach 1985a] H.J. Ohlbach, M. Schmidt-Schauss, The lion and the unicorn, J. of Automated Reasoning 1(3):327-332, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Ohlbach 1985b] H.J. Ohlbach, Predicate logic hacker tricks, J. of Automated Reasoning 1(4):435-440, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Ohlbach 1985c] H.J. Ohlbach, Theory unification in abstract clause graphs, Proc. GWAI-85, 9th German Workshop on Artificial Intelligence, Dassel/Solling (23-27 September 1985), Informatik-Fachberichte 118, ed. H. Stoyan, Springer-Verlag, Berlin, 1985, pp. 77-100.

*[Ohlbach 1986] H.J. Ohlbach, The semantic clause graph procedure -- A first overview, GWAI-86 und 2. Osterreichische Artificial-Intelligence-Tagung (Ottenstein/Niederosterreich, 22-26 September 1986), Informatik-Fachberichte 124, Springer-Verlag, Berlin, 1986, pp. 218-229.

[Ohlbach 1987] H.J. Ohlbach, Link inheritance in abstract clause graphs, J. of Automated Reasoning 3(1):1-34, March 1987.

*[Ohlbach 1988a] H.-J. Ohlbach, A resolution calculus for modal logics, SEKI Report SR-88-08, Universitat Kaiserslautern, 1988. also 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. 500-516.

[Ohlbach 1988b] H.-J. Ohlbach, J. Siekmann, Using automated reasoning techniques for deductive databases, SEKI Report SR-88-06, Universitat Kaiserslautern, 1988.

[Ohlbach 1989a] H.-J. Ohlbach, Context Logic, SEKI Report SR-89-08, Fachbereich Informatik, Universitat Kaiserslautern, Kaiserslautern, Germany, 1989.

*[Ohlbach 1989b] H.-J. Ohlbach, Context Logic -- An Introduction, Proc. 13 German Workshop on Artificial Intelligence (GWAI-89, Eringerfeld, 18-22 September 1989), ed. D. Metzing, Springer-Verlag, Berlin, 1989, pp. 27-36.

*[Ohlbach 1990a] H.J. Ohlbach, A. Herzig, Compilation techniques for logics (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. 683.

*[Ohlach 1990b] H.J. Ohlbach, Abstraction tree indexing for terms, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 479-484.

[Ohlach 1990c] H.J. Ohlbach, Compilation of recursive two-literal clauses into unification n algorithms, Proc. AIMSA, 1990.

[Ohsuga 1986a] A. Ohsuga, K. Sakai, Refutational theorem proving for equational systems based on term rewriting, Tech. Report COMP86-40, ICOT, 1986.

[Ohsuga 1986b] A. Ohsuga, K. Sakai, Metis: A term rewriting system generator, Tech. Report, ICOT Research Center, Tokyo, Japan, 1986.

[Ohsuga 1988] A. Ohsuga, K. Sakai, An efficient implementation method of reduction and narrowing in Metis, Tech. Report, ICOT Research Center, Japan, 1988.

*[Okada 1988] M. Okada, A logical analysis for theory of conditional rewriting, 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. 179-196.

[Omodeo 1982] E.G. Omodeo, The linked conjunct method for automatic deduction and related search techniques, Comput. and Math. with Appl. 8(3):185-203, 1982.

[Omodeo 1984] E.G. Omodeo, Decidability and proof procedures for set theory with a choice operator, PhD thesis, New York Univ., GSAS, Courant Institute of Mathematical Sciences, New York, 1984.

*[Omodeo 1986] E.G. Omodeo, Hints for the design of a set calculus oriented to Automated Deduction, Proc. Foundations of Logic and Functional Programming (Trento, Italy, 15-19 December 1986), ed. M. Boscarol, L.C. Aiello, and G. Levi, LNCS 306, Springer-Verlag, 1988, pp. 201-218.

*[Omodeo 1990] E. Omodeo, F. Parlamento, A. Policriti, Truth tables for a combinatorial kernel of set theories, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 485-490.

[Oppacher 1986a] F. Oppacher, E. Suen, Controlling deduction with proof condensation and heuristics, 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. 384-393.

[Oppacher 1986b] F. Oppacher, E. Suen, An efficient tableau-based theorem prover, Proc. 6th Canadian Conf. on Artificial Intelligence, Ecole Polytechnique de Montreal, Montreal, Canada, May 1986, pp. 31-35.

*[Oppacher 1988] F. Oppacher, E. Suen, HARP: A tableau-based theorem prover, J. of Automated Reasoning 4(1):69-100, March 1988.

[Oppen 1977] D. Oppen, G. Nelson, Fast decision algorithms based on union and find, Proc. 8th Symp. on Foundations of Computer Science, IEEE Computer Society, Princeton, N.J., 1977, pp. 114-119.

[Oppen 1978] D. Oppen, Reasoning about recursively defined data structures, CS Report STAN-CS-78-678, Stanford Univ., 1978; Proc. 5 ACM Symp. POPL, 1978, pp. 151-157.

[Oppen 1979] D.C. Oppen, Convexity, complexity and combinations of theories, 4th Symp. on Automated Deduction, Austin, 1979.

[Oppen 1979] D. Oppen, Complexity, convexity and combinations of theories, Theoretical Computer Science 12(1980):291-302.

[Orekov 1971] V.P. Orekov, On nonlengthening applications of equality rules, Seminars in Mathematics 16, V.A. Steklov Mathem. Institute, Leningrad, Consultants Bureau, NY-London, 1971, pp. 77-79.

[Orgass 1974] R.J. Orgass, Y.H. Teng, An interactive proof checking program, Laboratory for Computer Science, Rutgers Univ., 1974.

[Orlowska 1972] E. Orlowska, Theorem proving systems, Intl. Symp. and Summer School on Math. Foundations of Comput. Sci., Warsaw, Poland, August 1972.

[Orlowska 1978] E. Orlowska, The resolution principle for omega/sup +/-valued logic, Ann. Soc. Math. Pol. Ser. IV: Fundam. Inf. 2(7):1-15, Poland, 1978.

[Orlowska 1980] E. Orlowska, Resolution systems and their applications, I and II, Fundamenta Informaticae, pp. 235-267, 333-362, Poland, 1980.

[Otto 1985a] F. Otto, Deciding algebraic properties of monoids presented by finite Church-Rosser Thue systems, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 95-106.

[Otto 1985b] F. Otto, Elements of finite order for finite monadic Church-Rosser Thue systems. Transactions of the American Math. Soc. 291(1985):629-637.

[Otto 1985c] F. Otto, Decision problems and their complexity for monadic Church-Rosser Thue systems, Habilitationsschrift, Univ. Kaiserslautern, 1985.

[Otto 1987a] F. Otto, C. Squier, The word problem for finitely presented monoids and finite canonical rewriting systems,

[Otto 1987b] F. Otto, Some results about confluence on a given congruence class, 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. 145-155.

*[Otto 1989] F. Otto, Restrictions of congruences generated by finite canonical string-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. 359-370.

[Overbeek 1974] R.A. Overbeek, A new class of automated theorem-proving algorithms, JACM 21(1974):191-200.

[Overbeek 1975] R.A. Overbeek, An implementation of hyper-resolution, Computers and Mathematics with Applications 1(1975):201-214.

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

[Overbeek 1980] R.A. Overbeek, E.L. Lusk, Data structures and control architecture for implementation of theorem-proving programs, 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.

[Owe 1981] O. Owe, A technique for quantifier removal, Research Rep. 65, Inst. of Informatics, Univ. of Oslo, 1981.

[Owen 1968] R.H. Owen, Some Experiments with a Computer Realization of a Theorem-Proving Method, Dept. of Machine Intelligence and Perception, Univ. of Edinburgh, Res. Memo, No. MIP-R-43, November 1968.

[Owen 1986] S. Owen, Heuristics for analogy matching, DAI Research Paper 280, Dept. of Artificial Intelligence, Univ. of Edinburgh, February 1986; also in Proc. 7th ECAI, ECAI, 1986.

[Owen 1988] S. Owen, Finding and using analogies to guide mathematical proof, PhD thesis, Univ. of Edinburgh, 1988.

[Owen 1990] S. Owen, Analogy for automated reasoning, Volume 9, Academic Press, Inc., San Diego, CA, 1990.

[Owre 1985] S. Owre, J.D. Halpern, MUSE: The Sytek proof processing system, Sytek TR-85007, Sytek, Incorporated, 1225 Charleston Road, Mountain View, CA 94039, July 1985.

*[Owre 1992] S. Owre, J.M. Rushby, N. Shankar, PVS: A Prototype Verification System, 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. 748-752.

[Oyamaguchi 1986] M. Oyamaguchi, Sufficient sequentiality: a decidable condition for call-by-need computations in term rewriting systems, COMP86-38, 1986.

[Oyamaguchi 1987] M. Oyamaguchi, The Chruch-Rosser property for ground term-rewriting systems is decidable, Tech. Report, Faculty of Engineering, Mie University, Tsu 514, Japan, 1987; Theoretical Computer Science 49(1): 43-80, 1987.

[Ozturk 1989] Y. Ozturk, Interactive advice system for automated theorem provers, PhD Thesis, EECS Dept., Northwestern Univ., Evanston, 1989.

*[Ozturk 1990] Y. Ozturk, L. Henschen, Hyper resolution and equality axioms without functions substitutions, 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. 456-469.

[Padawitz 1983] P. Padawitz, Correctness, completeness and consistency of equational data type specifications, Dissertation, Report No. 83-15, FB 20, TU Berlin, 1983.

*[Padawitz 1986] P. Padawitz, Horn clause specifications: Reduction and narrowing, MIP-8601, Universitat Passau, Fakultat fur Mathematik und Informatik, February 1986.

[Padawitz 1987a] P. Padawitz, Strategy-controlled reduction and narrowing, 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. 242-255.

*[Padawitz 1987b] P. Padawitz, ECDS -- A rewrite rule based interpreter for a programming language with abstraction and communication, Report MIP-8703, Fakultat fur Mathematik und Informatik, Universitat Passau, 1987.

*[Padawitz 1988a] P. Padawitz, Inductive proofs of constructor-based Horn clauses, Report MIP-8810, Fakultat fur Mathematik und Informatik, Universitat Passau, April 1988.

*[Padawitz 1988b] P. Padawitz, Computing in Horn clause theories, EATCS Monographs on Theoretical Computer Science 16, Springer-Verlag, Berlin, 1988.

[Padawitz 1988c] P. Padawitz, Can inductive proofs be automated? EATCS Bulletin 35(1988): 163-170.

[Padawitz 1988d] P. Padawitz, Reduction and narrowing for Horn clause theories, Report, Universitat Passau, 1988; also Comput. J. 34(1):42-51, February 1991.

*[Padawitz 1989a] P. Padawitz, Inductive Expansion, MIP-8907, Fakultat fur Mathematik und Informatik, Universitat Passau, April 1989.

[Padawitz 1989b] P. Padawitz, Can inductive proofs be automated? Part II. EATCS Bulletin 37(1989): 168-174.

[Padawitz 1989c] P. Padawitz, On goal and term reduction calculi, Proc. 1st German Workshop on Term Rewriting, SEKI Report SR-89-02, Universitat Kaiserslautern, 1989.

[Padawitz 1990] P. Padawitz, Horn logic and rewriting for functional and logic program design, Report MIP-9002, Fakultat fur Mathematik und Informatik, Universitat Passau, 1990.

*[Padawitz 1991] P. Padawitz, Inductive expansion: a calculus for verifying and synthesizing functional and logic programs, J. Automated Reasoning 7(1):27-103, March 1991.

*[Padawitz 1991] P. Padawitz, Reduction and Narrowing for Horn clause theories, The Computer Journal 34(1):42-51, February 1991.

*[Panangaden 1989] P. Panangaden, P. Mendler, M.I. Schwartzbach, Recursively defined types in constructive type theory, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 369-410.

[Pankov 1978] P.S. Pankow, Composite method of proving some theorems in mathematical analysis with the aid of electronic computers, Kibernetika 14(3):119-125, USSR, May 1978.

[Parlamento 1988] F. Parlamento, A. Policriti, Decision procedures for elementary sublanguages of set theory. IX. Undecidability of set theoretic formulas involving restricted quantifiers, Comm. Pure Appl. Math 41(1988):221-251.

*[Parlamento 1991] F. Parlamento, A. Policriti, Decision procedures for elementary sublanguages of set theory: XIII. Model graphs, reflection and decidability, J. of Automated Reasoning 7(2):271-284, June 1991.

*[Parnas 1993] D. L. Parnas, Some theorems we should prove, Communications Research Laboratory, Dept. of Electrical and Computer Engineering, McMaster University, Hamilton, Ontario, June 1993.

*[Pase 1987] B. Pase, S. Kromodimoeljo, m-NEVER user's manual, TR-87-5420-13, I.P. Sharp Associates Limited, November 1987.

*[Pase 1988] B. Pase, S. Kromodimoeljo, m-NEVER System Summary, 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. 738-739.

*[Pase 1989] B. Pase, M. Saaltink, Formal verification in m-EVES, In Current Trends in Hardware Verification and Automated Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, NY, 1989, pp. 268-302.

[Pastre 1978] D. Pastre, Automatic theorem proving in set theory, Artificial Intelligence 10(1):1-27, North-Holland, 1978.

*[Pastre 1982] D. Pastre, A language for expressing mathematical knowledge in automatic theorem proving, Proc. ECAI-82, Paris-Sud, Orsay, France, 12-14 July 1982, pp. 116-118.

[Pastre 1987] D. Pastre, MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics, PhD thesis, Univ. Paris, 1987; also Artificial Intelligence Journal 38(April 1989):257-318.

*[Patel-Schneider 1990] P.F. Patel-Schneider, A decidable first-order logic for knowledge representation, J. Automated Reasoning 6(4):361-388, December 1990.

[Paterson 1978] M.S. Paterson, M.N. Wegman, Linear Unification, J. of Computer and Systems Sciences 16(2):158-167, 1978.

[Paul 1984a] E. Paul, A new interpretation of the resolution principle, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 333-355.

[Paul 1984b] E. Paul, Proof by induction in equational theories with relations between constructors, Proc. 9th Colloquium on Trees in Algebra and Programming (Bordeaux, France, March 1984), ed. B. Courcelle, Cambridge Univ. Press, 1984, pp. 211-225.

*[Paul 1985a] E. Paul, On solving the equality problem in theories defined by Horn clauses, 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. 363-377; also Theoretical Computer Science 44(2):127-153, 1986.

[Paul 1985b] E. Paul, Equational methods in first order predicate calculus, J. of Symbolic Computation 1(1):7-29, March 1985.

[Paulson 1983a] L. Paulson, The revised logic PPLAMBDA - A reference manual, Tech. Report 36, Computer Laboratory, Univ. of Cambridge, March 1983.

[Paulson 1983b] L. Paulson, Tactics and tacticals in Cambridge LCF, Tech. Report 39, Computer Laboratory, Univ. of Cambridge, July 1983.

[Paulson 1983c] L. Paulson, A higher-order implementation of rewriting, North-Holland, Science of Computer Programming 3(1983):119-149.

[Paulson 1983d] L. Paulson, Recent developments in LCF: Examples of structural induction, Tech. Report 34, Computer Laboratory, Univ. of Cambridge, January 1983.

[Paulson 1984a] L.C. Paulson, Deriving structural induction in LCF, Intl. Symp. on Semantics of Data Types, ed. G. Kahn, D.B. MacQueen, and G. Plotkin, Springer, pp. 197-214, 1984.

[Paulson 1984b] L.C. Paulson, Verifying the unification algorithm in LCF, Tech. Report 50, Computer Laboratory, Univ. of Cambridge, March 1984; also Science of Computer Programming 5(1985):143-169.

[Paulson 1985a] L.C. Paulson, Lessons learned from LCF: A survey of natural deduction proofs, The Computer J. 28(5):474-479, November 1985.

[Paulson 1985b] L.C. Paulson, Interactive theorem proving with Cambridge LCF: A user's manual, Report 80, Computer Lab., Univ. of Cambridge, 1985.

[Paulson 1985c] L.C. Paulson, Natural deduction proof as higher-order resolution, Tech. Report 82, Univ. of Cambridge, Computer Laboratory, 1985; also J. of Logic Programming 3(1986):237-258.

*[Paulson 1985d] L.C. Paulson, Proving termination of normalization functions for conditional expressions, Tech. Report 69, Univ. of Cambridge, Computer Laboratory, June 1985; also J. of Automated Reasoning 2(1):63-74, D. Reidel Publ. Co., Dordrecht, Holland, 1986.

*[Paulson 1986a] L.C. Paulson, Natural deduction as higher-order resolution, J. of Logic Programming 3(3):237-258, October 1986; also Pattern Recognition Letters 5(3):237-258, March 1987.

[Paulson 1986b] L.C. Paulson, Constructing recursion operators in intuitionistic type theory, J. of Symbolic Computation 2(1986):325-355.

[Paulson 1987a] L.C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge Univ. Press, 1987.

[Paulson 1987b] L.C. Paulson, The representation of logics in higher-order logic, Univ. Cambridge Technical Report R-113, 1987.

*[Paulson 1988a] L.C. Paulson, The foundation of a generic theorem prover, Report 130, Computer Laboratory, Univ. of Cambridge, 1988; also J. Automated Reasoning 5(3):363-397, September 1989.

*[Paulson 1988b] L.C. Paulson, A preliminary user's manual for Isabelle, Report 133, Computer Laboratory, Univ. of Cambridge, 1988.

*[Paulson 1988c] L.C. Paulson, Isabelle: The next seven hundred theorem provers, 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. 772-773.

[Paulson 1988d] L.C. Paulson, Higher-order logic as the basis of generic theorem provers, Report, Computer Lab., Univ. of Cambridge, 1988.

*[Paulson 1988e] L.C. Paulson, Experience with Isabelle: A generic theorem prover (preliminary version), Tech. Report No. 143, Computer Lab., Univ. of Cambridge, August 1988; also in COLOG 88, Institute of Cybernetics of the Estonian SSR, 1988.

*[Paulson 1989] L.C. Paulson, A formulation of the simple theory of types (for Isabelle), Tech. Report No. 175, Computer Laboratory, Univ. of Cambridge, August 1989.

*[Paulson 1993] L.C. Paulson, Set theory for verification: II. Induction and recursion, Tech. Report No. 312, Computer Laboratory, Univ. of Cambridge, September 1993.

[Pearl 1984] J. Pearl, Heuristics: Intelligent search strategies for computer problem solving, Addison-Wesley Publishing Company, 1984.

*[Pearl 1987] J. Pearl, R.E. Korf, Search techniques, Annual Review of Computer Science, Vol. 2, 1987. pp. 451-467.

[Pedersen 1981] J. Pedersen, M. Stickel, Complete sets of reductions for some equational theories, JACM 28(1981):233-264.

*[Pedersen 1985] J. Pedersen, Obtaining complete sets of reductions and equations without using special unification algorithms (extended abstract), 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. 422-423.

*[Pedersen 1989] J. Pedersen, Morphocompletion for one-relation monoids, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 574-578.

[Pederson 1984] J. Pederson, Confluence methods and the word problem in universal algebra, PhD diss., Emory Univ., Atlanta, 1984.

*[Peikert] R. Peikert, Automated theorem proving: the resolution method, SIGSAM Bulletin 21(3):61-68, August 1987.

[Pelin 1984] A. Pelin, J.H. Gallier, Solving word problems in free algebras using complexity functions, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 476-495.

*[Pelin 1988] A. Pelin, Computing with conditional rewrite rules, 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. 197-211.

[Pelletier 1982] F.J. Pelletier, Completely non-clausal, completely heuristically driven, automatic theorem proving, M.Sc. Thesis, Tech. Report TR82-7, Dept. of Computing Science, Univ. of Alberta, Edmonton, Alberta, 1982.

[Pelletier 1986a] F.J. Pelletier, Seventy-five problems for testing automatic theorem provers, J. of Automated Reasoning 2(2):191-216, D. Reidel Publ. Co., Dordrecht, Holland, 1986; also ``Errata,'' J. of Automated Reasoning 1988, pp. 235-236.

[Pelletier 1986b] F.J. Pelletier, THINKER, 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. 701-702.

[Pelletier 1987] F.J. Pelletier, Further developments in THINKER, an authomated theorem prover, Tech. Report TR-ARP-16.87, Automated Reasoning Project, Australia National Univeristy.

*[Pelletier 1991] F.J. Pelletier, The philosophy of automated theorem proving, Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1 (IJCAI-91, Darling Harbour, Sydney, Australia, 24-30 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp. 1039-1045.

[Pelletier 1993a] F.J. Pelletier, Automated Modal Logic Theorem Proving in THINKER. Tech Report TR 93-14, Department of Computing Science, Univ. Alberta, 1993. (source: F.J. Pelletier)

[Pelletier 1993b] F.J. Pelletier, Identity in Modal Logic Theorem Proving, in Studia Logica, v. 52, 1993, pp. 291-308. (source: F.J. Pelletier)

[Pereira 1978] L.M. Pereira, F.C.N. Pereira, D.H.D. Warren, User's guide to DEC system-10 Prolog, LNEC, Lisbon, 1978.

[Pereira 1979] L.M. Pereira, A. Porto, Intelligent backtracking and sidetracking in Horn clause programs - the theory, Dept. di Informatica, Universidade Nova de Lisboa, 1979.

[Pereira 1980] L.M. Pereira, A. Porto, Selective backtracking for logic programs, 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.

[Pereira 1985] F. Pereira, Logic programming, J. of Automated Reasoning 1(1):9-12, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

*[Perrin 1989] D. Perrin Equations in words, In: Resolution of Equations in Algebraic Structures: Vol 2, Rewriting Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 275-296.

[Peterson 1976] G.E Peterson, Theorem proving with lemmas, JACM 23(4):573-581, 1976.

[Peterson 1977] G.E. Peterson, M.E. Stickel, Complete sets of reductions for equational theories with complete unification algorithms, Tech. Rep., Dept. of Comput. Sci., Univ. of Arizona, Tucson, Arizona, September 1977; also JACM 28(2):233-264, 1981; also Tech. Note 269, SRI International.

[Peterson 1978] J. Peterson, An automatic theorem prover for substitution and detachment systems, Notre Dame J. of Formal Logic, Vol. XIX, January 1978, 119-122.

[Peterson 1980] G.E. Peterson, A technique for establishing completeness results in theorem proving with equality, Proc. 1st Natl. Conf. on Artificial Intelligence, Stanford Univ., CA, August 1980, pp. 87-89; also SIAM J. of Computing 12(1):82-100, 1983.

[Peterson 1981] G.E. Peterson, M.E. Stickel, Complete sets of reductions for some equational theories, JACM 28(2):233-264, April 1981.

[Peterson 1982] G.E. Peterson, M.E. Stickel, Complete systems of reductions using associative and commutative unification, Tech. note 269, Artificial Intelligence Center, SRI International, Menlo Park, CA, Oct 1982, to appear in Lecture Notes on Systems of Reductions, ed. M. Richter, 1982.

[Peterson 1983] G. Peterson, A technique for establishing completeness results in theorem proving with equality, SIAM J. of Computing 12(1):82-100, February 1983.

*[Peterson 1990a] G.E. Peterson, Complete sets of reduction with constraints, 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. 381-395.

*[Peterson 1990b] G.E. Peterson, Solving term inequalties, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 258-263.

[Pevac 1985] I. Pevac, Heuristic for avoiding skolemization in theorem proving, Publ. Inst. Math. 38(52), Beograd (N.S.), 1985, pp. 207-213.

[Pfenning 1984a] F. Pfenning, S. Issar, D. Nesmith, and P.B. Andrews, ETPS User's Manual, 5th edition, 44pp.

[Pfenning 1984b] F. Pfenning, Analytic and non-analytic proofs, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 394-413.

[Pfenning 1987] F. Pfenning, Proof transformations in higher-order logic, PhD thesis, Dept. of Mathematics, Carnegie-Mellon Univ., January 1987.

*[Pfenning 1988] F. Pfenning, Single axioms in the implicational propositional calculus, 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. 710-713.

*[Pfenning 1989] F. Pfenning, Elf: A language for logic definition and verified metaprogramming, Proc. 4th Annual Symp. on Logic in Computer Science (Pacific Grove, CA, 5-8 June 1989), IEEE Computer Society Press, 1989, pp. 313-322.

*[Pfenning 1990] F. Pfenning, D. Nesmith, Presenting intuitive deductions via symmetric simplification, 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. 336-350.

*[Pfenning 1991] F. Pfenning, Unification and anti-unification in the calculus of constructions, 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. 74-85.

[Pfenning 1992] F. Pfenning, E. Rohwedder, Implementing the meta-theory of deductive systems, 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. 537-551.

[Phyushevichene 1971] A. Yo Phyushevichene, Elimination of Cut-Type Rules in Axiomatic Theories with Equality, Seminars in Mathematics 16, V.A. Steklov Mathem. Institute, Leningrad, Consultants Bureau, NY-London, 1971, pp. 90-94.

*[Piazza 1990] J.S. di Piazza, Interweaving knowledge extracting, organizing and evaluating: A concrete design for preventing logic and structure bugs while interviewing experts, J. of Automated Reasoning 6(3):299-317, September 1990.

*[Pierce 1990] W. Pierce, Toward mechanical methods for streamlining proofs, 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. 351-365.

[Pietrzykowski 1970] T. Pietrzykowski, A Language for Computer Assisted Theorem-Proving, Dept. of Appl. Analysis and Comp. Sci, Research Report C5RR 2009, Univ. of Waterloo, Canada, 1970.

[Pietrzykowski 1971a] T. Pietrzykowski, D. Jensen, A complete mechanization of second order logic, Dept. of Appl. Analysis and Comput. Sci., Univ. of Waterloo, Canada, 1971; also Proc. ACM Annual Conf., 1972; also JACM 20(1973):333-364.

[Pietrzykowski 1971b] T. Pietrzykowski, A complete mechanization of w-order type theory, Rep. 2060, Dept. of appl. Analysis and Comput. Sci., Univ. of Waterloo, 1971; also Proc. ACM Annual Conf., 1973.

[Pietrzykowski 1978] T. Pietrzykowski, Mechanical Hypothesis Formation, Res. Rept. CS-78-33, Dept. of Computer Science, Univ. of Waterloo, 1978.

[Pietrzykowski 1982a] T. Pietrzykowski, S. Matwin, Exponential improvement of efficient backtracking: a strategy for plan-based deduction, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 223-239.

[Pietrzykowski 1982b] T. Pietrzykowski, S. Matwin, Exponential improvement of exhaustive backtracking: data structure and implementation, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 240-259.

[Pirotte 1973] A. Pirotte, Automatic theorem proving based on resolution, Annu. Rev. Autom. Program 7(4):201-266, 1973.

[Pitrat 1965] J. Pitrat, Realization of a program which chooses the theorems it proves, Proc. IFIP Congr. 1965, 1965, pp. 324-325.

[Plaisted 1976] D. Plaisted, Theorem proving and semantic trees, PhD thesis, Stanford Univ., 1976.

[Plaisted 1978a] D. Plaisted, A recursively defined ordering for proving termination of term rewriting systems, Tech. Rep. 78-943, Dept. of Comput. Sci, Univ. of Illinois, Urbana-Champaign, September 1978.

[Plaisted 1978b] D. Plaisted, Well-founded orderings for proving termination of systems of rewrite rules, Tech. Rep. 78-932, Dept. of Computer Science, Univ. of Illinois, Urbana-Champaign, July 1978.

[Plaisted 1980a] D.A. Plaisted, Abstraction mappings in mechanical theorem proving, 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. 264-280.

[Plaisted 1980b] D.A. Plaisted, An efficient relevance criterion for mechanical theorem proving, Proc. 1st Natl Conf. on Artificial Intelligence, Stanford Univ. August 1980, pp. 79-83.

[Plaisted 1981] D.A. Plaisted, Theorem proving with abstraction, Artificial Intelligence 16(1):47-108, March 1981.

[Plaisted 1982] D.A. Plaisted, A simplified problem reduction format, Artificial Intelligence 18(2):227-261, March 1982.

[Plaisted 1983] D. Plaisted, An associative path ordering, Tech. Report, Univ. of Illinois, Computer Science Dept., 1983.

[Plaisted 1984a] D.A. Plaisted, An associative path ordering, 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. 123-136.

[Plaisted 1984b] D.A. Plaisted, Using examples, case analysis, and dependency graphs in theorem proving, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 356-374.

[Plaisted 1984c] D.A. Plaisted, The occur-check problem in Prolog, Proc. 1984 Intl. Symp. on Logic Programming, Atlantic City, NJ, 1984, pp. 272-280.

[Plaisted 1984d] D.A. Plaisted, S. Greenbaum, Problem representations for back chaining and equality in resolution theorem proving, Proc. First Annual AI Applications Conf., Denver, CO, December 1984, pp. 417-423.

*[Plaisted 1985a] D.A. Plaisted, The undecidability of self-embedding for term rewriting systems, Information Processing Letters 20(2):61-64, February 1985.

[Plaisted 1985b] D. Plaisted, Semantic confluence tests and completion methods, Information and Control 65(1985):182-215.

[Plaisted 1986a] D.A. Plaisted, A decision procedure for combinations of propositional temporal logic and other specialized theories, J. of Automated Reasoning 2(2):171-190, D. Reidel Publ. Co., Dordrecht, Holland, 1986.

[Plaisted 1986b] D.A. Plaisted, A simple non-termination test for the Knuth-Bendix method, 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. 79-88.

[Plaisted 1986c] D.A. Plaisted, Abstraction using generalization functions, 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. 365-376.

[Plaisted 1986d] D.A. Plaisted, S.A. Greenbaum, A structure-preserving clause form translation, J. Symbolic Computation 2(3):293-304, September 1986.

*[Plaisted 1987] D.A. Plaisted, Non-Horn clause logic programming without contrapositives, Memo. Dept. CS, Univ. North Carolina, 1987; also J. Automated Reasoning 4(3):287-325, September 1988.

*[Plaisted 1988a] D.A. Plaisted, A goal directed theorem prover, 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. 737-737.

*[Plaisted 1988b] D.A. Plaisted, A logic for conditional term rewriting systems, 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. 212-227.

*[Plaisted 1990] D.A. Plaisted, Mechanical theorem proving, In Formal Techniques in Artificial Intelligence: A Sourcebook, ed. R.B. Banerji, Elsevier Science Publishers, Amsterdam, 1990, pp. 269-320.

*[Plaisted 1990a] D.A. Plaisted, A sequent-style model elimination strategy and a positive refinement, J. Automated Reasoning 6(4):389-402, December 1990.

[Plaisted 1990b] D.A. Plaisted, S.-J. Lee, Inference by clause linking, Tech. Report TR90-022, Univ. of North Carolina at Chapel Hill, NC, 1990.

[Pletat 1981] U. Pletat, G. Engels, H.-D. Ehrich, Operational semantics of algebraic specification with conditional equations, Proc. 7th CAAP Conf., Lille, France, 1981.

[Plotkin 1970a] G. Plotkin, Lattice-theoretic properties of subsumption, Memo. MIP-R-77, Univ. of Edinburgh, Scotland, 1970.

[Plotkin 1970b] G.D. Plotkin, A note on inductive generalization, Machine Intelligence 5, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1970.

[Plotkin 1971] G.D. Plotkin, A further note on inductive generalization, Machine Intelligence 6, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, 1971.

[Plotkin 1972] G.D. Plotkin, Building-in equational theories, Machine Intelligence 7, ed. B. Meltzer and D. Michie, Univ. of Edinburgh, 1972, pp. 73-90.

[Plotkin 1977] G.D. Plotkin, LCF considered as a programming language, Theoretical Computer Science 5(1977):223-257.

[Plummer 1977] D. Plummer, Gazing: controlling the use of rewrite rules, PhD thesis, Dept. of AI, Univ. of Edinburgh, 1977; also Research Paper 412.

[Plummer 1984a] D. Plummer, A. Bundy, Gazing: Identifying potentially useful inferences, Working Paper 160, Dept. Artificial Intelligence, Edinburgh, February 1984.

[Plummer 1984b] D. Plummer, RUT: Reconstructed UT Theorem Prover, Working Paper 165, Dept. Artificial Intelligence, Edinburgh, September 1984.

[Plummer 1985a] D. Plummer, An investigation and rational reconstruction of the UT theorem prover, DAI Research Paper 256, Dept. of Artificial Intelligence, Edinburgh, 1985.

[Plummer 1985b] D. Plummer, Gazing: Using the structure of the theory in theorem proving, Working paper 180, Dept. of Artificial Intelligence, Edinburgh, May 1985.

[Plummer 1988] D. Plummer, Gazing: A technique for controlling the use of rewrite rules, PhD thesis, Dept. of Artificial Intelligence, Univ. of Edinburgh, May 1988; also Research Paper 412, Univ. of Edinburgh, Scotland, 1988;

[Poe 1984] M.D. Poe, R. Nasr, J. Potter, J. Slinn, Bibliography on Prolog and logic programming, J. of Logic Programming 1(1):81-99, June 1984.

[Pohl 1969] I. Pohl, Bi-directional and heuristic search in path-problems, PhD thesis, Stanford Univ.; also Slac-Report, No. 104, 1969.

[Pohl 1970] I. Pohl, First results on the effect of error in heuristic search, Machine Intelligence 5, 1970.

[Pohst 1981] M.E. Pohst, D.Y.Y. Yun, On solving systems of algebraic equation via ideal bases and elimination theory, Proc. 1981 ACM Symp. on Symbolic and Algebraic Computation (SYMSAC), 1981, pp. 206-211.

*[Pollock 1990] J.L. Pollock, Interest driven suppositional reasoning, J. Automated Reasoning 6(4):419-461, December 1990.

[Polya 1945] G. Polya, How to Solve it, Princeton Univ. Press, 1945; reprinted Doubleday and Co., Garden City, NY, 1957; 2nd Edition, How to solve it; a new aspect of mathematical method, Princeton Univ. Press, 1973.

[Polya 1954] G. Polya, Induction and analogy in mathematics, Princeton Univ. Press, 1954.

[Polya 1965] G. Polya, Mathematical Discovery (two volumes), John Wiley and Sons Inc., 1965.

*[Ponder 1987] C.G. Ponder, Applications of hashing in algebraic manipulation (an annotated bibliograpy), SIGSAM Bulletin 21(4):10-13, November 1987.

[Ponder 1988] C. Ponder, Augmenting expensive functions in Macsyma with lookup tables, Chapter 9 in Evaluation of "Performance Enhancements" in Algebraic Manipulation Systems, PhD. Diss, Univ. California at Berkeley, Dept. of EECS, also UCB/CSD 88/453, p. 85-100.

[Poole 1984a] D.L. Poole, The logical definition of deduction systems, Research Report CS-84-12, Logic Programming Group, Dept. of Computer Science, Univ. of Waterloo, Waterloo, Canada, June 1984.

[Poole 1984b] D. Poole, Making clausal theorem provers non-clausal, Proc. CSCSI/SCEIO Conf. 1984, Canadian Society for Computational Studies of Intelligence, Univ. of Western Ontario, London, Canada, May 1984; also Research Report CS-85-52, Logic Programming Group, Dept. of Computer Science, Univ. of Waterloo, Waterloo, Canada, December 1985.

[Pople 1973] H.E. Pople, On the mechanization of abductive logic, Proc. 3rd IJCAI, Stanford Univ., 1973, pp. 147-152.

[Popplestone 1967] R.J. Popplestone, Beth-tree methods in automated theorem proving, Machine Intelligence 1, ed. N.L. Collins and D. Michie, American Elsevier, 1967, pp. 31-46.

[Popplestone 1970] R.J. Popplestone, An experiment in automatic induction, Machine Intelligence 5, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, 1970, pp. 203-206.

[Porat 1985] S. Porat, N. Francez, Fairness in term rewriting systems, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 287-300.

[Porat 1986] S. Porat, N. Francez, Full-commutation and fair-termination in equational (and combined) term-rewriting systems, 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. 21-41.

[Posegga 1985] J. Posegga, Using deduction graphs as a representation for resolution proofs, Diploma thesis, Univ. Kaiserslautern, 1986.

*[Potter 1988] Potter, R.C. Potter, D.A. Plaisted, Term rewriting: some experimental results, 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. 435-453.

*[Potschke 1982] D. Potschke, Toward a mathematical theory of analogical reasoning, Proc. ECAI-82, Univ. Paris-Sud, Orsay, France, 12-14 July 1982. pp. 54-59.

[Pratt 1977] V.R. Pratt, A practical decision method for propositional dynamic logic, Proc. 10th Annual ACM Symp. on Theory of Computing, San Diego, CA, 1977, pp. 326-337.

[Prawitz 1960a] D. Prawitz, H. Prawitz, N. Voghera, A mechanical proof procedure and it realization in an electronic computer, JACM 7(1960):102-128; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 202-228.

[Prawitz 1960b] D. Prawitz, An improved proof procedure, Theoria 26(1960):102-139; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 162-201.

[Prawitz 1965] D. Prawitz, Natural Deduction: A proof theoretical study, Almquist and Wiskell, Stockholm, Sweden, 1965.

[Prawitz 1967] D. Prawitz, Completeness and Hauptsatz for second order logic, Theoria 33(1967):246-254.

[Prawitz 1968] D. Prawitz, Hauptsatz for higher order logic, J. Symbolic Logic 33(1968):452-457.

[Prawitz 1969] D. Prawitz, Advances and problems in mechanical proof procedures, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 73-89; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 283-297.

[Prawitz 1970] D. Prawitz, A proof procedure with matrix reduction, Symp. on Automatic Demonstration (Versailles, France), ed. M. Laudet et al., Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 207-214.

*[Pritchard 1990] P. Pritchard, J. Slaney, Computing models of propositional logics (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. 685.

*[Pritchard 1991] P. Pritchard, Algorithms for finding matrix models of propositional calculi, J. Automated Reasoning 7(4):475-487, December 1991.

[PRL 1984] The PRL Staff, PRL: Proof Refinement Logic Programmer's Manual, Computer Science Dept., Cornell Univ., 1984.

[PRL 1985] The PRL Staff, Implementing mathematics with the Nuprl Proof Development System, Computer Science Dept., Cornell Univ., May 1985.

*[Protzen 1992] M. Protzen, Disproving Conjectures, 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. 340-354.

[Przymusinski 1986] T. Przymusinski, Query answering in circumscriptive and closed-world theories, Proc. AAAI-86, 5th Natl. Conf. on Artificial Intelligence, Philadelphia, PA, 11-15 August 1986, pp. 186-190.

*[Przymusinski 1989] T.C. Przymusinski, On the declarative and procedural semantics of logic programs, J. of Automated Reasoning 5(2):167-205, June 1989.

[Psenicnikova 1964] S.V. Psenbicnikova, On an algorithm for the automatic proof of certain theorems in analysis, Izv. Akad. Nauk Azerbaidzan. SSR. Ser. Fiz-Teh. Mat. Nauk, No. 4, pp. 65-67, 1964

*[Puel 1989] L. Puel, Embedding with patterns and associated recursive path ordering, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 371-387.

*[Puel 1990] L. Puel, A. Suarez, Compiling pattern matching by term decomposition, Proc. 1990 ACM Conf. on LISP and Functional Programming (Nice, France, 27-29 June 1990), ACM Press, New York, NY, 1990, pp. 273-281.

[Purdom 1985] P.W. Purdom, C.A. Brown, Fast many-to-one matching algorithms, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 407-416.

[Purdom 1987a] P.W. Purdom, C.A. Brown, Tree matching and simplification, Software - Practice and Experience 17(2):105-115, February 1987.

[Purdom 1987b] P.W. Purdom, Detecting looping simplifications, 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. 54-61.

*[Purushothaman 1989] S. Purushothaman, P.A. Subrahmanyam, Mechanical certification of systolic algorithms, J. Automated Reasoning 5(1):67-91, March 1989.

*[Pym 1990] D. Pym, L. Wallen, Investigations into proof-search in a system of first-order dependent function types, 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. 236-250.

[Qian 1986] Zh. Qian, Sufficient condition for confluent and terminating term rewrite system and its extension to recursively presented term rewriting, PROSPECTRA Study Notes M.1.1.S1-SN-16.2. Univ. of Bremen, November 1986.

[Qian 1987] Zh. Qian, Structured contextual 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. 168-179.

*[Qian 1992] Z. Qian, K. Wang, Higher-order E-unification for arbitrary theories, Proc. Joint Intl. Conf. and Symp. on Logic Programming, ed. K. Apt, The MIT Press, Cambridge, MA, 1992, pp. 52-66.

*[Quaife 1988] A. Quaife, Automated proofs of Lob's theorem and Godel's two incompleteness theorems, J. Automated Reasoning 4(2):219-231, June 1988.

*[Quaife 1989] A. Quaife, Automated development of Tarski' geometry, J. Automated Reasoning 5(1):97-118, March 1989.

[Quaife 1990] A. Quaife, Automated development of fundamental mathematical theories, PhD Dissertation, Univ. of California at Berkeley, 1990.

*[Quaife 1991] A. Quaife, Unsolved problems in elementary number theory, J. of Automated Reasoning 7(2):287-300, June 1991.

[Quine 1952] W.V.O. Quine, The problem of simplifying truth functions, American Math. Monthly 59(1952):521-531.

[Quine 1955] W.V. Quine, A proof procedure for quantification theory, J. of Symbolic Logic 20(June 1955):141-149.

[Quine 1959] W.V.O. Quine, On cores and prime implicants of truth functions, American Math. Monthly 66(1959):755-760.

[Quinland 1968a] J.R. Quinland, E.B. Hunt, A formal deductive problem-solving system, JACM 15(4):625-646, 1968.

[Quinland 1968b] J.R. Quinland, E.B. Hunt, An Experience Gathering Problem-Solving System, Tech. Report 68-1-03, Comp. Sci Group, Univ. of Washington, Seattle, May 1968.

[Quintana 1988] P.J. de la Quintana, Natural deduction based automatic theorem proving for first order modal logics, Research report 88/5, Dept. of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7 2BZ, England, 1988.

[Raatz 1987] S. Raatz, Aspects of a graph-based proof procedure for Horn clauses, PhD thesis, University of Pennsylvania, 1987.

[Rabin 1973] M.O. Rabin, M.J. Fisher, Super-exponential complexity of theorem proving procedures, Proc. AMS SIAM Symp. Appl. Math., AMS, Providence, RI, 1973, pp. 27-42.

*[Rabinov 1988] A. Rabinov, A restriction of factoring in binary resolution, 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. 582-591.

*[Rajasekar 1989] A. Rajasekar, J. Lobo, J. Minker, Weak generalized closed world assumption, J. Automated Reasoning 5(3):293-307, September 1989.

[Ramesh 1986] R. Ramesh, R.M. Verma, T. Krishnaprasad, I.V. Ramakrishnan, Term matching on parallel computers, Tech. Report 86/20, Department of Computer Science, SUNY at Stony Brook, August 1986; also Proc. 14th Intl. Colloquium on Automata, Languages, and Programming (ICALP '87, Karlsruhe, W. Germany, 13-17 July 1987), ed. T. Ottmann, LNCS 267, Springer-Verlag, Berlin, 1987.

[Ramesh 1987] R. Ramesh, I.V. Ramakrishnan, Optimal speedups for parallel pattern matching in trees, 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. 274-285.

*[Ramesh 1990] R. Ramesh, I.V. Ramakrishnan, D.S. Warren, Automata-driven indexing of Prolog clauses, Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages (San Francisco, CA, 17-19 January 1990), ACM, 1990, pp. 281-291.

*[Ramsay 1991] A. Ramsay, Generating relevant models, J. Automated Reasoning 7(3):359-368, September 1991.

*[Randell 1992] D.A. Randell, A.G. Cohn, Z. Cui, Computing transitivity tables: A challenge for automated theorem provers, 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. 786-790.

*[Rao 1987] V.N. Rao, V. Kumar, K. Ramesh, A parallel implementation of iterative-deepening A*, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, pp. 178-182.

[Raph 1984] Karl Mark G. Raph, The Markgraf Karl refutation procedure, Memo-SEKI-MK-84-01, Universitat Kaiserslautern and Univ. of Karlsruhe, W. Germany, January 1984.

[Raphael 1968] B. Raphael, Programming a Robot, Proc. 4th IFIP Congress, North-Holland Publ. Co., Amsterdam, 1968, pp. 135-139.

[Raphael 1969] B. Raphael, Some results about proof by resolution, SIGART Newsletter 14(1969):22-25.

[Raphael 1970] B. Raphael, The frame problem in problem-solving systems, Tech. Note 33, A.I. Group, Stanford Research Inst., Menlo Park, CA, June 1970.

[Raphael 1973] B. Raphael, R. Fikes, R. Waldinger, Research in advanced formal theorem proving techniques, Stanford Research Inst., Menlo Park, CA, August 1973.

[Rasiowa 1977] H. Rasiowa, Algorithmic Logic, Institute of Computer Science Polish Academy of Science, Warsaw, 1977.

[Raulefs 1978a] P. Raulefs, J. Siekmann, Unification of idempotent functions, Internal Report Memo SEKI-78-1, Universitat Karlsruhe, 1978.

[Raulefs 1978b] P. Raulefs, J. Siekmann, P. Szabo, E. Unvericht, A short survey on the state of the art in matching and unification problems, AISB Quarterly issue 32(December 1978):17-21; also SIGSAM Bulletin 13(1979):14-20.

*[Rayna 1987] G. Rayna, REDUCE: Software for Algebraic Computation, Springer-Verlag, NY, 1987.

[Read 1988] S. Read, Proof theory and semantics for relevant logics, Automated Reasoning Project, Australian National Univ., Canberra, ACT.2601, Australia.

[Reboh 1972] R. Reboh, B. Raphael, R.A. Yates, R.E. Kling, C. Velarde, Study of automatic theorem-proving programs, SRI-TN-75, Artificial Intelligence Center, SRI International, Menlo Park, CA, 1972.

[Reckhow 1976] R.A. Reckhow, On the lengths of proofs in the propositional calculus, PhD thesis, Dept. of Computer Science, Univ. of Toronto, 1976.

*[Reddy 1989] U.S. Reddy, Rewriting techniques for program synthesis, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 388-403.

*[Reddy 1990] U.S. Reddy, Term rewriting induction, 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. 162-177.

[Reeves 1983] S.V. Reeves, An introduction semantic tableaux, Dept. of Computer Science, CSM-55, Univ. of Essex, 1983.

[Reeves 1985a] S.V. Reeves, Theorem-proving by semantic tableaux, PhD thesis, Univ. of Birmingham, 1985.

[Reeves 1985b] S.V. Reeves, A note on functional reflexivity in semantic tableaux with partial unification, Dept. of Computer Science and Statistics, Queen Mary College, Univ. of London, June 1985.

*[Reeves 1987a] S. Reeves, Semantic tableaux as a framework for automated theorem-proving, Proc. 1987 AISB Conf., Advances in Artificial Intelligence (Univ. of Edinburgh, 6-10 April 1987), ed. J. Hallam and C. Mellish, John Wiley & Sons, 1987, pp. 125-139.

[Reeves 1987b] S.V. Reeves, Adding equality to semantic tableaux, J. of Automated Reasoning 3(3):225-246, September 1987.

*[Reif 1992] W. Reif, The KIV system: systematic construction of verified software, 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, 753-757.

[Reiter 1969] R. Reiter, The predicate elimination strategy in theorem proving, Dept. of Comput. Sci., Univ. of British Columbia, Vancouver, Canada, 1969; also Proc. 2nd ACM Symp. on Theoretical Computer Sci., 1970, pp. 180-183.

[Reiter 1971] R. Reiter, Two results on ordering for resolution with merging and linear format, JACM 18(October 1971):630-646.

[Reiter 1972] R. Reiter, The use of models in automatic theorem proving, Tech. Report 72-09, Dept. of Computer Science, Univ. of British Columbia, Vancouver, BC, Canada, 1972.

[Reiter 1973] R. Reiter, A semantically guided deductive system for automatic theorem proving, Proc. 3rd IJCAI, Stanford Univ., 1973, pp. 41-46; also IEEE Trans. on Computers C-25(4):328-334, 1976.

[Reiter 1975] R. Reiter, A paradigm for automated formal inference, IEEE Theorem Proving Workshop, Argonne National Lab., IL, June 1975.

[Reiter 1976] R. Reiter, A semantically guided deductive system for automatic theorem proving, IEEE Trans. on Computers C-25(4):328-334, April 1976.

[Reiter 1980] R. Reiter, A logic for default reasoning, Artificial Intelligence 13(1):81-132, April 1980.

[Remy 1981] J.L. Remy, P.A.S. Veloso, An economical method for comparing data type specifications, ACM SIGPLAN 16(5):39-42, May 1981.

[Remy 1982] J.L. Remy, Proving conditional identities by equational case reasoning, rewriting and normalization, Report 82-R-085, CRIN, Nancy, 1982; also Proc. of 1982-83 Research Seminar, LITP, Paris, France, 1983.

[Remy 1983] J.L. Remy, Conditional term rewriting system for abstract data types, Submitted for publication, Univ. of Nancy, France, June 1983.

[Remy 1984] J.L. Remy, H. Zhang, REVEUR 4: A system for validating conditional algebraic specifications of parameterized abstract data types, Rapport 54506, Centre de Recherche en Informatique de Nancy, France, 1984.

*[Remy 1985a] J.L. Remy, H. Zhang, REVEUR 4: A system for validating conditional algebraic specifications of abstract data types, Proc. 6th European Conf. on Artificial Intelligence: Advances in Artificial Intelligence, ECAI-84 (Pisa, Italy, 5-7 September 1984), ed. T. O'Shea, North-Holland, Amsterdam, 1985, pp. 373-382.

[Remy 1985b] J.L. Remy, H. Zhang, Contextual Rewriting, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 46-62.

[Reps 1984] T. Reps, B. Alpern, Interactive proof checking, Proc. 11th ACM Symp. on Principles of Programming Languages (Salt Lake City, Utah, January 1984), ACM, NY, 1984, pp. 36-45.

[Rety 1985b] T.W. Reps, T. Teitelbaum, The synthesizer generator reference manual, Tech. Report TR 84-619, Computer Science Dept., Cornell Univ., Ithaca, NY, August 1985.

[Rety 1985a] P. Rety, C. Kirchner, H. Kirchner, P. Lescanne, NARROWER: A new algorithm for unification and its application to logic programming, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 141-157; also CRIN report 86-R-131, 1986.

[Rety 1987] P. Rety, Improving basic narrowing techniques, 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. 228-241.

[Reynolds 1968] J.C. Reynolds, A generalized resolution principal based upon context-free grammers, Proc. IFIP Congr. 1968, pp. 1405-1411.

[Reynolds 1970] J.C. Reynolds, Transformational systems and the algebraic structure of atomic formulas, Machine Intelligence 5, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, 1970, pp. 135-151.

[Rice 1983] M. Rice, The construction of a complete minimal set of contextual normal forms, Proc. 1st Conf. European Computer Algebra Conf. (EUROCAL '83, London, England), ed. J.A. Van Hulzen, LNCS 162, Springer-Verlag, Berlin, 1983, pp. 255-266.

[Rich 1980] R.P. Rich, Mechanical proof testing, Computer Languages 5(1), 1980, pp. 1-28.

[Rich 1983] E. Rich, Artificial Intelligence, McGraw-Hill, 1983.

[Richards 1989] T. Richards, Clausal form logic: An introduction to the logic of computer reasoning, Addison-Wesley Publ. Co., Sydney, Australia, 1989.

[Richter 1974] M. Richter, A note on paramodulation and the functional reflexive axioms, Technical Report, Univ. of Texas at Austin, 1974.

[Richter 1982] M.M. Richter, Complete and incomplete system of reductions, Informatikfachberichte 57, ed. J. Nehmer, Springer-Verlag, 1982.

[Rissland 1980] E. Rissland, E. Soloway, Generating examples in LIPS: Data and programs, COINS Tech Report 80-07, Amherst Dept. of Computer and Information Sci., Univ. of Mass. at Amherst, 1980.

[Ritchie 1987] B. Ritchie, The design and implementation of an interactive proof editor, PhD thesis, Edinburgh Univ. 1987.

*[Ritchie 1988] B. Ritchie, P. Taylor, The interactive proof editor: An experiment in interactive theorem, ECS-LFCS-88-61, Lab. for Foundations of Computer Science, Dept. of Computer Science, Univ. of Edinburgh, July 1988; also In Current Trends in Hardware Verification and Automated Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, NY, 1989, pp. 303-322.

*[Rittri 1990] M. Rittri, Retrieving library identifiers via equational matching of types, 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. 603-617.

*[Roach 1990] J.W. Roach, R. Sundararajan, L.T. Watson, Replacing unification by constraint satisfaction to improve logic program expressiveness, J. of Automated Reasoning 6(1):51-75, March 1990.

[Robinson 1957] A. Robinson, Proving theorems, as done by man, machine and logician, Summaries of talks presented at the Summer Inst. for Symbolic Logic, Communications Res. Div., Inst. for Defense Analysis, Princeton, NJ, 2nd Edition 1960; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 74-76.

[Robinson 1960] A. Robinson, On the mechanization of the theory of equations, Bull. Res. Council Israel, 9F, 1960, pp. 47-70.

[Robinson 1961] J.A. Robinson, A General Theorem-Proving Program for the IBM 704, Argonne National Lab., Memo No. 6447, November 1961.

[Robinson 1963a] J.A. Robinson, A machine-oriented first-order logic (abstract), J. Symb. Logic 28(1963):302.

[Robinson 1963b] J.A. Robinson, Theorem proving on the computer, JACM 10(2):163-174, April 1963; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 372-383.

[Robinson 1963c] A. Robinson, A basis for the mechanization of the theory of equations, Computer Programming and Formal Systems, ed. Braffort and Hirschberg, North-Holland, Amsterdam, 1963, pp. 95-99.

[Robinson 1964] J.A. Robinson, On Automatic Deduction, Rice Univ., Studies 50, pp. 69-89, 1964.

[Robinson 1965a] J.A. Robinson, Automatic deduction with hyper-resolution, Intl. J. of Computer Mathematics 1(1965):227-234; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 416-423.

[Robinson 1965b] J.A. Robinson, A machine-oriented logic based on the resolution principal, JACM 12(1):23-41, 1965; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 397-415.

[Robinson 1967a] J.A. Robinson, A review of automatic theorem proving, Proc. Annual Symposia in Applied Math. XIX, Amer. Math. Soc., Providence, 1967, pp. 1-18.

[Robinson 1967c] G. Robinson, Dependency of Equality Axioms in Elementary Group Theory, Comp. Group, Tech. Memo No. 53, Stanford Lin. Acc. Center, 1967.

[Robinson 1967d] G. Robinson, L. Shalla, L.T. Wos, Two Inference Rules for FOPC with Equality, AMD Tech. Memo No. 142, Argonne National Laboratory, 1967.

[Robinson 1967e] J.A. Robinson, Heuristic and complete processes in the mech. of theorem proving, in Systems and Computer Science, ed. Hart and Tahusu Univ. of Toronto Press, 1967, pp. 116-124.

[Robinson 1968a] J.A. Robinson, New directions in Mechanical theorem proving, Proc. IFIP Congr. 1968 1, pp. 63-68; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 152-158.

[Robinson 1968b] J.A. Robinson, The generalized resolution principal, Machine Intelligence 3, ed. Dale and Michie, Oliver and Boyd, Edinburgh, 1968, pp. 77-93; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 135-151.

[Robinson 1968c] J.A. Robinson, The Present State of Mechanical Theorem Proving, Proc. 4th Systems Symp., 1968.

[Robinson 1969a] J.A. Robinson, Mechanizing higher order logic, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, 1969.

[Robinson 1969b] G. Robinson, L. Wos, Completeness of paramodulation, Spring 1968 meeting of the Association of Symbolic Logic 34, 1969, p. 160.

[Robinson 1969c] G. Robinson, L. Wos, Paramodulation and theorem-proving in first-order theories with equality, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 135-150; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 298-313.

[Robinson 1970a] J.A. Robinson, A note on mechanizing higher order logic, Machine Intelligence 5, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1970, pp. 123-133.

[Robinson 1970b] G. Robinson, L. Wos, Axiom systems in automatic theorem proving, Symp. on Automatic Demonstration, Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 215-236.

[Robinson 1970c] J.A. Robinson, An overview of mechanical theorem proving, in Theoretical Approaches to Non-Numerical Problem Solving, ed. Banerji and Mesarovic, NY, Springer-Verlag, 1970, pp. 2-20.

*[Robinson 1971a] J.A. Robinson, Building deduction machines, Artificial Intelligence and Heuristic Programming, ed. Findler and Meltzer, American Elsevier, NY, 1971, pp. 3-13.

*[Robinson 1971b] J.A. Robinson, Computational logic: The unification computation, in Machine Intelligence 6, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1971, pp. 63-72.

[Robinson 1976] J.A. Robinson, Fast unification, in Theorem Proving Workshop, Oberwolfach, W. Germany, January 1976.

[Robinson 1979] J.A. Robinson, Logic: Form and function, Edinburgh Univ. Press, Edinburgh, 1979.

[Rolf 1985] N. Rolf, Automated theorem proving methods, Univ. of Oslo, Olso, Norway, BIT 25, 1(1985):51-69.

[Rosen 1973] B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, JACM 20, 1973.

*[Ross 1988] K.S. Ross, R.W. Topor, Inferring negative information from disjunctive databases, J. Automated Reasoning 4(4):397-424, December 1988.

*[Roy 1989] P. Van Roy, An intermediate language to support Prolog's unification, Logic Programming: Proc. of the North American Conf., 1989, Vol. 2, ed. E.L. Lusk, R.A. Overbeek, MIT Press, 1989, pp. 1148-1164.

[Rubin 1976] N. Rubin, A hierarchical technique for mechanical theorem proving and its application to programming language design., Courant Comput. Sci. Report 10, Courant Inst. of Mathematical Sci., NY, 1976.

[Rudnicki 1987] P. Rudnicki, Obvious inferences, J. of Automated Reasoning 3(4):383-393, December 1987.

[Rush 1986] T. Rush, D. Coleman, Combining pattern-matching algorithms, Tech. Report HPL-BRC-TR-86-036, Hewlett-Packard Laboratories, Bristol, UK, December 1986.

*[Rush 1988] T. Rush, D. Coleman, Architecture for conditional term rewriting, 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. 266-278.

[Rusinowitch 1985] M. Rusinowitch, Path of subterms and recursive decomposition ordering revisited, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 225-240; also J. of Symbolic Computation 3(1 and 2):117-117, February/April 1987.

[Rusinowitch 1987] M. Rusinowitch, Theorem proving with resolution and superposition: an extension of Knuth and Bendix procedure as a complete set of inference rules, Internal Report 87-R-128, CRIN, Nancy, France, 1987.

[Rusinowitch 1987] M. Rusinowitch, On termination of the direct sum of term rewriting systems, Information Processing Letters 26(1987):65-70.

*[Russell 1992] S. Russell, Efficient memory-bounded search methods, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 3-7 August 1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992, pp. 1-5.

[Russinoff 1983] D.M. Russinoff, A mechanical proof of Wilson's theorem, Dept. of Computer Sciences, Univ. of Texas at Austin, 1983.

[Russinoff 1985] D.M. Russinoff, An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem, J. of Automated Reasoning 1(2):121-139, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Russinoff 1989] D.M. Russinoff, A verified Prolog compiler for the Warren abstract machine, MCC Technical Report Number ACT-ST-292-89, Microelectronics and Computer Techology Corporation, Austin, TX, July 1989.

[Ruzicka 1989] P. Ruzicka, I. Privara, An almost linear Robinson unification algorithm, Acta Informat. 27(1989):61-71.

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