ORA Canada Bibliography of Automated Deduction: Authors U to Z
[Ullman 1975] S. Ullman, Modeldriven geometry theorem prover,
MITAI 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. 8096.
*[Uribe 1992a] T.E. Uribe, Sorted unification using set
constraints, 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. 163177.
*[Uribe 1992b] T.E. Uribe, A. M. Frisch, M.K. Mitchell, An
overview of FRAPPS 2.0: A framework for resolutionbased automated
proof procedure 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. 721725.
[Urquhart 1987] A. Urquhart, Hard examples for resolution, JACM
34(1):209219, January 1987.
[Ursic 1984] S. Ursic, A linear characterization of NPclausal
propositional calculus, Proc. 7th Intl. Conf. on Automated
Deduction (CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS
170, SpringerVerlag, NY, 1984, pp. 80100.
[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. 7782.
[VanderBrug 1971] G.J. VanderBrug, D.H. Fishman, J. Minder,
Outline, bibliography and KWIC index on mechanical theorem proving
and its applications, Tech. Report TR159, Computer Science
Center, Univ. of Maryland (June 1971), 51pp.
[Vanderbrug 1975] G.J. Vanderbrug, J. Minker, Statespace,
problemreduction, and theorem proving  some relationships, CACM
18(2):107115, 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):276282.
[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, SpringerVerlag,
Berlin, 1985, pp. 272289.
[Venturini 1975] M. VenturiniZilli, Complexity of the
unification algorithm for firstorder expressions, Calcolo XII,
Fasc. IV, OctoberDecember 1975, pp. 361372.
[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, SpringerVerlag, December 1986, pp.
504518.
*[Verma 1988] R.M. Verma, I.V. Ramakrishnan, Optimal time bounds
for parallel term matching, 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.
694703.
[Veroff 1981] R. Veroff, Canonicalization and demodulation in
theorem proving, Tech. Rep. ANL816, Argonne National Laboratory,
Argonne, Illinois, February 1981.
[Veroff 1990] R. Veroff, L. Wos, The linked inference principle,
I: The formal treatment, Preprint MCSP1600690, 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 (CADE11, Saratoga Springs, NY, USA,
June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence
607, SpringerVerlag, Berlin, 1992, pp. 663667.
[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):193225, 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, 58 July 1988),
IEEE, 1988, pp. 212217.
*[Vorobyov 1989] S.G. Vorobyov, Conditional rewrite rule systems
with builtin arithmetic and induction, Proc. 3rd Intl. Conf.
Rewriting Techniques and Applications (Chapel Hill, North
Carolina, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 492512.
[Voronkov 1986] A.A. Voronkov, A.I. Degtyarev, Automatic theorem
proving, Cybernetics 3(22):290297, MayJune 1986.
[Voronkov 1988] A.A. Voronkov, A proofsearch method for
firstorder logic. In COLOG88 (papers presented at the Intl.
Conf. on Computer Logic), Part 2, Tallinn, 1988, pp. 104118; also
in Proc. COLOG88: Intl. Conf. on Computer Logic, LNCS 417,
SpringerVerlag, 1990, pp. 300312. *[Voronkov 1990] A.A.
Voronkov, LISS  The Logic Inference Search System (abstract),
Proc. 10th Intl. Conf. on Automated Deduction (CADE10,
Kaiserslautern, FRG, July 1990), Lecture Notes in Artificial
Intelligence 449, ed. M.E. Stickel, SpringerVerlag, Berlin, 1990,
pp. 677678.
*[Voronkov 1992] A. Voronkov, Theorem proving in nonstandard
logics based on the inverse method, 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. 648662.
*[Wakayama 1988] T. Wakayama, T.H. Payne, Case inference in
resolutionbased languages, 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.
313322.
*[Wakayama 1990] T. Wakayama, T.H. Payne, Casefree programs: An
abstraction of definite Horm programs, 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. 87101.
[Waldinger 1969] R. Waldinger, Constructing programs
automatically using theorem proving, PhD thesis, CarnegieMellon
Univ., Pittsburgh, Penn., 1969.
*[Waldinger 1990] R. Waldinger, Programsynthetic deduction
(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. 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 domainspecific global strategies in
general purpose theoremprovers, 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. AISB85, Warwick, England, April 1985, pp. 6677; also
Artificial Intelligence and Its Applications, ed. A.G. Cohn and
J.R. Thomas, John Wiley & Sons Ltd., 1986, pp. 3550.
*[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,
610 April 1987), ed. J. Hallam and C. Mellish, John Wiley &
Sons, 1987, pp. 141153.
[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. 917923.
[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
nonclassical 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
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 325339.
[Walther 1981] C. Walther, Elimination of redundant links in
extended connection graphs, Interner Bericht 10/81, Univ. of
Karlsruhe; also Proc. GWAI81, InformatikFachberichte 47, ed.
J.H. Siekmann, SpringerVerlag, Berlin, 1981, pp. 201213.
[Walther 1982a] C. Walther, A manysorted 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.
882891; 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 manysorted
theories, Interner Bericht 9/84, Institut fur Informatik I., Univ.
Karlsruhe, 1984; also Proc. 6th European Conf. on Artificial
Intelligence: Advances in Artificial Intelligence, ECAI84 (Pisa,
Italy, 57 September), ed. T. O'Shea, NorthHolland, Amsterdam,
1985, pp. 383392.
[Walther 1984b] C. Walther, A mechanical solution of Schubert's
steamroller by manysorted resolution, Proc. AAAI84, Natl Conf.
on Artificial Intelligence, Univ. of Texas at Austin, 610 August
1984, pp. 330334; also (revised version) J. of Artificial
Intelligence 26(2):217224, May 1985.
[Walther 1984c] C. Walther, Schubert's steamroller  a case
study in manysorted resolution, Interner Bericht 5/84, Institut
fur Informatik I, Universitat Karlsruhe, May 1984.
[Walther 1985] C. Walther, A classification of unification
problems in manysorted theories, Interner Bericht 10/85,
Universitat Karlsruhe, Institut fur Informatik I, 1985, pp. 143;
also Proc. 8th Intl. CADE (Oxford), Springer, LNCS 230, 1986, pp.
525537.
[Walther 1986] C. Walther, A classification of manysorted
unification problems, Proc. 8th Intl. Conf. on Automated Deduction
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 525537.
[Walther 1987a] C. Walther, Argumentbounded 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 (CADE9, Argonne, Illinois,
2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 602621. [Walther 1987b] C.
Walther, Mechanization of termination proofs, Internal report,
Universitat Karlsruhe, 1987.
*[Walther 1988] C. Walther, Manysorted unification, JACM
35(1):117, January 1988.
*[Walther 1993] C. Walther, Combining induction axioms by
machine, Proc. 13th IJCAI (Chambery, France, 28 August3 September
1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 95101.
[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 manysorted theories, J. of Symbolic Logic 17, 1952.
[Wang 1960a] H. Wang, Proving theorems by pattern recognition I,
CACM 3(April 1960):220234; also Automation of Reasoning 
Classical Papers on Computational Logic, Vol. I, 19571966, ed. J.
Siekmann and G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
229243.
[Wang 1960b] H. Wang, Towards mechanical mathematics, IBM J. of
Research and Development 4(January 1960):222; also The Modeling
of Mind, ed. Sayre and Crosson, A Clarion Book, Simon and
Schuster, NY, 1963, pp. 91120; also Automation of Reasoning 
Classical Papers on Computational Logic, Vol. I, 19571966, ed. J.
Siekmann and G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
244264.
[Wang 1961] H. Wang, Proving theorems by pattern recognition II,
Bell System Tech. J. 40(January 1961):141.
[Wang 1963a] H. Wang, The mechanization of mathematical
arguments, Proc. Symp. Appl. Math. 15(1963):3140.
[Wang 1963b] H. Wang, Mechanical mathematics and inferential
analysis, In Computer Programming and Formal Systems, ed. Braffort
and Hirschberg, NorthHolland, Amsterdam, 1963, pp. 120.
[Wang 1965a] H. Wang, Games, logic and computers, Scientific
American, pp. 98107, 1965.
[Wang 1965b] H. Wang, Formalization and automatic theorem
proving, Proc. IFIP Congr. 1965, pp. 5158.
[Wang 1967] H. Wang, Remarks on machine, sets, and the decision
problem, In Formal Systems and Recursive Functions, ed. Crossley
and Dummett, NorthHolland, Amsterdam, 1967, pp. 304320.
[Wang 1970] H. Wang, On the longrange 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, SpringerVerlag,
Berlin, 1970, pp. 101111.
[Wang 1984] T.C. Wang, W.W. Bledsoe, Hierarchical deduction,
Tech. Report ATP78A, 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. 12011207.
[Wang 1986a] T.C. Wang, ECR: An equality conditional resolution
proof procedure, Proc. 8th Intl. Conf. on Automated Deduction
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 254271.
[Wang 1986b] T.C. Wang, SHDProver at University of Texas at
Austin, Proc. 8th Intl. Conf. on Automated Deduction (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 707708.
[Wang 1987] T.C. Wang, W.W. Bledsoe, Hierarchical Deduction, J.
of Automated Reasoning 3(1):3577, March 1987.
[Wang 1987a] T.C Wang, Case studies of Zmodule reasoning:
Proving benchmark theorems for ring theory, J. of Automated
Reasoning 3(4):437451, 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. 75106, 1987.
*[Wang 1988] T. C. Wang, Elements of Zmodule reasoning, 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. 2140.
*[Wang 1989a] D. Wang, On Wu's method for proving constructive
geometric theorems, Proc. 11th IJCAI (Detroit, Michigan, USA,
2025 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp.
419424.
*[Wang 1989b] T.C. Wang, Solving open problems in right
alternative rings with Zmodule reasoning, J. of Automated
Reasoning 5(2):141165, June 1989.
*[Wang 1992] T.C. Wang, A.Goldberg, RVF: an automated formal
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. 735739.
[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. 109115.
[Warren 1980] D.H.D. Warren, Logic programming and compiler
writing, Software  Practice and Experience 10:107125, 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, Computerimplemented set
theory, The American Mathematical Monthly 87(7):557560, 1980.
*[Weidenbach 1990] C. Weidenbach, H.J. Ohlbach, A resolution
calculus with dynamic sort structures and partial functions, Proc.
9th ECAI (Stockholm, Sweden, 610 August 1990), ed. L.C. Aiello,
Pitman Publishing, London, 1990, pp. 688693.
*[Weidenbach 1993] C. Weidenbach, Extending the resolution
method with sorts, Proc. 13th IJCAI (Chambery, France, 28 August3
September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp.
6065.
[Weispfenning 1986] V. Weispfenning, Diamond formulas in the
dynamic logic of recursively enumerable programs, Proc. 8th Intl.
Conf. on Automated Deduction (CADE8, Oxford, England, July
27August 1, 1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag,
Berlin, 1986, pp. 564571.
*[Weispfenning 1987] V. Weispfenning, Grobner bases for
polynomial ideals over commutative regular rings, Proc. European
Conf. on Computer Algebra (EUROCAL '87,Leipzig, GDR, 25 June
1987), ed. J.H. Davenport, LNCS 378, SpringerVerlag, Berlin,
1989, pp. 336347; also Report MIP8822, Fakultat fur Mathematik
und Informatik, Universitat Passau, 1988.
*[Weispfenning 1988] V. Weispfenning, Efficient decision
procedures for locally finite theories II, Report MIP8808,
Fakultat fur Mathematik und Informatik, Universitat Passau, 1988;
also Proc. Intl. Symp. Symbolic and Algebraic Computation (ISSAC
'88, Rome, Italy, 48 July 1988), ed. P. Gianni, LNCS 358,
SpringerVerlag, Berlin, 1989, pp. 390401.
*[Weispfenning 1989] V. Weispfenning, Constructing universal
Grobner bases, Report MIP8901, Fakultat fur Mathematik und
Informatik, Universitat Passau, January 1989.
[Weispfenning 1990] V. Weispfenning, Comprehensive Grobner
bases, Report MIP9003, 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
firstorder logic, Stanford AI Lab. Memo AIM235, Stanford Univ.,
September 1974; revised Stanford AI Lab. Memo AIM235.1, Stanford
Univ., 1977.
[Weyhrauch 1980] R.W. Weyhrauch, Prolegomena to a theory of
mechanized formal reasoning, Stanford AI Memo AIM315, 1978; also
Artificial Intelligence 13(1980):133170; 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, SpringerVerlag, Berlin, 1982, pp. 151158.
[Whitehead 1925] A.N. Whitehead, B. Russell, Principia
Mathematica I, Cambridge Univ. Press, Cambridge, MA, 1925.
[Wilding 1990] M. Wilding, A mechanicallychecked correctness
proof of a floatingpoint 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):439446,
September 1991.
[Wilkins 1973] D.E. Wilkins, Quest: A nonclausal
theoremproving system, M.Sc. thesis, Computer Science Memo2,
Univ. of Essex, Essex, England, 1973.
[Wilkins 1974] D. Wilkins, A nonclausal theoremproving system,
Proc. AISB Summer Conf., British Computer Society, London, 1974,
pp. 257267.
[Wilson 1976] G.A. Wilson, J. Minker, Resolution, refinements
and search strategies  a comparative study, IEEE Trans. on
Computers C25(8):795801, 1976.
[Wilson 1986] G.B. Wilson, Implementation of a connection method
theoremprover 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
C25(8):835843, 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 MultipleValued
Logic, Rosemount, Illinois, IEEE, 1978, pp. 251256.
[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 (CADE4, Austin, Texas, 13 February 1979), ed. W.H.
Joyner, 1979; also JACM 29(2):273284, 1982.
[Winker 1981] S. Winker, L. Wos, E. Lusk, Semigroups,
antiautomorphisms and involutions: A computer solution to an open
problem I, Mathematics of Computation 37(156):533545, 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, SpringerVerlag,
Berlin, 1982, pp. 109131.
*[Winker 1990a] S. Winker, Robbins algebra: conditions that make
a nearboolean algebra boolean, J. Automated Reasoning
6(4):465489, December 1990.
[Winker 1990b] S. Winker, Absorption and idempotency criteria
for a problem in nearboolean algebras, Preprint MCSP1770990,
Mathematics and Computer Science Division, Argonne National
Laboratory, 1990.
[Winkler 1983] F. Winkler, B. Buchberger, A criterion for
eliminating unnecessary reductions in the KnuthBendix algorithm,
Proc. Colloquium on Algebra, Combinatorics, and Logic in Computer
Science, Gyor, Hungary, 1216 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):849869.
[Winkler 1984] F. Winkler, The ChurchRosser property in
computer algebra and special theorem proving: An investigation of
criticalpair/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 KnuthBendix completion algorithm, Tech. Rep. 8504, Dept.
of Comp. and Inf. Sci., Univ. of Delaware, 1985.
*[Winkler 1985b] F. Winkler, Reducing the complexity of the
KnuthBendix completion algorithm: a `unification' of different
approaches, 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. 378389.
[Winkler 1986a] F. Winkler, B Buchberger, A criterion for
eliminating unnecessary reductions in the KnuthBendix algorithm,
Proc. Algebra, Combinatorics and Logic in Computer Science (Gyor,
Hungary, 1983), Colloq. Math. Soc., Vol. 42., NorthHolland,
AmsterdamNew York, 1986, pp. 849869.
[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, KnuthBendix procedure and Buchberger
algorithm: a synthesis, In Symbolic and Algebraic Computation:
Proc. of the ACMSIGSAM 1989 Internat. Symp. (Portland, OR, 1719
July 1989), ed. G. Gonnet, ACM Press, NY, NY, 1989, pp. 5567.
[Winston 1980] P.H. Winston, Learning and reasoning by analogy,
CACM 23(12):689703, 1980.
[Winston 1981] P.H. Winston, B.K.P. Horn, LISP, AddisonWesley
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 MIP9008, Fakultat fur Mathematik und Informatik,
Universitat Passau, 1990.
*[Wissmann 1988] D. Wissmann, Applying rewriting techniques to
groups with powercommutationpresentations, Proc. Intl. Symp.
Symbolic and Algebraic Computation (ISSAC '88, Rome, Italy, 48
July 1988), ed. P. Gianni, LNCS 358, SpringerVerlag, Berlin,
1989, pp. 378389.
[Witlink 1987] J.G. Witlink, A deficiency of natural deduction,
Information Processing Letters 25(4):233234, 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. 121140.
[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):8587.
*[Wolfram 1989b] D.A. Wolfram, Intractable unifiability problems
and backtracking, J. Automated Reasoning 5(1):3747, March 1989.
*[Wolfram 1990] D.A. Wolfram, ACE: The Abstract Clause Engine
(abstract), Proc. 10th Intl. Conf. on Automated Deduction
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 679680.
[Wolper 1985] P. Wolper, The tableau method for temporal logic:
An overview, Logique et Analyse 110111(JuneSept 1985):119136.
[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.
615621; also Automation of Reasoning  Classical Papers on
Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 387393.
[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.
325326.
[Wos 1965b] L. Wos, G. Robinson, D. Carson, Efficiency and
completeness of the set of support strategy in theorem proving,
JACM 12(October 1965):536541; also Automation of Reasoning 
Classical Papers on Computational Logic, Vol. I, 19571966, ed. J.
Siekmann and G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
484489.
[Wos 1967] L. Wos, G. Robinson, D. Carson, L. Shalla, The
concept of demodulation in theorem proving, JACM 14(October
1967):698709; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 6681.
[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, SpringerVerlag,
Berlin, 1970, pp. 276310.
[Wos 1973] L. Wos, G. Robinson, Maximal models and refutation
completeness: Semidecision procedures in automated theorem
proving, in Word Problems: Decision Problems and the
BurnsideProblem in Group Theory, ed. W. Boone, F. Cannonito and
R. Lyndon, NorthHolland, NY, 1973, pp. 609639; also Automation
Of Reasoning  Classical Papers On Computational Logic, Vol. II,
19671970, ed. J. Siekmann And G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 578608.
[Wos 1980] L. Wos, R. Overbeek, L. Henschen,
Hyperparamodulation: A refinement of paramodulation, Proc. 5th
Conf. on Automated Deduction (Les Arcs, France, 811 July 1980),
ed. W. Bibel and R. Kowalski, LNCS 87, SpringerVerlag, Berlin,
1980.
[Wos 1981a] L. Wos, Solving open questions with an automated
theoremproving program, Argonne National Lab., IL, 1981; also
Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138,
SpringerVerlag, Berlin, 1982, pp. 131.
[Wos 1981b] L. Wos, S. Winker, E. Lusk, An automated reasoning
system, Proc. AFIPS National Computer Conf., 1981, pp. 697702.
[Wos 1983a] L. Wos, L. Henschen, Automated theorem proving
19651970, in Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 124.
[Wos 1983b] L. Wos, Automated reasoning: Real uses and potential
uses, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp.
867876.
[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):205223, 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 (CADE7, Napa, CA, May 1984),
ed. R.E. Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp.
316332.
[Wos 1984b] L. Wos, R. Overbeek, E. Lusk, J. Boyle, Automated
Reasoning: Introduction and Applications, PrenticeHall 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):303356.
[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 (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 229239.
[Wos 1987a] L. Wos, Some obstacles to the automation of
reasoning, and the problem of redundant information, J. of
Automated Reasoning 3(1):8190, March 1987.
[Wos 1987b] L. Wos, The problem of choosing the inference rule
to employ, J. of Automated Reasoning 3(2):201209, June 1987.
[Wos 1987c] L. Wos, The problem of extending the set of support
strategy, J. of Automated Reasoning 3(3):319328, September 1987.
[Wos 1987d] L. Wos, The problem of definition expansion and
contraction, J. of Automated Reasoning 3(4):433435, December
1987.
*[Wos 1988a] L. Wos, Automated Reasoning: 33 Basic Research
Problems, PrenticeHall, Englewood Cliffs, NJ, 1988.
*[Wos 1988b] L. Wos, The problem of finding a strategy to
control binary paramodulation, J. of Automated Reasoning
4(1):101107, March 1988.
*[Wos 1988c] L. Wos, W. McCune, Challenge problems focusing on
equality and combinatory logic: evaluating automated
theoremproving programs, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
714729.
*[Wos 1988d] L. Wos, The problem of explaining the disparate
performance of hyperresoluton and paramodulation, J. of Automated
Reasoning 4(2):215217, June 1988.
*[Wos 1988e] L. Wos, The problem of selfanalytically choosing
the set of support, J. of Automated Reasoning 4(3):327329,
September 1987.
*[Wos 1988f] L. Wos, The problems of selfanalytically choosing
the weights, J. Automated Reasoning 4(4):463464, December 1988.
[Wos 1988] L. Wos and W. McCune, Searching for fixed point
combinators by using automated theorem proving: a preliminary
report, ANL8810, Argonne National Laboratory, 1988.
[Wos 1989a] L. Wos, R. Overbeek, E. Lusk, Subsumption, a
sometimes undervalued procedure, Preprint MCSP930789,
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):9395, March 1989.
*[Wos 1989c] L. Wos, The problem of determining the size of a
complete set of reductions, J. of Automated Reasoning
5(2):235237, June 1989.
*[Wos 1989d] L. Wos, The problem of guaranteeing the existence
of a complete set of reductions, J. of Automated Reasoning
5(3):399401, September 1989.
*[Wos 1989d] L. Wos, The problem of guaranteeing the absence of
a complete set of reductions, J. Automated Reasoning 5(4):531532,
December 1989.
[Wos 1989e] L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk,
R. Stevens, R. Butler, OTTER experiments pertinent to CADE10,
Tech. Report ANL89/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 (CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes
in Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 485499.
*[Wos 1990b] L. Wos, The problem of choosing between logic
programming and generalpurpose automated reasoning, J. of
Automated Reasoning 6(1):7778, March 1990.
*[Wos 1990c] L. Wos, The problem of finding a mapping between
clause representation and naturaldeduction representation, J. of
Automated Reasoning 6(2):211212, June 1990.
*[Wos 1990d] L. Wos, Meeting the challenge of fifty years of
logic, J. of Automated Reasoning 6(2):213232, June 1990.
*[Wos 1990e] L. Wos, The problem of finding a semantic strategy
for focusing inference rules, J. of Automated Reasoning
6(3):337339, September 1990.
*[Wos 1990f] L. Wos, The problem of choosing between predicate
and function notation for problem representation, J. Automated
Reasoning 6(4):463464, 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):105107, March 1991.
*[Wos 1991b] L. Wos, A wellkept secret of history, J. Automated
Reasoning 7(3):301302, September 1991.
*[Wos 1991c] L. Wos, The problem of choosing the type of
subsumption to use, J. Automated Reasoning 7(3):435438, September
1991.
*[Wos 1991d] L. Wos, The problem of choosing the representation,
inference rule, and strategy, J. Automated Reasoning 7(4):631634,
December 1991.
*[Wos 1992] L. Wos, The impossibility of the automation of
logical reasoning (abstract), 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, p. 14.
[Wrightson 1979] G. Wrightson, A proof procedure for
higherorder modal logic, Proc. 4th Workshop on Automated
Deduction (CADE4, Austin, Texas, 13 February 1979), ed. W.H.
Joyner, 1979, pp. 148154.
[Wrightson 1984a] G. Wrightson, Semantic tableaux, unification
and links, Tech. Report CSDANZARP84001, Department of Computer
Science, Univ. of Wellington, Victoria, New Zealand, 1984.
[Wrightson 1984b] G. Wrightson, Nonclassical logic theorem
proving using links and unification in semantic tableaux, TR
CSDANZARP84003, Victoria Univ., Wellington, New Zealand, 1984.
[Wrightson 1985] G. Wrightson, Nonclassical logic theorem
proving, J. of Automated Reasoning 1(1):3740, 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, 24 November 1987, pp. 553566.
*[Wroblewski 1987] D.A. Wroblewski, Nondestructive graph
unification, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI
87), Seattle, Washington, 1317 July 1987, pp. 582587.
[Wu 1978] Wu Wentsun, On the decision problem and the
mechanization of theorem proving in elementary geometry, Scientia
Sinica 21(2):159172, MarchApril 1978; also Contemp. Math.
29:213234.
[Wu 1979] Wu Wentsun, Mechanical theorem proving in elementary
differential geometry, Scientia Sinica, Mathematics Supplement I,
1979, pp. 94102 (in Chinese); also Science Press, Proc. 1980
Beijing Symp. on Differential Geometry and Differential Equations
2(1982):125138,10731092.
[Wu 1982] Wu W.T., Toward mechanization of geometry  Some
comments on Hilbert's "Grundlagen der Geometrie", Acta
Mathematica Scientia 2(2):125138, 1982.
[Wu 1983] Wu W.T., Some remarks on mechanical theorem proving
in elementary geometry, Acta Mathematica Scientia 3(4):357360,
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.
89118, pp. 235242.
[Wu 1984b] Wu W.T., Basic principles of mechanical theorem
proving in elementary geometries, J. of System Sciences and
Mathematical Sciences 4(3):207235, July 1984; also republished in
J. of Automated Reasoning 2(4):221252, September 1986.
[Wu 1986a] Wu Wentsun, On zeros of algebraic equations  an
application of Ritt's principle, Kexue Tongbao 31(1):15, 1986.
[Wu 1986b] Wu Wentsun, A mechanization method of geometry and
its applications, I. Distances, areas and volumes, J. of Systems
Sci. and Math. Sci 6(1986):204216.
[Wu 1986c] Wu Wentsun, A mechanization method of geometry and
its applications, I. Distances, areas and volumes in Euclidean and
nonEuclidean geometries, Kexue Tongbao 32(1986): 436440.
[Wu 1987a] Wu W.t., On reducibility problem in mechanical
theorem proving of elementary geometries, Chinese Quarterly J. of
Math. 2(1):120, 1987.
[Wu 1987b] Wu Wentsun, A mechanization method of geometry and
its applications, 2. Curve pairs of Bertrand type, Kexue Tongbao
32(1987): 585588.
*[Wu 1991] Wu Wentsun, Mechanical theorem proving of
differential geometries and some of its applications in mechanics,
J. of Automated Reasoning 7(2):171191, June 1991.
*[Wurtz 1992] J. Wurtz, Unifying cycles, Research report
RR9222, 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, 37 August 1992), ed. B. Neumann,
John Wiley & Sons, Chichester, 1992, pp. 6064.
[Xiaorong 1989] Huang Xiaorong, A human oriented proof
presentation model, SEKI Report SR8911, Universitat
Kaiserslautern, 1989.
*[XuHua 1989] L. XuHua, Lock, linear lambdaparamodulation in
operator fuzzy logic, Proc. 11th IJCAI (Detroit, Michigan, USA,
2025 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp.
435440.
[Yamaguchi 1985] T. Yamaguchi, Y. Tezuka, O. Kakusho, Parallel
Processing of Resolution, Proc. 9th IJCAI, Vol. 2, Los Angeles,
CA, 1823 August 1985.
[Yamamoto 1987] A. Yamamoto, A theoretical combination of
SLDresolution and narrowing, Proc. ICLP'87, 1987, pp. 470487.
[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 8301,
October 1983; also ICOT Technical Report TR027, Kyoto Univ.,
October 1983.
[Yates 1970] R. Yates, B. Raphael, T. Hart, Resolution graphs,
Artificial Intelligence 1(34):257289, Winter 1970.
[Yelick 1985a] K. Yelick, Combining unification algorithms for
confined regular equational theories, Proc. 1st Conf. Rewriting
Techniques and Applications (Dijon, France, 2022 May 1985), ed.
J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin, 1985. pp.
365380.
[Yelick 1985b] K. Yelick, A generalized approach to equational
unification, Internal Report MIT/LCS/TR344, MIT, 1985.
[Yelick 1987] K.A. Yelick, Unification in combinations of
collapsefree regular theories, J. of Symbolic Computation 3(1 and
2):153181, 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 (CADE11, Saratoga Springs, NY, USA, June
1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 109123.
[Yelowitz 1976] L. Yelowitz, New results and techniques in
resolution theory, IEEE Trans. on Computers C25(7):673677, July
1976.
[You 1986a] J. You, P.A. Subrahmanyam, Eunification 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, SpringerVerlag, Berlin, 1986,
pp. 454463.
[You 1986b] J.H. You, P.A. Subrahmanyam, A class of confluent
term rewriting systems and unification, J. of Automated Reasoning
2(4):391418, December 1986.
[You 1988] J.H. You, Outer narrowing for equational theories
based on constructors, Proc. ICALP '88, LNCS 317, SpringerVerlag,
pp. 727741, 1988.
*[Young 1989] W.D. Young, A mechanically verified code
generator, J. Automated Reasoning 5(4):493518, December 1989.
*[Yu 1990] Y. Yu, Computer proofs in group theory, J. of
Automated Reasoning 6(3):251286, September 1990.
*[Yuhua 1993] Z. Yuhua, And/Or parallel execution of logic
programs: exploiting dependent andparallelism, ACM SIGPlan
Notices 28(5):1928, May 1993.
[Zadeh 1979] L.A. Zadeh, Approximate reasoning based on fuzzy
logic, Proc. 6th IJCAI, Tokyo, August 1979, pp. 10041010.
[Zaionc 1985] M. Zaionc, The set of unifiers in typed 1calculus
as regular expressions, Proc. 1st Conf. Rewriting Techniques and
Applications (Dijon, France, 2022 May 1985), ed. J.P. Jouannaud,
LNCS 202, SpringerVerlag, Berlin, 1985, pp. 430440.
*[Zaionc 1988] M. Zaionc, Mechanical procedure for proof
construction via closed terms in typed lambda calculus, J.
Automated Reasoning 4(2):173190, 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):5464.
[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, NYLondon, 1971, pp. 26311.
[Zamov 1989] N.K. Zamov, Maslov's inverse method and decidable
classes, Annals of Pure and Aplied Logic 42(1989):165194.
[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, 1519 December
1986), ed. M. Boscarol, L.C. Aiello, and G. Levi, LNCS 306,
SpringerVerlag, 1988, pp. 114139.
*[Zell 1989] A. Zell, T. Braunt, Iterativedeepening Prolog,
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. 919929.
[Zhang 1987] H. Zhang, An efficient algorithm for simple
diphonatine equations, Tech. Report 8726, Dept of Computer
Science, RPI, 1987.
*[Zhang 1988a] H. Zhang, D. Kapur, Firstorder theorem proving
using conditional rewrite rules, 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. 120.
*[Zhang 1988b] H. Zhang, D. Kapur, M.S. Krishnamorrthy, A
mechanizable induction principle for equational specifications,
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. 162181.
[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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 513527.
[Zhang 1990] H. Zhang, Automated proof of ring commutativity
problems by algebraic methods, J. Symbolic Comput. 9(4):423427,
April 1990.
[Zhang 1991] H. Zhang, Cut elimination and automatic proof
procedures, Theor. Comput. Sci 91(2):265284, 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 (CADE11, Saratoga Springs, NY, USA, June
1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 431445.
*[Zhang 1992b] H. Zhang, X. Hua, Herky: High performance
rewriting in RRL, 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. 696700.
[Zucker 1975] J. Zucker, Formalization of classical mathematics
in AUTOMATH, In Colloques Internationaux du Centre Nationale de la
Recherche Scientifique, No 249, 1975, pp. 136145.
