ORA Canada Bibliography of Automated Deduction: Authors O to R
[O'Donnell 1977] M.J. O'Donnell, Computing in systems described
by equations, LNCS 58, SpringerVerlag, Berlin, 1977.
[O'Donnell 1985] M.J. O'Donnell, Equational logic as a
programming language, MIT Press, Cambridge, MA, 1985.
[O'Donnell 1987] M.J. O'Donnell, Termrewriting implementation
of equational logic programming, Proc. 2nd Intl. Conf. on
Rewriting Techniques and Applications (Bordeaux, France, 2527 May
1987), ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987,
pp. 112.
[Ogawa 1979] H. Ogawa, T. Kitahashi, K. Tanaka, The theorem
prover using a parallel processing system, Proc. 6th IJCAI, Tokyo,
August 1979, pp. 665667.
*[O'Hearn 1989a] P. O'Hearn, Z. Stachniak, A resolution
framework for finitelyvalued firstorder logics, 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. 6981; also J.
Symbolic Comput. 13(3):235254, March 1992.
[O'Hearn 1989b] P. O'Hearn, Z. Stachniak, A note on theorem
proving strategies for resolution counterparts of finitelyvalued
logic, Proc. Internat. Symp. on Symbolic and Algebraic
Computation, Portland, pp. 364372, 1989.
[Ohlbach 1982] H.J. Ohlbach, The Markgraf Karl refutation
procedure: The logic engine, Interner Bericht 24/82, Memo
SEKI8211, 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 SEKI83V, Institut fur Informatik I, Universitat
Karlsruhe, W. Germany, 1983. also Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 496508.
[Ohlbach 1985a] H.J. Ohlbach, M. SchmidtSchauss, The lion and
the unicorn, J. of Automated Reasoning 1(3):327332, D. Reidel
Publ. Co., Dordrecht, Holland, 1985.
[Ohlbach 1985b] H.J. Ohlbach, Predicate logic hacker tricks, J.
of Automated Reasoning 1(4):435440, D. Reidel Publ. Co.,
Dordrecht, Holland, 1985.
[Ohlbach 1985c] H.J. Ohlbach, Theory unification in abstract
clause graphs, Proc. GWAI85, 9th German Workshop on Artificial
Intelligence, Dassel/Solling (2327 September 1985),
InformatikFachberichte 118, ed. H. Stoyan, SpringerVerlag,
Berlin, 1985, pp. 77100.
*[Ohlbach 1986] H.J. Ohlbach, The semantic clause graph
procedure  A first overview, GWAI86 und 2. Osterreichische
ArtificialIntelligenceTagung (Ottenstein/Niederosterreich, 2226
September 1986), InformatikFachberichte 124, SpringerVerlag,
Berlin, 1986, pp. 218229.
[Ohlbach 1987] H.J. Ohlbach, Link inheritance in abstract clause
graphs, J. of Automated Reasoning 3(1):134, March 1987.
*[Ohlbach 1988a] H.J. Ohlbach, A resolution calculus for modal
logics, SEKI Report SR8808, Universitat Kaiserslautern, 1988.
also 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. 500516.
[Ohlbach 1988b] H.J. Ohlbach, J. Siekmann, Using automated
reasoning techniques for deductive databases, SEKI Report
SR8806, Universitat Kaiserslautern, 1988.
[Ohlbach 1989a] H.J. Ohlbach, Context Logic, SEKI Report
SR8908, Fachbereich Informatik, Universitat Kaiserslautern,
Kaiserslautern, Germany, 1989.
*[Ohlbach 1989b] H.J. Ohlbach, Context Logic  An
Introduction, Proc. 13 German Workshop on Artificial Intelligence
(GWAI89, Eringerfeld, 1822 September 1989), ed. D. Metzing,
SpringerVerlag, Berlin, 1989, pp. 2736.
*[Ohlbach 1990a] H.J. Ohlbach, A. Herzig, Compilation techniques
for logics (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. 683.
*[Ohlach 1990b] H.J. Ohlbach, Abstraction tree indexing for
terms, Proc. 9th ECAI (Stockholm, Sweden, 610 August 1990), ed.
L.C. Aiello, Pitman Publishing, London, 1990, pp. 479484.
[Ohlach 1990c] H.J. Ohlbach, Compilation of recursive
twoliteral 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
COMP8640, 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, 810 July 1987), ed. S.
Kaplan and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin,
1988, pp. 179196.
[Omodeo 1982] E.G. Omodeo, The linked conjunct method for
automatic deduction and related search techniques, Comput. and
Math. with Appl. 8(3):185203, 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, 1519 December
1986), ed. M. Boscarol, L.C. Aiello, and G. Levi, LNCS 306,
SpringerVerlag, 1988, pp. 201218.
*[Omodeo 1990] E. Omodeo, F. Parlamento, A. Policriti, Truth
tables for a combinatorial kernel of set theories, Proc. 9th ECAI
(Stockholm, Sweden, 610 August 1990), ed. L.C. Aiello, Pitman
Publishing, London, 1990, pp. 485490.
[Oppacher 1986a] F. Oppacher, E. Suen, Controlling deduction
with proof condensation and heuristics, Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 384393.
[Oppacher 1986b] F. Oppacher, E. Suen, An efficient
tableaubased theorem prover, Proc. 6th Canadian Conf. on
Artificial Intelligence, Ecole Polytechnique de Montreal,
Montreal, Canada, May 1986, pp. 3135.
*[Oppacher 1988] F. Oppacher, E. Suen, HARP: A tableaubased
theorem prover, J. of Automated Reasoning 4(1):69100, 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.
114119.
[Oppen 1978] D. Oppen, Reasoning about recursively defined data
structures, CS Report STANCS78678, Stanford Univ., 1978; Proc.
5 ACM Symp. POPL, 1978, pp. 151157.
[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):291302.
[Orekov 1971] V.P. Orekov, On nonlengthening applications of
equality rules, Seminars in Mathematics 16, V.A. Steklov Mathem.
Institute, Leningrad, Consultants Bureau, NYLondon, 1971, pp.
7779.
[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):115, Poland, 1978.
[Orlowska 1980] E. Orlowska, Resolution systems and their
applications, I and II, Fundamenta Informaticae, pp. 235267,
333362, Poland, 1980.
[Otto 1985a] F. Otto, Deciding algebraic properties of monoids
presented by finite ChurchRosser Thue systems, Proc. 1st Conf.
Rewriting Techniques and Applications (Dijon, France, 2022 May
1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin,
1985. pp. 95106.
[Otto 1985b] F. Otto, Elements of finite order for finite
monadic ChurchRosser Thue systems. Transactions of the American
Math. Soc. 291(1985):629637.
[Otto 1985c] F. Otto, Decision problems and their complexity for
monadic ChurchRosser 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, 2527 May 1987), ed. P.
Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987, pp. 145155.
*[Otto 1989] F. Otto, Restrictions of congruences generated by
finite canonical stringrewriting systems, Proc. 3rd Intl. Conf.
Rewriting Techniques and Applications (Chapel Hill, North
Carolina, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 359370.
[Overbeek 1974] R.A. Overbeek, A new class of automated
theoremproving algorithms, JACM 21(1974):191200.
[Overbeek 1975] R.A. Overbeek, An implementation of
hyperresolution, Computers and Mathematics with Applications
1(1975):201214.
[Overbeek 1976] R. Overbeek, J. McCharen, L. Wos, Complexity and
related enhancements for automated theoremproving programs,
Computers and Mathematics with Applications 2(1A):116, 1976.
[Overbeek 1980] R.A. Overbeek, E.L. Lusk, Data structures and
control architecture for implementation of theoremproving
programs, Proc. 5th Conf. on Automated Deduction (Les Arcs,
France, 811 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87,
SpringerVerlag, 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 TheoremProving Method, Dept. of Machine
Intelligence and Perception, Univ. of Edinburgh, Res. Memo, No.
MIPR43, 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 TR85007, 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
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 748752.
[Oyamaguchi 1986] M. Oyamaguchi, Sufficient sequentiality: a
decidable condition for callbyneed computations in term
rewriting systems, COMP8638, 1986.
[Oyamaguchi 1987] M. Oyamaguchi, The ChruchRosser property for
ground termrewriting systems is decidable, Tech. Report, Faculty
of Engineering, Mie University, Tsu 514, Japan, 1987; Theoretical
Computer Science 49(1): 4380, 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 (CADE10, Kaiserslautern, FRG, July
1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 456469.
[Padawitz 1983] P. Padawitz, Correctness, completeness and
consistency of equational data type specifications, Dissertation,
Report No. 8315, FB 20, TU Berlin, 1983.
*[Padawitz 1986] P. Padawitz, Horn clause specifications:
Reduction and narrowing, MIP8601, Universitat Passau, Fakultat
fur Mathematik und Informatik, February 1986.
[Padawitz 1987a] P. Padawitz, Strategycontrolled reduction and
narrowing, Proc. 2nd Intl. Conf. on Rewriting Techniques and
Applications (Bordeaux, France, 2527 May 1987), ed. P. Lescanne,
LNCS 256, SpringerVerlag, Berlin, 1987, pp. 242255.
*[Padawitz 1987b] P. Padawitz, ECDS  A rewrite rule based
interpreter for a programming language with abstraction and
communication, Report MIP8703, Fakultat fur Mathematik und
Informatik, Universitat Passau, 1987.
*[Padawitz 1988a] P. Padawitz, Inductive proofs of
constructorbased Horn clauses, Report MIP8810, 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,
SpringerVerlag, Berlin, 1988.
[Padawitz 1988c] P. Padawitz, Can inductive proofs be automated?
EATCS Bulletin 35(1988): 163170.
[Padawitz 1988d] P. Padawitz, Reduction and narrowing for Horn
clause theories, Report, Universitat Passau, 1988; also Comput. J.
34(1):4251, February 1991.
*[Padawitz 1989a] P. Padawitz, Inductive Expansion, MIP8907,
Fakultat fur Mathematik und Informatik, Universitat Passau, April
1989.
[Padawitz 1989b] P. Padawitz, Can inductive proofs be automated?
Part II. EATCS Bulletin 37(1989): 168174.
[Padawitz 1989c] P. Padawitz, On goal and term reduction
calculi, Proc. 1st German Workshop on Term Rewriting, SEKI Report
SR8902, Universitat Kaiserslautern, 1989.
[Padawitz 1990] P. Padawitz, Horn logic and rewriting for
functional and logic program design, Report MIP9002, 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):27103, March 1991.
*[Padawitz 1991] P. Padawitz, Reduction and Narrowing for Horn
clause theories, The Computer Journal 34(1):4251, 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. AitKaci, M. Nivat, Academic Press, Inc., San
Diego, 1989, pp. 369410.
[Pankov 1978] P.S. Pankow, Composite method of proving some
theorems in mathematical analysis with the aid of electronic
computers, Kibernetika 14(3):119125, 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):221251.
*[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):271284, 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, mNEVER user's manual,
TR87542013, I.P. Sharp Associates Limited, November 1987.
*[Pase 1988] B. Pase, S. Kromodimoeljo, mNEVER System Summary,
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. 738739.
*[Pase 1989] B. Pase, M. Saaltink, Formal verification in
mEVES, In Current Trends in Hardware Verification and Automated
Theorem Proving, ed. G. Birtwistle and P.A. Subrahmanyam,
SpringerVerlag, NY, 1989, pp. 268302.
[Pastre 1978] D. Pastre, Automatic theorem proving in set
theory, Artificial Intelligence 10(1):127, NorthHolland, 1978.
*[Pastre 1982] D. Pastre, A language for expressing mathematical
knowledge in automatic theorem proving, Proc. ECAI82, ParisSud,
Orsay, France, 1214 July 1982, pp. 116118.
[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):257318.
*[PatelSchneider 1990] P.F. PatelSchneider, A decidable
firstorder logic for knowledge representation, J. Automated
Reasoning 6(4):361388, December 1990.
[Paterson 1978] M.S. Paterson, M.N. Wegman, Linear Unification,
J. of Computer and Systems Sciences 16(2):158167, 1978.
[Paul 1984a] E. Paul, A new interpretation of the resolution
principle, Proc. 7th Intl. Conf. on Automated Deduction (CADE7,
Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, SpringerVerlag,
NY, 1984, pp. 333355.
[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. 211225.
*[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, 13 April 1985), Vol. 2:
Research Contributions, ed. B.F. Caviness, LNCS 204,
SpringerVerlag, Berlin, pp. 363377; also Theoretical Computer
Science 44(2):127153, 1986.
[Paul 1985b] E. Paul, Equational methods in first order
predicate calculus, J. of Symbolic Computation 1(1):729, 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 higherorder implementation of
rewriting, NorthHolland, Science of Computer Programming
3(1983):119149.
[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. 197214, 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):143169.
[Paulson 1985a] L.C. Paulson, Lessons learned from LCF: A survey
of natural deduction proofs, The Computer J. 28(5):474479,
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
higherorder resolution, Tech. Report 82, Univ. of Cambridge,
Computer Laboratory, 1985; also J. of Logic Programming
3(1986):237258.
*[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):6374, D. Reidel Publ. Co., Dordrecht,
Holland, 1986.
*[Paulson 1986a] L.C. Paulson, Natural deduction as higherorder
resolution, J. of Logic Programming 3(3):237258, October 1986;
also Pattern Recognition Letters 5(3):237258, March 1987.
[Paulson 1986b] L.C. Paulson, Constructing recursion operators
in intuitionistic type theory, J. of Symbolic Computation
2(1986):325355.
[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
higherorder logic, Univ. Cambridge Technical Report R113, 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):363397,
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
(CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R.
Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp. 772773.
[Paulson 1988d] L.C. Paulson, Higherorder 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, AddisonWesley Publishing Company,
1984.
*[Pearl 1987] J. Pearl, R.E. Korf, Search techniques, Annual
Review of Computer Science, Vol. 2, 1987. pp. 451467.
[Pedersen 1981] J. Pedersen, M. Stickel, Complete sets of
reductions for some equational theories, JACM 28(1981):233264.
*[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, 13 April 1985), Vol. 2:
Research Contributions, ed. B.F. Caviness, LNCS 204,
SpringerVerlag, Berlin, pp. 422423.
*[Pedersen 1989] J. Pedersen, Morphocompletion for onerelation
monoids, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 574578.
[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):6168, 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 (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 476495.
*[Pelin 1988] A. Pelin, Computing with conditional rewrite
rules, 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. 197211.
[Pelletier 1982] F.J. Pelletier, Completely nonclausal,
completely heuristically driven, automatic theorem proving, M.Sc.
Thesis, Tech. Report TR827, Dept. of Computing Science, Univ. of
Alberta, Edmonton, Alberta, 1982.
[Pelletier 1986a] F.J. Pelletier, Seventyfive problems for
testing automatic theorem provers, J. of Automated Reasoning
2(2):191216, D. Reidel Publ. Co., Dordrecht, Holland, 1986; also
``Errata,'' J. of Automated Reasoning 1988, pp. 235236.
[Pelletier 1986b] F.J. Pelletier, THINKER, Proc. 8th Intl. Conf.
on Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 701702.
[Pelletier 1987] F.J. Pelletier, Further developments in
THINKER, an authomated theorem prover, Tech. Report TRARP16.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 (IJCAI91, Darling Harbour, Sydney, Australia,
2430 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp.
10391045.
[Pelletier 1993a] F.J. Pelletier, Automated Modal Logic Theorem
Proving in THINKER. Tech Report TR 9314, 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. 291308.
(source: F.J. Pelletier)
[Pereira 1978] L.M. Pereira, F.C.N. Pereira, D.H.D. Warren,
User's guide to DEC system10 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, 811 July 1980), ed. W. Bibel and R. Kowalski, LNCS
87, SpringerVerlag, Berlin, 1980.
[Pereira 1985] F. Pereira, Logic programming, J. of Automated
Reasoning 1(1):912, 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. AitKaci, M. Nivat, Academic Press, Inc., San Diego, 1989,
pp. 275296.
[Peterson 1976] G.E Peterson, Theorem proving with lemmas, JACM
23(4):573581, 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):233264, 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, 119122.
[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. 8789; also SIAM J. of Computing 12(1):82100, 1983.
[Peterson 1981] G.E. Peterson, M.E. Stickel, Complete sets of
reductions for some equational theories, JACM 28(2):233264, 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):82100, February 1983.
*[Peterson 1990a] G.E. Peterson, Complete sets of reduction with
constraints, 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. 381395.
*[Peterson 1990b] G.E. Peterson, Solving term inequalties, Proc.
8th National Conf. on Artificial Intelligence (AAAI90, July
29August 3, 1990), AAAI Press/MIT Press, 1990, pp. 258263.
[Pevac 1985] I. Pevac, Heuristic for avoiding skolemization in
theorem proving, Publ. Inst. Math. 38(52), Beograd (N.S.), 1985,
pp. 207213.
[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 nonanalytic proofs,
Proc. 7th Intl. Conf. on Automated Deduction (CADE7, Napa, CA,
May 1984), ed. R.E. Shostak, LNCS 170, SpringerVerlag, NY, 1984,
pp. 394413.
[Pfenning 1987] F. Pfenning, Proof transformations in
higherorder logic, PhD thesis, Dept. of Mathematics,
CarnegieMellon Univ., January 1987.
*[Pfenning 1988] F. Pfenning, Single axioms in the implicational
propositional calculus, 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.
710713.
*[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, 58 June 1989), IEEE
Computer Society Press, 1989, pp. 313322.
*[Pfenning 1990] F. Pfenning, D. Nesmith, Presenting intuitive
deductions via symmetric simplification, 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. 336350.
*[Pfenning 1991] F. Pfenning, Unification and antiunification
in the calculus of constructions, 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.
7485.
[Pfenning 1992] F. Pfenning, E. Rohwedder, Implementing the
metatheory of deductive systems, 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. 537551.
[Phyushevichene 1971] A. Yo Phyushevichene, Elimination of
CutType Rules in Axiomatic Theories with Equality, Seminars in
Mathematics 16, V.A. Steklov Mathem. Institute, Leningrad,
Consultants Bureau, NYLondon, 1971, pp. 9094.
*[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):299317, September 1990.
*[Pierce 1990] W. Pierce, Toward mechanical methods for
streamlining proofs, 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. 351365.
[Pietrzykowski 1970] T. Pietrzykowski, A Language for Computer
Assisted TheoremProving, 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):333364.
[Pietrzykowski 1971b] T. Pietrzykowski, A complete mechanization
of worder 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. CS7833, Dept. of Computer Science, Univ.
of Waterloo, 1978.
[Pietrzykowski 1982a] T. Pietrzykowski, S. Matwin, Exponential
improvement of efficient backtracking: a strategy for planbased
deduction, Proc. 6th Conf. on Automated Deduction, ed. D.
Loveland, LNCS 138, SpringerVerlag, Berlin, 1982, pp. 223239.
[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, SpringerVerlag, Berlin, 1982, pp. 240259.
[Pirotte 1973] A. Pirotte, Automatic theorem proving based on
resolution, Annu. Rev. Autom. Program 7(4):201266, 1973.
[Pitrat 1965] J. Pitrat, Realization of a program which chooses
the theorems it proves, Proc. IFIP Congr. 1965, 1965, pp. 324325.
[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. 78943,
Dept. of Comput. Sci, Univ. of Illinois, UrbanaChampaign,
September 1978.
[Plaisted 1978b] D. Plaisted, Wellfounded orderings for proving
termination of systems of rewrite rules, Tech. Rep. 78932, Dept.
of Computer Science, Univ. of Illinois, UrbanaChampaign, July
1978.
[Plaisted 1980a] D.A. Plaisted, Abstraction mappings in
mechanical theorem proving, Proc. 5th Conf. on Automated Deduction
(Les Arcs, France, 811 July 1980), ed. W. Bibel and R. Kowalski,
LNCS 87, SpringerVerlag, Berlin, 1980, pp. 264280.
[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. 7983.
[Plaisted 1981] D.A. Plaisted, Theorem proving with abstraction,
Artificial Intelligence 16(1):47108, March 1981.
[Plaisted 1982] D.A. Plaisted, A simplified problem reduction
format, Artificial Intelligence 18(2):227261, 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. 123136.
[Plaisted 1984b] D.A. Plaisted, Using examples, case analysis,
and dependency graphs in theorem proving, Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 356374.
[Plaisted 1984c] D.A. Plaisted, The occurcheck problem in
Prolog, Proc. 1984 Intl. Symp. on Logic Programming, Atlantic
City, NJ, 1984, pp. 272280.
[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. 417423.
*[Plaisted 1985a] D.A. Plaisted, The undecidability of
selfembedding for term rewriting systems, Information Processing
Letters 20(2):6164, February 1985.
[Plaisted 1985b] D. Plaisted, Semantic confluence tests and
completion methods, Information and Control 65(1985):182215.
[Plaisted 1986a] D.A. Plaisted, A decision procedure for
combinations of propositional temporal logic and other specialized
theories, J. of Automated Reasoning 2(2):171190, D. Reidel Publ.
Co., Dordrecht, Holland, 1986.
[Plaisted 1986b] D.A. Plaisted, A simple nontermination test
for the KnuthBendix method, Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 7988.
[Plaisted 1986c] D.A. Plaisted, Abstraction using generalization
functions, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 365376.
[Plaisted 1986d] D.A. Plaisted, S.A. Greenbaum, A
structurepreserving clause form translation, J. Symbolic
Computation 2(3):293304, September 1986.
*[Plaisted 1987] D.A. Plaisted, NonHorn clause logic
programming without contrapositives, Memo. Dept. CS, Univ. North
Carolina, 1987; also J. Automated Reasoning 4(3):287325,
September 1988.
*[Plaisted 1988a] D.A. Plaisted, A goal directed theorem prover,
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. 737737.
*[Plaisted 1988b] D.A. Plaisted, A logic for conditional term
rewriting systems, 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.
212227.
*[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.
269320.
*[Plaisted 1990a] D.A. Plaisted, A sequentstyle model
elimination strategy and a positive refinement, J. Automated
Reasoning 6(4):389402, December 1990.
[Plaisted 1990b] D.A. Plaisted, S.J. Lee, Inference by clause
linking, Tech. Report TR90022, 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, Latticetheoretic properties of
subsumption, Memo. MIPR77, 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, Buildingin equational theories,
Machine Intelligence 7, ed. B. Meltzer and D. Michie, Univ. of
Edinburgh, 1972, pp. 7390.
[Plotkin 1977] G.D. Plotkin, LCF considered as a programming
language, Theoretical Computer Science 5(1977):223257.
[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):8199, June 1984.
[Pohl 1969] I. Pohl, Bidirectional and heuristic search in
pathproblems, PhD thesis, Stanford Univ.; also SlacReport, 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. 206211.
*[Pollock 1990] J.L. Pollock, Interest driven suppositional
reasoning, J. Automated Reasoning 6(4):419461, 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):1013, 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. 85100.
[Poole 1984a] D.L. Poole, The logical definition of deduction
systems, Research Report CS8412, Logic Programming Group, Dept.
of Computer Science, Univ. of Waterloo, Waterloo, Canada, June
1984.
[Poole 1984b] D. Poole, Making clausal theorem provers
nonclausal, Proc. CSCSI/SCEIO Conf. 1984, Canadian Society for
Computational Studies of Intelligence, Univ. of Western Ontario,
London, Canada, May 1984; also Research Report CS8552, 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. 147152.
[Popplestone 1967] R.J. Popplestone, Bethtree methods in
automated theorem proving, Machine Intelligence 1, ed. N.L.
Collins and D. Michie, American Elsevier, 1967, pp. 3146.
[Popplestone 1970] R.J. Popplestone, An experiment in automatic
induction, Machine Intelligence 5, ed. B. Meltzer and D. Michie,
Edinburgh Univ. Press, 1970, pp. 203206.
[Porat 1985] S. Porat, N. Francez, Fairness in term rewriting
systems, Proc. 1st Conf. Rewriting Techniques and Applications
(Dijon, France, 2022 May 1985), ed. J.P. Jouannaud, LNCS 202,
SpringerVerlag, Berlin, 1985. pp. 287300.
[Porat 1986] S. Porat, N. Francez, Fullcommutation and
fairtermination in equational (and combined) termrewriting
systems, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 2141.
[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 (CADE9, Argonne, Illinois, 2326 May 1988),
ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag, Berlin,
1988, pp. 435453.
*[Potschke 1982] D. Potschke, Toward a mathematical theory of
analogical reasoning, Proc. ECAI82, Univ. ParisSud, Orsay,
France, 1214 July 1982. pp. 5459.
[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. 326337.
[Prawitz 1960a] D. Prawitz, H. Prawitz, N. Voghera, A mechanical
proof procedure and it realization in an electronic computer, JACM
7(1960):102128; also Automation of Reasoning  Classical Papers
on Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 202228.
[Prawitz 1960b] D. Prawitz, An improved proof procedure, Theoria
26(1960):102139; also Automation of Reasoning  Classical Papers
on Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 162201.
[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):246254.
[Prawitz 1968] D. Prawitz, Hauptsatz for higher order logic, J.
Symbolic Logic 33(1968):452457.
[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. 7389; also
Automation Of Reasoning  Classical Papers On Computational Logic,
Vol. II, 19671970, ed. J. Siekmann And G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 283297.
[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, SpringerVerlag,
Berlin, 1970, pp. 207214.
*[Pritchard 1990] P. Pritchard, J. Slaney, Computing models of
propositional logics (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. 685.
*[Pritchard 1991] P. Pritchard, Algorithms for finding matrix
models of propositional calculi, J. Automated Reasoning
7(4):475487, 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 (CADE11, Saratoga Springs, NY,
USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial
Intelligence 607, SpringerVerlag, Berlin, 1992, pp. 340354.
[Przymusinski 1986] T. Przymusinski, Query answering in
circumscriptive and closedworld theories, Proc. AAAI86, 5th
Natl. Conf. on Artificial Intelligence, Philadelphia, PA, 1115
August 1986, pp. 186190.
*[Przymusinski 1989] T.C. Przymusinski, On the declarative and
procedural semantics of logic programs, J. of Automated Reasoning
5(2):167205, 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. FizTeh. Mat. Nauk, No. 4, pp. 6567, 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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
371387.
*[Puel 1990] L. Puel, A. Suarez, Compiling pattern matching by
term decomposition, Proc. 1990 ACM Conf. on LISP and Functional
Programming (Nice, France, 2729 June 1990), ACM Press, New York,
NY, 1990, pp. 273281.
[Purdom 1985] P.W. Purdom, C.A. Brown, Fast manytoone matching
algorithms, Proc. 1st Conf. Rewriting Techniques and Applications
(Dijon, France, 2022 May 1985), ed. J.P. Jouannaud, LNCS 202,
SpringerVerlag, Berlin, 1985. pp. 407416.
[Purdom 1987a] P.W. Purdom, C.A. Brown, Tree matching and
simplification, Software  Practice and Experience 17(2):105115,
February 1987.
[Purdom 1987b] P.W. Purdom, Detecting looping simplifications,
Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications
(Bordeaux, France, 2527 May 1987), ed. P. Lescanne, LNCS 256,
SpringerVerlag, Berlin, 1987, pp. 5461.
*[Purushothaman 1989] S. Purushothaman, P.A. Subrahmanyam,
Mechanical certification of systolic algorithms, J. Automated
Reasoning 5(1):6791, March 1989.
*[Pym 1990] D. Pym, L. Wallen, Investigations into proofsearch
in a system of firstorder dependent function types, 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. 236250.
[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.S1SN16.2.
Univ. of Bremen, November 1986.
[Qian 1987] Zh. Qian, Structured contextual rewriting, Proc. 2nd
Intl. Conf. on Rewriting Techniques and Applications (Bordeaux,
France, 2527 May 1987), ed. P. Lescanne, LNCS 256,
SpringerVerlag, Berlin, 1987, pp. 168179.
*[Qian 1992] Z. Qian, K. Wang, Higherorder Eunification for
arbitrary theories, Proc. Joint Intl. Conf. and Symp. on Logic
Programming, ed. K. Apt, The MIT Press, Cambridge, MA, 1992, pp.
5266.
*[Quaife 1988] A. Quaife, Automated proofs of Lob's theorem and
Godel's two incompleteness theorems, J. Automated Reasoning
4(2):219231, June 1988.
*[Quaife 1989] A. Quaife, Automated development of Tarski'
geometry, J. Automated Reasoning 5(1):97118, 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):287300, June 1991.
[Quine 1952] W.V.O. Quine, The problem of simplifying truth
functions, American Math. Monthly 59(1952):521531.
[Quine 1955] W.V. Quine, A proof procedure for quantification
theory, J. of Symbolic Logic 20(June 1955):141149.
[Quine 1959] W.V.O. Quine, On cores and prime implicants of
truth functions, American Math. Monthly 66(1959):755760.
[Quinland 1968a] J.R. Quinland, E.B. Hunt, A formal deductive
problemsolving system, JACM 15(4):625646, 1968.
[Quinland 1968b] J.R. Quinland, E.B. Hunt, An Experience
Gathering ProblemSolving System, Tech. Report 68103, 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 graphbased proof procedure
for Horn clauses, PhD thesis, University of Pennsylvania, 1987.
[Rabin 1973] M.O. Rabin, M.J. Fisher, Superexponential
complexity of theorem proving procedures, Proc. AMS SIAM Symp.
Appl. Math., AMS, Providence, RI, 1973, pp. 2742.
*[Rabinov 1988] A. Rabinov, A restriction of factoring in binary
resolution, 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. 582591.
*[Rajasekar 1989] A. Rajasekar, J. Lobo, J. Minker, Weak
generalized closed world assumption, J. Automated Reasoning
5(3):293307, 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, 1317 July 1987),
ed. T. Ottmann, LNCS 267, SpringerVerlag, 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, 2527 May
1987), ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987,
pp. 274285.
*[Ramesh 1990] R. Ramesh, I.V. Ramakrishnan, D.S. Warren,
Automatadriven indexing of Prolog clauses, Conf. Record 17th
Annual ACM Symp. on Principles of Programming Languages (San
Francisco, CA, 1719 January 1990), ACM, 1990, pp. 281291.
*[Ramsay 1991] A. Ramsay, Generating relevant models, J.
Automated Reasoning 7(3):359368, 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 (CADE11, Saratoga
Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in
Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
786790.
*[Rao 1987] V.N. Rao, V. Kumar, K. Ramesh, A parallel
implementation of iterativedeepening A*, Proc. 6th Natl Conf. on
Artificial Intelligence (AAAI 87), Seattle, Washington, 1317 July
1987, pp. 178182.
[Raph 1984] Karl Mark G. Raph, The Markgraf Karl refutation
procedure, MemoSEKIMK8401, Universitat Kaiserslautern and
Univ. of Karlsruhe, W. Germany, January 1984.
[Raphael 1968] B. Raphael, Programming a Robot, Proc. 4th IFIP
Congress, NorthHolland Publ. Co., Amsterdam, 1968, pp. 135139.
[Raphael 1969] B. Raphael, Some results about proof by
resolution, SIGART Newsletter 14(1969):2225.
[Raphael 1970] B. Raphael, The frame problem in problemsolving
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 SEKI781, 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):1721; also
SIGSAM Bulletin 13(1979):1420.
*[Rayna 1987] G. Rayna, REDUCE: Software for Algebraic
Computation, SpringerVerlag, 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 theoremproving programs, SRITN75,
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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 388403.
*[Reddy 1990] U.S. Reddy, Term rewriting induction, 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. 162177.
[Reeves 1983] S.V. Reeves, An introduction semantic tableaux,
Dept. of Computer Science, CSM55, Univ. of Essex, 1983.
[Reeves 1985a] S.V. Reeves, Theoremproving 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 theoremproving, Proc. 1987 AISB Conf., Advances in
Artificial Intelligence (Univ. of Edinburgh, 610 April 1987), ed.
J. Hallam and C. Mellish, John Wiley & Sons, 1987, pp.
125139.
[Reeves 1987b] S.V. Reeves, Adding equality to semantic
tableaux, J. of Automated Reasoning 3(3):225246, September 1987.
*[Reif 1992] W. Reif, The KIV system: systematic construction of
verified software, 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, 753757.
[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. 180183.
[Reiter 1971] R. Reiter, Two results on ordering for resolution
with merging and linear format, JACM 18(October 1971):630646.
[Reiter 1972] R. Reiter, The use of models in automatic theorem
proving, Tech. Report 7209, 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. 4146; also IEEE Trans. on Computers C25(4):328334,
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
C25(4):328334, April 1976.
[Reiter 1980] R. Reiter, A logic for default reasoning,
Artificial Intelligence 13(1):81132, April 1980.
[Remy 1981] J.L. Remy, P.A.S. Veloso, An economical method for
comparing data type specifications, ACM SIGPLAN 16(5):3942, May
1981.
[Remy 1982] J.L. Remy, Proving conditional identities by
equational case reasoning, rewriting and normalization, Report
82R085, CRIN, Nancy, 1982; also Proc. of 198283 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, ECAI84 (Pisa, Italy, 57
September 1984), ed. T. O'Shea, NorthHolland, Amsterdam, 1985,
pp. 373382.
[Remy 1985b] J.L. Remy, H. Zhang, Contextual Rewriting, Proc.
1st Conf. Rewriting Techniques and Applications (Dijon, France,
2022 May 1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag,
Berlin, 1985, pp. 4662.
[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. 3645.
[Rety 1985b] T.W. Reps, T. Teitelbaum, The synthesizer generator
reference manual, Tech. Report TR 84619, 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, 2022 May 1985), ed. J.P. Jouannaud,
LNCS 202, SpringerVerlag, Berlin, 1985, pp. 141157; also CRIN
report 86R131, 1986.
[Rety 1987] P. Rety, Improving basic narrowing techniques, Proc.
2nd Intl. Conf. on Rewriting Techniques and Applications
(Bordeaux, France, 2527 May 1987), ed. P. Lescanne, LNCS 256,
SpringerVerlag, Berlin, 1987, pp. 228241.
[Reynolds 1968] J.C. Reynolds, A generalized resolution
principal based upon contextfree grammers, Proc. IFIP Congr.
1968, pp. 14051411.
[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.
135151.
[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, SpringerVerlag, Berlin, 1983, pp. 255266.
[Rich 1980] R.P. Rich, Mechanical proof testing, Computer
Languages 5(1), 1980, pp. 128.
[Rich 1983] E. Rich, Artificial Intelligence, McGrawHill, 1983.
[Richards 1989] T. Richards, Clausal form logic: An introduction
to the logic of computer reasoning, AddisonWesley 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,
SpringerVerlag, 1982.
[Rissland 1980] E. Rissland, E. Soloway, Generating examples in
LIPS: Data and programs, COINS Tech Report 8007, 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, ECSLFCS8861, 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, SpringerVerlag, NY, 1989, pp. 303322.
*[Rittri 1990] M. Rittri, Retrieving library identifiers via
equational matching of types, 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. 603617.
*[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):5175,
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,
19571966, ed. J. Siekmann and G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 7476.
[Robinson 1960] A. Robinson, On the mechanization of the theory
of equations, Bull. Res. Council Israel, 9F, 1960, pp. 4770.
[Robinson 1961] J.A. Robinson, A General TheoremProving Program
for the IBM 704, Argonne National Lab., Memo No. 6447, November
1961.
[Robinson 1963a] J.A. Robinson, A machineoriented firstorder
logic (abstract), J. Symb. Logic 28(1963):302.
[Robinson 1963b] J.A. Robinson, Theorem proving on the computer,
JACM 10(2):163174, April 1963; also Automation of Reasoning 
Classical Papers on Computational Logic, Vol. I, 19571966, ed. J.
Siekmann and G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
372383.
[Robinson 1963c] A. Robinson, A basis for the mechanization of
the theory of equations, Computer Programming and Formal Systems,
ed. Braffort and Hirschberg, NorthHolland, Amsterdam, 1963, pp.
9599.
[Robinson 1964] J.A. Robinson, On Automatic Deduction, Rice
Univ., Studies 50, pp. 6989, 1964.
[Robinson 1965a] J.A. Robinson, Automatic deduction with
hyperresolution, Intl. J. of Computer Mathematics
1(1965):227234; also Automation of Reasoning  Classical Papers
on Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 416423.
[Robinson 1965b] J.A. Robinson, A machineoriented logic based
on the resolution principal, JACM 12(1):2341, 1965; also
Automation of Reasoning  Classical Papers on Computational Logic,
Vol. I, 19571966, ed. J. Siekmann and G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 397415.
[Robinson 1967a] J.A. Robinson, A review of automatic theorem
proving, Proc. Annual Symposia in Applied Math. XIX, Amer. Math.
Soc., Providence, 1967, pp. 118.
[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. 116124.
[Robinson 1968a] J.A. Robinson, New directions in Mechanical
theorem proving, Proc. IFIP Congr. 1968 1, pp. 6368; also
Automation Of Reasoning  Classical Papers On Computational Logic,
Vol. II, 19671970, ed. J. Siekmann And G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 152158.
[Robinson 1968b] J.A. Robinson, The generalized resolution
principal, Machine Intelligence 3, ed. Dale and Michie, Oliver and
Boyd, Edinburgh, 1968, pp. 7793; also Automation Of Reasoning 
Classical Papers On Computational Logic, Vol. II, 19671970, ed.
J. Siekmann And G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
135151.
[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
theoremproving in firstorder theories with equality, Machine
Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ.
Press, Edinburgh, 1969, pp. 135150; also Automation Of Reasoning
 Classical Papers On Computational Logic, Vol. II, 19671970, ed.
J. Siekmann And G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
298313.
[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. 123133.
[Robinson 1970b] G. Robinson, L. Wos, Axiom systems in automatic
theorem proving, Symp. on Automatic Demonstration, Lecture Notes
in Math. 125, SpringerVerlag, Berlin, 1970, pp. 215236.
[Robinson 1970c] J.A. Robinson, An overview of mechanical
theorem proving, in Theoretical Approaches to NonNumerical
Problem Solving, ed. Banerji and Mesarovic, NY, SpringerVerlag,
1970, pp. 220.
*[Robinson 1971a] J.A. Robinson, Building deduction machines,
Artificial Intelligence and Heuristic Programming, ed. Findler and
Meltzer, American Elsevier, NY, 1971, pp. 313.
*[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. 6372.
[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):5169.
[Rosen 1973] B.K. Rosen, Treemanipulating systems and
ChurchRosser theorems, JACM 20, 1973.
*[Ross 1988] K.S. Ross, R.W. Topor, Inferring negative
information from disjunctive databases, J. Automated Reasoning
4(4):397424, 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. 11481164.
[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):383393, December 1987.
[Rush 1986] T. Rush, D. Coleman, Combining patternmatching
algorithms, Tech. Report HPLBRCTR86036, HewlettPackard
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, 810 July 1987), ed. S. Kaplan
and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin, 1988, pp.
266278.
[Rusinowitch 1985] M. Rusinowitch, Path of subterms and
recursive decomposition ordering revisited, Proc. 1st Conf.
Rewriting Techniques and Applications (Dijon, France, 2022 May
1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin,
1985. pp. 225240; also J. of Symbolic Computation 3(1 and
2):117117, 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
87R128, CRIN, Nancy, France, 1987.
[Rusinowitch 1987] M. Rusinowitch, On termination of the direct
sum of term rewriting systems, Information Processing Letters
26(1987):6570.
*[Russell 1992] S. Russell, Efficient memorybounded search
methods, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 37 August
1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992,
pp. 15.
[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
BoyerMoore theorem prover: A proof of Wilson's theorem, J. of
Automated Reasoning 1(2):121139, 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
ACTST29289, 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):6171.
