ORA Canada Bibliography of Automated Deduction: Authors U to Z

[Ullman 1975] S. Ullman, Model-driven geometry theorem prover, MIT-AI Lab. Memo 321, May 1975.

[Ullman 1976] J.R. Ullman, An algorithm for subgraph isomorphism, JACM 23(1), 1976.

*[Umrigar 1990] Z.D. Umrigar, Finding advantageous orders for argument unification for the Prolog WAM, Logic Programming: Proc. of the 1990 North American Conf., ed. S. Debray and M. Hermenegildo, MIT Press, 1990, pp. 80-96.

*[Uribe 1992a] T.E. Uribe, Sorted unification using set constraints, 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. 163-177.

*[Uribe 1992b] T.E. Uribe, A. M. Frisch, M.K. Mitchell, An overview of FRAPPS 2.0: A framework for resolution-based automated proof procedure 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. 721-725.

[Urquhart 1987] A. Urquhart, Hard examples for resolution, JACM 34(1):209-219, January 1987.

[Ursic 1984] S. Ursic, A linear characterization of NP-clausal propositional calculus, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 80-100.

[Vaalen 1975] J. van Vaalen, An extension of unification to substitution with an application to automatic theorem proving, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975, pp. 77-82.

[VanderBrug 1971] G.J. VanderBrug, D.H. Fishman, J. Minder, Outline, bibliography and KWIC index on mechanical theorem proving and its applications, Tech. Report TR-159, Computer Science Center, Univ. of Maryland (June 1971), 51pp.

[Vanderbrug 1975] G.J. Vanderbrug, J. Minker, State-space, problem-reduction, and theorem proving - some relationships, CACM 18(2):107-115, February 1975.

[Veenker 1970] G. Veenker, A proof procedure with spec. reliance on the equality relation, Proc. Intl. Symp., Bonn, 1970.

[Veenker 1971] G. Veenker, Theorem proving by computer, Angew. Inf. 6(1971):276-282.

[Venkatesh 1986] G. Venkatesh, A decision method for temporal logic based on resolution, Proc. 5th Conf. Foundations of Software Technology and Theoretical Computer Science (New Delhi, India, December 1985), ed. S.N. Maheshwari, LNCS 206, Springer-Verlag, Berlin, 1985, pp. 272-289.

[Venturini 1975] M. Venturini-Zilli, Complexity of the unification algorithm for first-order expressions, Calcolo XII, Fasc. IV, October-December 1975, pp. 361-372.

[Verma 1986] R.M. Verma, T. Krishnaprasad, I.V. Ramakrishnan, An efficient parallel algorithm for term matching, Proc. 6th Intl. Conf. on Foundations of Software Technology and Theoretical Computer Science, LNCS 241, Springer-Verlag, December 1986, pp. 504-518.

*[Verma 1988] R.M. Verma, I.V. Ramakrishnan, Optimal time bounds for parallel term matching, 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. 694-703.

[Veroff 1981] R. Veroff, Canonicalization and demodulation in theorem proving, Tech. Rep. ANL-81-6, Argonne National Laboratory, Argonne, Illinois, February 1981.

[Veroff 1990] R. Veroff, L. Wos, The linked inference principle, I: The formal treatment, Preprint MCS-P160-0690, Mathematics and Computer Science Division, Argonne National Laboratory, 1990.

*[Vershinin 1992] K. Vershinin, I. Romanenko, One more logic with uncertainty and resolution principle for it, 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. 663-667.

[Vorob'ev 1958] N.N. Vorob'ev, A new decision algorithm in the constructive propositional calculus, Trydy Matem. Inst. Steklov; Transl.: Proc. Steklov Inst. Math. 2(52):193-225, 1958.

*[Vorobyov 1988] S.G. Vorobyov, On the arithmetic inexpressiveness of term rewriting systems, Proc. 3rd Annual Symp. on Logic in Computer Science (Edinburgh, Scotland, 5-8 July 1988), IEEE, 1988, pp. 212-217.

*[Vorobyov 1989] S.G. Vorobyov, Conditional rewrite rule systems with built-in arithmetic and induction, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 492-512.

[Voronkov 1986] A.A. Voronkov, A.I. Degtyarev, Automatic theorem proving, Cybernetics 3(22):290-297, May-June 1986.

[Voronkov 1988] A.A. Voronkov, A proof-search method for first-order logic. In COLOG-88 (papers presented at the Intl. Conf. on Computer Logic), Part 2, Tallinn, 1988, pp. 104-118; also in Proc. COLOG-88: Intl. Conf. on Computer Logic, LNCS 417, Springer-Verlag, 1990, pp. 300-312. *[Voronkov 1990] A.A. Voronkov, LISS - The Logic Inference Search System (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 677-678.

*[Voronkov 1992] A. Voronkov, Theorem proving in non-standard logics based on the inverse method, 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. 648-662.

*[Wakayama 1988] T. Wakayama, T.H. Payne, Case inference in resolution-based languages, 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. 313-322.

*[Wakayama 1990] T. Wakayama, T.H. Payne, Case-free programs: An abstraction of definite Horm programs, 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. 87-101.

[Waldinger 1969] R. Waldinger, Constructing programs automatically using theorem proving, PhD thesis, Carnegie-Mellon Univ., Pittsburgh, Penn., 1969.

*[Waldinger 1990] R. Waldinger, Program-synthetic deduction (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. 684.

[Wallen 1983a] L. Wallen, Using proof plans to control deduction, DAI Research Paper 185, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1983.

[Wallen 1983b] L.A. Wallen, Towards the provision of a natural mechanism for expressing domain-specific global strategies in general purpose theorem-provers, Research Paper 202, Dept. of Artificial Intelligence, Edinburgh, September 1983.

*[Wallen 1985] L.A. Wallen, Generating connection calculi from tableaux and sequent based proof systems, DAI Research Paper 258, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1985; also Proc. AISB-85, Warwick, England, April 1985, pp. 66-77; also Artificial Intelligence and Its Applications, ed. A.G. Cohn and J.R. Thomas, John Wiley & Sons Ltd., 1986, pp. 35-50.

*[Wallen 1987a] L.A. Wallen, G.V. Wilson, A computationally efficient proof system for S5 modal logic, Proc. 1987 AISB Conf., Advances in Artificial Intelligence (Univ. of Edinburgh, Scotland, 6-10 April 1987), ed. J. Hallam and C. Mellish, John Wiley & Sons, 1987, pp. 141-153.

[Wallen 1987b] L.A. Wallen, Matrix proof methods for modal logics, Proc. 10th IJCAI (Los Altos, CA), ed. J. McDermott, Morgan Kaufmann Inc., 1987, pp. 917-923.

[Wallen 1987c] L.A. Wallen, G.V. Wilson, Automated deduction in S5 modal logic: Theory and implementation, Research Paper 315, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1987.

[Wallen 1987d] L. Wallen, Automated deduction in modal logics, PhD thesis, Univ. of Edinburgh, 1987.

*[Wallen 1990] L.A. Wallen, Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics, The MIT Press, Cambridge, Massachusetts, 1990.

*[Walsh 1992]] T. Walsh, A. Nunes, A. Bundy, The use of proof plans to sum series, 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. 325-339.

[Walther 1981] C. Walther, Elimination of redundant links in extended connection graphs, Interner Bericht 10/81, Univ. of Karlsruhe; also Proc. GWAI-81, Informatik-Fachberichte 47, ed. J.H. Siekmann, Springer-Verlag, Berlin, 1981, pp. 201-213.

[Walther 1982a] C. Walther, A many-sorted calculus based on resolution and paramodulation, Interner Bericht 34/82, Institut fur Informatik I, Universitat Karlsruhe, 1982; also Proc. 8th IJCAI, ed. M. Kaufmann, Karlsruhe, W. Germany, August 1983, pp. 882-891; also in Research Notes in Artificial Intelligence, Pitman and Morgan Kaufmann Publishers, London, England, and Los Altos, CA, 1987.

[Walther 1982b] C. Walther, The Markgraf Karl refutation procedure: PLL - a first order language for an automated theorem prover, Interner Bericht 35/82, Institut fur Informatik I, Universitat Karlsruhe, 1982.

*[Walther 1984a] C. Walther, Unification in many-sorted theories, Interner Bericht 9/84, Institut fur Informatik I., Univ. Karlsruhe, 1984; also Proc. 6th European Conf. on Artificial Intelligence: Advances in Artificial Intelligence, ECAI-84 (Pisa, Italy, 5-7 September), ed. T. O'Shea, North-Holland, Amsterdam, 1985, pp. 383-392.

[Walther 1984b] C. Walther, A mechanical solution of Schubert's steamroller by many-sorted resolution, Proc. AAAI-84, Natl Conf. on Artificial Intelligence, Univ. of Texas at Austin, 6-10 August 1984, pp. 330-334; also (revised version) J. of Artificial Intelligence 26(2):217-224, May 1985.

[Walther 1984c] C. Walther, Schubert's steamroller - a case study in many-sorted resolution, Interner Bericht 5/84, Institut fur Informatik I, Universitat Karlsruhe, May 1984.

[Walther 1985] C. Walther, A classification of unification problems in many-sorted theories, Interner Bericht 10/85, Universitat Karlsruhe, Institut fur Informatik I, 1985, pp. 1-43; also Proc. 8th Intl. CADE (Oxford), Springer, LNCS 230, 1986, pp. 525-537.

[Walther 1986] C. Walther, A classification of many-sorted unification problems, 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. 525-537.

[Walther 1987a] C. Walther, Argument-bounded algorithms as a basis for automated termination proofs, Interner Bericht 17/87, Fakultat fur Informatik, Universitat Karlsruhe, 1987; 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. 602-621. [Walther 1987b] C. Walther, Mechanization of termination proofs, Internal report, Universitat Karlsruhe, 1987.

*[Walther 1988] C. Walther, Many-sorted unification, JACM 35(1):1-17, January 1988.

*[Walther 1993] C. Walther, Combining induction axioms by machine, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 95-101.

[Wan 1987] H. Wan, On proving geometry theorems via characteristic set computatation, MS project report, Dept. of Computer Science, RPI, Troy, December 1987. [Wang 1952] H. Wang, Logic of many-sorted theories, J. of Symbolic Logic 17, 1952.

[Wang 1960a] H. Wang, Proving theorems by pattern recognition I, CACM 3(April 1960):220-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. 229-243.

[Wang 1960b] H. Wang, Towards mechanical mathematics, IBM J. of Research and Development 4(January 1960):2-22; also The Modeling of Mind, ed. Sayre and Crosson, A Clarion Book, Simon and Schuster, NY, 1963, pp. 91-120; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 244-264.

[Wang 1961] H. Wang, Proving theorems by pattern recognition II, Bell System Tech. J. 40(January 1961):1-41.

[Wang 1963a] H. Wang, The mechanization of mathematical arguments, Proc. Symp. Appl. Math. 15(1963):31-40.

[Wang 1963b] H. Wang, Mechanical mathematics and inferential analysis, In Computer Programming and Formal Systems, ed. Braffort and Hirschberg, North-Holland, Amsterdam, 1963, pp. 1-20.

[Wang 1965a] H. Wang, Games, logic and computers, Scientific American, pp. 98-107, 1965.

[Wang 1965b] H. Wang, Formalization and automatic theorem proving, Proc. IFIP Congr. 1965, pp. 51-58.

[Wang 1967] H. Wang, Remarks on machine, sets, and the decision problem, In Formal Systems and Recursive Functions, ed. Crossley and Dummett, North-Holland, Amsterdam, 1967, pp. 304-320.

[Wang 1970] H. Wang, On the long-range prospects of automatic theorem proving, Symp. on Automatic Demonstration (Versailles, France, 1968), ed. M. Laudet, D. Lacombe, L. Nolin, and M. Schutzenberger, Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 101-111.

[Wang 1984] T.-C. Wang, W.W. Bledsoe, Hierarchical deduction, Tech. Report ATP-78A, Univ. of Texas at Austin, March 1984.

[Wang 1985] T.-C. Wang, Designing examples for semantically guided hierarchical deduction, Proc. 9th IJCAI, Los Angeles, CA, August 1985, pp. 1201-1207.

[Wang 1986a] T.-C. Wang, ECR: An equality conditional resolution proof procedure, 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. 254-271.

[Wang 1986b] T.-C. Wang, SHD-Prover at University of Texas at Austin, 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. 707-708.

[Wang 1987] T.-C. Wang, W.W. Bledsoe, Hierarchical Deduction, J. of Automated Reasoning 3(1):35-77, March 1987.

[Wang 1987a] T.-C Wang, Case studies of Z-module reasoning: Proving benchmark theorems for ring theory, J. of Automated Reasoning 3(4):437-451, December 1987.

[Wang 1987b] D. Wang, X. Gao, Geometry theorems proved mechanically using Wu's method - Part on Euclidean geometry, MM Research preprints, No. 2, pp. 75-106, 1987.

*[Wang 1988] T. C. Wang, Elements of Z-module reasoning, 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. 21-40.

*[Wang 1989a] D. Wang, On Wu's method for proving constructive geometric theorems, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 419-424.

*[Wang 1989b] T.-C. Wang, Solving open problems in right alternative rings with Z-module reasoning, J. of Automated Reasoning 5(2):141-165, June 1989.

*[Wang 1992] T.C. Wang, A.Goldberg, RVF: an automated formal 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. 735-739.

[Warren 1974] D.H.D. Warren, WARPLAN: A system for generating plans, Tech. report 76, Univ. of Edinburgh, Edinburgh, Scotland, 1974.

[Warren 1977a] D.H.D. Warren, Implementing Prolog - compiling predicate logic programs, DAI Research Reports 39 and 40, Dept. of Artificial Intelligence, DAI Research Report No. 39, Edinburgh Univ., May 1977.

[Warren 1977b] D.H.D. Warren, Applied logic - Its use and implementation as a programming tool, PhD thesis, Univ. of Edinburgh, Scotland, 1977; also Tech. Note 290, SRI International, 1983.

[Warren 1977c] D.H.D. Warren, L.M. Pereira, F. Pereira, Prolog - the language and its implementation compared with LISP, Proc. ACM Symp. on Artificial Intelligence and Programming Languages, issued as SIGPLAN Notices 12:8, and SIGART Newsletter, No. 64, August 1977, pp. 109-115.

[Warren 1980] D.H.D. Warren, Logic programming and compiler writing, Software -- Practice and Experience 10:107-125, 1980.

[Warren 1983] D.H.D. Warren, An abstract Prolog instruction set, Tech. Report 309, Artificial Intelligence Center, SRI International, Menlo Park, CA, October 1983.

[Warren 1988] D.H.D. Warren, Implementation of Prolog, Lecture Notes, Tutorial No. 3, 5th Intl. Conf. and Symp. on Logic Programming, Seattle, WA, August 1988.

*[Watts 1980] D.E. Watts, J.K. Cohen, Computer-implemented set theory, The American Mathematical Monthly 87(7):557-560, 1980.

*[Weidenbach 1990] C. Weidenbach, H.J. Ohlbach, A resolution calculus with dynamic sort structures and partial functions, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 688-693.

*[Weidenbach 1993] C. Weidenbach, Extending the resolution method with sorts, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 60-65.

[Weispfenning 1986] V. Weispfenning, Diamond formulas in the dynamic logic of recursively enumerable programs, 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. 564-571.

*[Weispfenning 1987] V. Weispfenning, Grobner bases for polynomial ideals over commutative regular rings, Proc. European Conf. on Computer Algebra (EUROCAL '87,Leipzig, GDR, 2-5 June 1987), ed. J.H. Davenport, LNCS 378, Springer-Verlag, Berlin, 1989, pp. 336-347; also Report MIP-8822, Fakultat fur Mathematik und Informatik, Universitat Passau, 1988.

*[Weispfenning 1988] V. Weispfenning, Efficient decision procedures for locally finite theories II, Report MIP-8808, Fakultat fur Mathematik und Informatik, Universitat Passau, 1988; also Proc. Intl. Symp. Symbolic and Algebraic Computation (ISSAC '88, Rome, Italy, 4-8 July 1988), ed. P. Gianni, LNCS 358, Springer-Verlag, Berlin, 1989, pp. 390-401.

*[Weispfenning 1989] V. Weispfenning, Constructing universal Grobner bases, Report MIP-8901, Fakultat fur Mathematik und Informatik, Universitat Passau, January 1989.

[Weispfenning 1990] V. Weispfenning, Comprehensive Grobner bases, Report MIP-9003, Fakultat fur Mathematik und Informatik, Universitat Passau, 1990.

[Welham 1976] R. Welham, Geometry problem solving, DAI Research Report 14, Edinburgh, January 1976.

[Weyhrauch 1974] R. Weyhrauch, FOL: A proof checker for first-order logic, Stanford AI Lab. Memo AIM-235, Stanford Univ., September 1974; revised Stanford AI Lab. Memo AIM-235.1, Stanford Univ., 1977.

[Weyhrauch 1980] R.W. Weyhrauch, Prolegomena to a theory of mechanized formal reasoning, Stanford AI Memo AIM-315, 1978; also Artificial Intelligence 13(1980):133-170; also in Readings in Artificial Intelligence, ed. B.L. Webber and N.J. Nilsson, Morgan Kaufmann Publishers, Los Altos, CA, 1981 also in Readings in Knowledge Representation, ed. R. Brachman and H. Levesque, Morgan Kaufmann Publishers, Los Altos, CA, 1985.

[Weyhrauch 1982] R. Weyhrauch, An example of FOL using metatheory: Formalizing reasoning systems and introducing derived inference rules, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 151-158.

[Whitehead 1925] A.N. Whitehead, B. Russell, Principia Mathematica I, Cambridge Univ. Press, Cambridge, MA, 1925.

[Wilding 1990] M. Wilding, A mechanically-checked correctness proof of a floating-point search program, Technical Report 56, Computational Logic, Inc., May 1990.

*[Wilding 1991] M. Wilding, Proving Matijasevich's lemma with a default arithmetic strategy, J. Automated Reasoning 7(3):439-446, September 1991.

[Wilkins 1973] D.E. Wilkins, Quest: A non-clausal theorem-proving system, M.Sc. thesis, Computer Science Memo-2, Univ. of Essex, Essex, England, 1973.

[Wilkins 1974] D. Wilkins, A non-clausal theorem-proving system, Proc. AISB Summer Conf., British Computer Society, London, 1974, pp. 257-267.

[Wilson 1976] G.A. Wilson, J. Minker, Resolution, refinements and search strategies - a comparative study, IEEE Trans. on Computers C-25(8):795-801, 1976.

[Wilson 1986] G.B. Wilson, Implementation of a connection method theorem-prover for S5 modal logic, Master's thesis, Department of Artificial Intelligence, Univ. of Edinburgh, 1986.

[Winker 1975a] S. Winker, Dynamic demodulation, Internal Memo, Dept. of Computer Sci., Northern Illinois Univ., 1975.

[Winker 1975b] S.K. Winker, Complete demodulations in automatic theorem proving, Univ. of Northern Illinois, Comput. Sci. Dept., July 1975.

[Winker 1976] S. Winker, An evaluation of an implementation of qualified hyperresolution, IEEE Trans. on Computers C-25(8):835-843, 1976.

[Winker 1978] S. Winker, L. Wos, Automated generation of models and counterexamples and its application to open questions in ternary Boolean algebra, Proc. 8th Intl. Symp. on Multiple-Valued Logic, Rosemount, Illinois, IEEE, 1978, pp. 251-256.

[Winker 1979] S. Winker, Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979; also JACM 29(2):273-284, 1982.

[Winker 1981] S. Winker, L. Wos, E. Lusk, Semi-groups, antiautomorphisms and involutions: A computer solution to an open problem I, Mathematics of Computation 37(156):533-545, October 1981.

[Winker 1982] S. Winker, L. Wos, Procedure implementation through demodulation and related tricks, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 109-131.

*[Winker 1990a] S. Winker, Robbins algebra: conditions that make a near-boolean algebra boolean, J. Automated Reasoning 6(4):465-489, December 1990.

[Winker 1990b] S. Winker, Absorption and idempotency criteria for a problem in near-boolean algebras, Preprint MCS-P177-0990, Mathematics and Computer Science Division, Argonne National Laboratory, 1990.

[Winkler 1983] F. Winkler, B. Buchberger, A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm, Proc. Colloquium on Algebra, Combinatorics, and Logic in Computer Science, Gyor, Hungary, 12-16 September 1983; also abstract in ACM SIGSAM Bulletin 17(3&4), issue no. 67 & 68, August and November 1983, p. 20; also Coll. Math. Soc. J. Bolyai 42(1983):849-869.

[Winkler 1984] F. Winkler, The Church-Rosser property in computer algebra and special theorem proving: An investigation of critical-pair/completion algorithms, Doctoral dissertation, Inst. f. Math., Johannes Kepler Universitat, Linz (VWGO), Austria, 1984.

[Winkler 1985a] F. Winkler, A note on improving the complexity of the Knuth-Bendix completion algorithm, Tech. Rep. 85-04, Dept. of Comp. and Inf. Sci., Univ. of Delaware, 1985.

*[Winkler 1985b] F. Winkler, Reducing the complexity of the Knuth-Bendix completion algorithm: a `unification' of different approaches, 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. 378-389.

[Winkler 1986a] F. Winkler, B Buchberger, A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm, Proc. Algebra, Combinatorics and Logic in Computer Science (Gyor, Hungary, 1983), Colloq. Math. Soc., Vol. 42., North-Holland, Amsterdam-New York, 1986, pp. 849-869.

[Winkler 1986b] F. Winkler, Solution of equations I: Polynomial idealsss and Grobner bases, Proc. Conf. on Computers and Mathematics, Stanford Univ., 30 July - 1 August 1986, to appear.

[Winkler 1989] F. Winkler, Knuth-Bendix procedure and Buchberger algorithm: a synthesis, In Symbolic and Algebraic Computation: Proc. of the ACM-SIGSAM 1989 Internat. Symp. (Portland, OR, 17-19 July 1989), ed. G. Gonnet, ACM Press, NY, NY, 1989, pp. 55-67.

[Winston 1980] P.H. Winston, Learning and reasoning by analogy, CACM 23(12):689-703, 1980.

[Winston 1981] P.H. Winston, B.K.P. Horn, LISP, Addison-Wesley Co., 1981.

[Winterstein 1976] G. Winterstein, Unification in second order logic, Bericht 3, Universitat Kaiserslautern, 1976.

[Wiring 1990] M. Wirsing, Proofs in structured specifications, Report MIP-9008, Fakultat fur Mathematik und Informatik, Universitat Passau, 1990.

*[Wissmann 1988] D. Wissmann, Applying rewriting techniques to groups with power-commutation-presentations, Proc. Intl. Symp. Symbolic and Algebraic Computation (ISSAC '88, Rome, Italy, 4-8 July 1988), ed. P. Gianni, LNCS 358, Springer-Verlag, Berlin, 1989, pp. 378-389.

[Witlink 1987] J.G. Witlink, A deficiency of natural deduction, Information Processing Letters 25(4):233-234, 17 June 1987.

[Wittgenstein 1963] L. Wittgenstein, Remarks on mechanical mathematics, in The Modeling of Mind, ed. Sayre and Crosson, A Clarion Book, Simon and Schuster, NY, 1963, pp. 121-140.

[Wolfram 1987] D.A. Wolfram, Reducing thrashing by adaptive backtracking, Tech. Report 112, Univ. of Cambridge Computer Laboratory, August 1987.

[Wolfram 1989a] D.A. Wolfram, Forward checking and intelligent backtracking, Information Processing Letters 32(1989):85-87.

*[Wolfram 1989b] D.A. Wolfram, Intractable unifiability problems and backtracking, J. Automated Reasoning 5(1):37-47, March 1989.

*[Wolfram 1990] D.A. Wolfram, ACE: The Abstract Clause Engine (abstract), Proc. 10th Intl. Conf. on Automated Deduction (CADE-10, Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel, Springer-Verlag, Berlin, 1990, pp. 679-680.

[Wolper 1985] P. Wolper, The tableau method for temporal logic: An overview, Logique et Analyse 110-111(June-Sept 1985):119-136.

[Wos 1964a] L.T. Wos, D.F. Carson, G.A. Robinson, Some theorem proving strategies and their implementation, AMD Tech. Memo 72, Argonne National Lab., 1964.

[Wos 1964b] L. Wos, D. Carson, G. Robinson, The unit preference strategy in theorem proving, In 1964 Fall Joint Comput. Conf.: AFIPS Conf. Proc. 26, Spartan Books, Washington D.C., 1964, pp. 615-621; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 387-393.

[Wos 1965a] L. Wos, G.A. Robinson, D.F. Carson, Automatic generation of proofs in the language of mathematics, Proc. IFIP Congr. 1965, Vol 2, Spartan Books, Washington, D.C., 1965, pp. 325-326.

[Wos 1965b] L. Wos, G. Robinson, D. Carson, Efficiency and completeness of the set of support strategy in theorem proving, JACM 12(October 1965):536-541; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 484-489.

[Wos 1967] L. Wos, G. Robinson, D. Carson, L. Shalla, The concept of demodulation in theorem proving, JACM 14(October 1967):698-709; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 66-81.

[Wos 1968] L.T. Wos, G.A. Robinson, The maximal model theorem, Abstract, Spring 1968 Meeting of Association for Symbolic Logic, J. of Symbolic Logic, 1968.

[Wos 1970] L. Wos, G. Robinson, Paramodulation and set of support, Proc. of the IRIA Symp. on Automatic Demonstration (Versailles, France), Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 276-310.

[Wos 1973] L. Wos, G. Robinson, Maximal models and refutation completeness: Semidecision procedures in automated theorem proving, in Word Problems: Decision Problems and the Burnside-Problem in Group Theory, ed. W. Boone, F. Cannonito and R. Lyndon, North-Holland, NY, 1973, pp. 609-639; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 578-608.

[Wos 1980] L. Wos, R. Overbeek, L. Henschen, Hyperparamodulation: A refinement of paramodulation, 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.

[Wos 1981a] L. Wos, Solving open questions with an automated theorem-proving program, Argonne National Lab., IL, 1981; also Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 1-31.

[Wos 1981b] L. Wos, S. Winker, E. Lusk, An automated reasoning system, Proc. AFIPS National Computer Conf., 1981, pp. 697-702.

[Wos 1983a] L. Wos, L. Henschen, Automated theorem proving 1965-1970, in Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 1-24.

[Wos 1983b] L. Wos, Automated reasoning: Real uses and potential uses, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 867-876.

[Wos 1983c] L. Wos, S. Winker, R. Veroff, B. Smith, L. Henschen, Questions concerning possible shortest single axioms in equivalential calculus: An application of automated theorem proving to infinite domains, Notre Dame J. of Formal Logic 24(2):205-223, April 1983.

[Wos 1984a] L. Wos, R. Veroff, B. Smith, and W. McCune, The linked inference principle II: The user's viewpoint, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 316-332.

[Wos 1984b] L. Wos, R. Overbeek, E. Lusk, J. Boyle, Automated Reasoning: Introduction and Applications, Prentice-Hall Inc., Englewood Cliffs, NJ, 1984.

[Wos 1984c] L. Wos, S. Winker, R. Veroff, B. Smith, and L. Henschen, A new use of an automated reasoning asistant: Open questions in equivalential calculus and the study of infinite domains, Artificial Intelligence 22(1984):303-356.

[Wos 1985] L. Wos, What is automated reasoning? J. of Automated Reasoning 1(1):5, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Wos 1986] L. Wos, W. McCune, Negative hyperparamodulation, 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. 229-239.

[Wos 1987a] L. Wos, Some obstacles to the automation of reasoning, and the problem of redundant information, J. of Automated Reasoning 3(1):81-90, March 1987.

[Wos 1987b] L. Wos, The problem of choosing the inference rule to employ, J. of Automated Reasoning 3(2):201-209, June 1987.

[Wos 1987c] L. Wos, The problem of extending the set of support strategy, J. of Automated Reasoning 3(3):319-328, September 1987.

[Wos 1987d] L. Wos, The problem of definition expansion and contraction, J. of Automated Reasoning 3(4):433-435, December 1987.

*[Wos 1988a] L. Wos, Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, NJ, 1988.

*[Wos 1988b] L. Wos, The problem of finding a strategy to control binary paramodulation, J. of Automated Reasoning 4(1):101-107, March 1988.

*[Wos 1988c] L. Wos, W. McCune, Challenge problems focusing on equality and combinatory logic: evaluating automated theorem-proving programs, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 714-729.

*[Wos 1988d] L. Wos, The problem of explaining the disparate performance of hyperresoluton and paramodulation, J. of Automated Reasoning 4(2):215-217, June 1988.

*[Wos 1988e] L. Wos, The problem of self-analytically choosing the set of support, J. of Automated Reasoning 4(3):327-329, September 1987.

*[Wos 1988f] L. Wos, The problems of self-analytically choosing the weights, J. Automated Reasoning 4(4):463-464, December 1988.

[Wos 1988] L. Wos and W. McCune, Searching for fixed point combinators by using automated theorem proving: a preliminary report, ANL-88-10, Argonne National Laboratory, 1988.

[Wos 1989a] L. Wos, R. Overbeek, E. Lusk, Subsumption, a sometimes undervalued procedure, Preprint MCS-P93-0789, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, July 1989; to appear in Festschrift for J.A. Robinson, ed. J.-L. Lassez.

*[Wos 1989b] L. Wos, The problem of finding an inference rule for set theory, J. Automated Reasoning 5(1):93-95, March 1989.

*[Wos 1989c] L. Wos, The problem of determining the size of a complete set of reductions, J. of Automated Reasoning 5(2):235-237, June 1989.

*[Wos 1989d] L. Wos, The problem of guaranteeing the existence of a complete set of reductions, J. of Automated Reasoning 5(3):399-401, September 1989.

*[Wos 1989d] L. Wos, The problem of guaranteeing the absence of a complete set of reductions, J. Automated Reasoning 5(4):531-532, December 1989.

[Wos 1989e] L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, R. Butler, OTTER experiments pertinent to CADE-10, Tech. Report ANL-89/39, Argonne National Laboratory, 1989.

*[Wos 1990a] L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, R. Butler, Automated reasoning contributes to mathematics and logic, 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. 485-499.

*[Wos 1990b] L. Wos, The problem of choosing between logic programming and general-purpose automated reasoning, J. of Automated Reasoning 6(1):77-78, March 1990.

*[Wos 1990c] L. Wos, The problem of finding a mapping between clause representation and natural-deduction representation, J. of Automated Reasoning 6(2):211-212, June 1990.

*[Wos 1990d] L. Wos, Meeting the challenge of fifty years of logic, J. of Automated Reasoning 6(2):213-232, June 1990.

*[Wos 1990e] L. Wos, The problem of finding a semantic strategy for focusing inference rules, J. of Automated Reasoning 6(3):337-339, September 1990.

*[Wos 1990f] L. Wos, The problem of choosing between predicate and function notation for problem representation, J. Automated Reasoning 6(4):463-464, December 1990.

*[Wos 1991a] L. Wos, The problem of finding a restriction strategy more effective than the set of support strategy, J. Automated Reasoning 7(1):105-107, March 1991.

*[Wos 1991b] L. Wos, A well-kept secret of history, J. Automated Reasoning 7(3):301-302, September 1991.

*[Wos 1991c] L. Wos, The problem of choosing the type of subsumption to use, J. Automated Reasoning 7(3):435-438, September 1991.

*[Wos 1991d] L. Wos, The problem of choosing the representation, inference rule, and strategy, J. Automated Reasoning 7(4):631-634, December 1991.

*[Wos 1992] L. Wos, The impossibility of the automation of logical reasoning (abstract), 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, p. 1-4.

[Wrightson 1979] G. Wrightson, A proof procedure for higher-order modal logic, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 148-154.

[Wrightson 1984a] G. Wrightson, Semantic tableaux, unification and links, Tech. Report CSD-ANZARP-84-001, Department of Computer Science, Univ. of Wellington, Victoria, New Zealand, 1984.

[Wrightson 1984b] G. Wrightson, Non-classical logic theorem proving using links and unification in semantic tableaux, TR CSD-ANZARP-84-003, Victoria Univ., Wellington, New Zealand, 1984.

[Wrightson 1985] G. Wrightson, Non-classical logic theorem proving, J. of Automated Reasoning 1(1):37-40, with references, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

*[Wrightson 1987] G. Wrightson, Semantic tableaux and links, Proc. Australian Joint Artificial Intelligence Conf. (AI'87) Syndney Masonic Centre, 2-4 November 1987, pp. 553-566.

*[Wroblewski 1987] D.A. Wroblewski, Nondestructive graph unification, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, pp. 582-587.

[Wu 1978] Wu Wen-tsun, On the decision problem and the mechanization of theorem proving in elementary geometry, Scientia Sinica 21(2):159-172, March-April 1978; also Contemp. Math. 29:213-234.

[Wu 1979] Wu Wen-tsun, Mechanical theorem proving in elementary differential geometry, Scientia Sinica, Mathematics Supplement I, 1979, pp. 94-102 (in Chinese); also Science Press, Proc. 1980 Beijing Symp. on Differential Geometry and Differential Equations 2(1982):125-138,1073-1092.

[Wu 1982] Wu W.-T., Toward mechanization of geometry -- Some comments on Hilbert's "Grundlagen der Geometrie", Acta Mathematica Scientia 2(2):125-138, 1982.

[Wu 1983] Wu W.-T., Some remarks on mechanical theorem proving in elementary geometry, Acta Mathematica Scientia 3(4):357-360, 1983.

[Wu 1984a] Wu W.-T., Some recent advances in mechanical theorem proving of geometries, In: Automated Theorem Proving: After 25 Years, ed. W.W. Bledsoe and D. Loveland, Contemporary Mathematics Series 19, American Math. Society, Providence, RI, 1984, pp. 89-118, pp. 235-242.

[Wu 1984b] Wu W.-T., Basic principles of mechanical theorem proving in elementary geometries, J. of System Sciences and Mathematical Sciences 4(3):207-235, July 1984; also republished in J. of Automated Reasoning 2(4):221-252, September 1986.

[Wu 1986a] Wu Wen-tsun, On zeros of algebraic equations - an application of Ritt's principle, Kexue Tongbao 31(1):1-5, 1986.

[Wu 1986b] Wu Wen-tsun, A mechanization method of geometry and its applications, I. Distances, areas and volumes, J. of Systems Sci. and Math. Sci 6(1986):204-216.

[Wu 1986c] Wu Wen-tsun, A mechanization method of geometry and its applications, I. Distances, areas and volumes in Euclidean and non-Euclidean geometries, Kexue Tongbao 32(1986): 436-440.

[Wu 1987a] Wu W.-t., On reducibility problem in mechanical theorem proving of elementary geometries, Chinese Quarterly J. of Math. 2(1):1-20, 1987.

[Wu 1987b] Wu Wen-tsun, A mechanization method of geometry and its applications, 2. Curve pairs of Bertrand type, Kexue Tongbao 32(1987): 585-588.

*[Wu 1991] Wu Wen-tsun, Mechanical theorem proving of differential geometries and some of its applications in mechanics, J. of Automated Reasoning 7(2):171-191, June 1991.

*[Wurtz 1992] J. Wurtz, Unifying cycles, Research report RR-92-22, Deutsches Forschungszentrum fur Kunstliche Intelligenz GmbH (DFKI) (German Research Center for Artificial Intelligence), Stuhlsatzenhausweg 3, 6600 Saarbrucken 11, 1992; also Proc. 10th ECAI (ECAI 92, Vienna, Austria, 3-7 August 1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992, pp. 60-64.

[Xiaorong 1989] Huang Xiaorong, A human oriented proof presentation model, SEKI Report SR-89-11, Universitat Kaiserslautern, 1989.

*[XuHua 1989] L. XuHua, Lock, linear lambda-paramodulation in operator fuzzy logic, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 435-440.

[Yamaguchi 1985] T. Yamaguchi, Y. Tezuka, O. Kakusho, Parallel Processing of Resolution, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985.

[Yamamoto 1987] A. Yamamoto, A theoretical combination of SLD-resolution and narrowing, Proc. ICLP'87, 1987, pp. 470-487.

[Yarmush 1976] D.L. Yarmush, The linear conjunct and other algorithms for mechanical theorem proving, IMM 412, Courant Inst. Of Math. Sci., NY, July 1976.

[Yasuura 1983] H. Yasuura, On the parallel computational complexity of unification, Yajima Lab. Research Report, ER 83-01, October 1983; also ICOT Technical Report TR-027, Kyoto Univ., October 1983.

[Yates 1970] R. Yates, B. Raphael, T. Hart, Resolution graphs, Artificial Intelligence 1(3-4):257-289, Winter 1970.

[Yelick 1985a] K. Yelick, Combining unification algorithms for confined regular equational theories, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 365-380.

[Yelick 1985b] K. Yelick, A generalized approach to equational unification, Internal Report MIT/LCS/TR-344, MIT, 1985.

[Yelick 1987] K.A. Yelick, Unification in combinations of collapse-free regular theories, J. of Symbolic Computation 3(1 and 2):153-181, February/April 1987.

*[Yelick 1992] K.A. Yelick, S.J. Garland, A parallel completion procedure for term rewriting 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. 109-123.

[Yelowitz 1976] L. Yelowitz, New results and techniques in resolution theory, IEEE Trans. on Computers C-25(7):673-677, July 1976.

[You 1986a] J. You, P.A. Subrahmanyam, E-unification algorithms for a class of confluent term rewriting systems, Proc. Intl. Colloquium on Automata, Languages and Programming (Rennes, France, July 1986), ed. L. Kott, LNCS 226, Springer-Verlag, Berlin, 1986, pp. 454-463.

[You 1986b] J.-H. You, P.A. Subrahmanyam, A class of confluent term rewriting systems and unification, J. of Automated Reasoning 2(4):391-418, December 1986.

[You 1988] J.-H. You, Outer narrowing for equational theories based on constructors, Proc. ICALP '88, LNCS 317, Springer-Verlag, pp. 727-741, 1988.

*[Young 1989] W.D. Young, A mechanically verified code generator, J. Automated Reasoning 5(4):493-518, December 1989.

*[Yu 1990] Y. Yu, Computer proofs in group theory, J. of Automated Reasoning 6(3):251-286, September 1990.

*[Yuhua 1993] Z. Yuhua, And/Or parallel execution of logic programs: exploiting dependent and-parallelism, ACM SIGPlan Notices 28(5):19-28, May 1993.

[Zadeh 1979] L.A. Zadeh, Approximate reasoning based on fuzzy logic, Proc. 6th IJCAI, Tokyo, August 1979, pp. 1004-1010.

[Zaionc 1985] M. Zaionc, The set of unifiers in typed 1-calculus as regular expressions, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 430-440.

*[Zaionc 1988] M. Zaionc, Mechanical procedure for proof construction via closed terms in typed lambda calculus, J. Automated Reasoning 4(2):173-190, June 1988.

[Zamov 1969] N.K. Zamov, V.I. Sharonov, On a class of strategies which can be used to establish decidability by the resolution principle, Issled po konstruktivnoye matematikye i matematicheskoie logikye III, Vol. 16(1969):54-64.

[Zamov 1971] N.K. Zamov, V.J. Sharonov, A class of strategies for the determination of provability by the resolution method, Seminars in Mathematics 16, V.A. Steklov Mathem. Institute, Leningrad, Consultants Bureau, NY-London, 1971, pp. 26-311.

[Zamov 1989] N.K. Zamov, Maslov's inverse method and decidable classes, Annals of Pure and Aplied Logic 42(1989):165-194.

[Zandleven 1974] I. Zandleven, A verifying program for AUTOMATH, Proc. Symp. on APL, ed. P. Braffort, Paris, 1974.

*[Zaniolo 1986] C. Zaniolo, D. Sacca, Rule rewriting methods for efficient implementations of Horn logic, 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. 114-139.

*[Zell 1989] A. Zell, T. Braunt, Iterative-deepening Prolog, 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. 919-929.

[Zhang 1987] H. Zhang, An efficient algorithm for simple diphonatine equations, Tech. Report 87-26, Dept of Computer Science, RPI, 1987.

*[Zhang 1988a] H. Zhang, D. Kapur, First-order theorem proving using conditional rewrite rules, 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. 1-20.

*[Zhang 1988b] H. Zhang, D. Kapur, M.S. Krishnamorrthy, A mechanizable induction principle for equational specifications, 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. 162-181.

[Zhang 1988c] H. Zhang, Reduction, superposition and induction: Automated reasoning in an equational logic, PhD diss., Rensselaer Polytechnic Institute, Dept. of Computer Science, Schenectady, NY, 1988.

*[Zhang 1989] H. Zhang, D. Kapur, Consider only general superpositions in completion procedures, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 513-527.

[Zhang 1990] H. Zhang, Automated proof of ring commutativity problems by algebraic methods, J. Symbolic Comput. 9(4):423-427, April 1990.

[Zhang 1991] H. Zhang, Cut elimination and automatic proof procedures, Theor. Comput. Sci 91(2):265-284, December 23, 1991.

*[Zhang 1992a] H. Zhang, X. Hua, Proving the Chinese remainder theorem by the cover set induction, 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. 431-445.

*[Zhang 1992b] H. Zhang, X. Hua, Herky: High performance rewriting in RRL, 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. 696-700.

[Zucker 1975] J. Zucker, Formalization of classical mathematics in AUTOMATH, In Colloques Internationaux du Centre Nationale de la Recherche Scientifique, No 249, 1975, pp. 136-145.