ORA Canada

ORA Canada
Home
Contact us
What's new?
Products and services
Z/EVES
EVES
Ada'95
Reports and Collections
ORA Canada
Bibliography
Automated Deduction
Bibliography
    A-B
    C-E
    F-G
    H-J
    K-L
    M-N
    O-R
    S-T
    U-Z

ORA Canada Bibliography of Automated Deduction: Authors K to L

[Kabulov 1986] V.K. Kabulov, Proof of theorems in the propositional calculus, Dokl. Akad. Nauk USSR 5:5-6, 1986.

*[Kalkbrener 1987] M. Kalkbrener, Solving systems of algebraic equations by using Grobner bases, 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. 282-292.

[Kallick 1965a] B. Kallick, Automatic TP and game playing: A dispassionate view, TIT Res. Inst., Chicago, Ill., January 1965.

[Kallick 1965b] B. Kallick, Theorem-Proving by Computer, TIT Res. Inst., Chicago, Ill., January 1965.

[Kallick 1966] B. Kallick, Theorem-proving by computer, TIT Res. Inst., Chicago, Ill., April 1966.

[Kallick 1968a] B. Kallick, Proof procedures and decision procedures based on the resolution method, PhD thesis, Northwestern Univ., August 1968.

[Kallick 1968b] B. Kallick, A decision procedure based on the resolution method, Proc. IFIP Congr. 1968, 1968, pp. 269-275.

[Kalman 1983] J.A. Kalman, J.G. Peterson, Computer-aided studies of all possible shortest single axioms for the equivalential calculus, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 933-935.

[Kamin 1980a] S. Kamin, J.J. Levy, Attempts for generalising the recursive path orderings, Unpublished manuscript, Dept. of Computer Science, Univ. Illinois, Urbana-Champaign, February 1980.

[Kamin 1980b] S. Kamin, J.J. Levy, Two generalizations of the recursive path ordering, Unpublished manuscript, U. of Illinois at Urbana-Chamgaign, 1980.

[Kanamori 1986] T. Kanamori, H. Fujita, Formulation of induction formulas in verification of PROLOG 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. 281-299.

[Kandri-Rody 1983] A. Kandri-Rody, D. Kapur, On relationship between Buchberger's Grobner basis algorithm and the Knuth-Bendix completion procedure, TIS Report No. 83CRD286, General Electric Research and Development Center, Schenectady, NY, 1983.

[Kandri-Rodi 1984] A. Kandri-Rodi, D. Kapur, Algorithms for computing the Grobner bases of polynomial ideals over various Euclidean rings, Proc. EUROSAM 84 (Cambridge, England, July 9-11, 1984), ed. Fitch, LNCS 174, Springer-Verlag, 1984, pp. 195-208.

[Kandri-Rodi 1985] A. Kandri-Rodi, D. Kapur, P. Narendran, An ideal theoretic approach to word problems and unification problems over finitely presented commutative algebras, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985. pp. 345-364.

*[Kandri-Rody 1988] A. Kandri-Rody, D. Kapur, Computing a Grobner basis of a polynomial ideal over a Euclidean domain, J. of Symbolic Computation 6(1):37-57, August 1988.

*[Kandri-Rody 1988] A. Kandri-Rody, V. Weispfenning, Non-commutative Grobner Bases in algebras of solvable type, MIP-8807, Fakultat fur Mathematik und Informatik, Universitat Passau, March 1988.

[Kandri-Rody 1989] A. Kandri-Rody, D. Mapur, F. Winkler, Knuth-Bendix procedure and Buchberger algorithm---A synthesis, Tech. Report 89-18, Dept. of Computer Science, State Univ. of New York, Albany, NY 1989.

[Kanellakis 1989] P.C. Kanellakis, P.Z. Revesz, On the relationship of congruence closure and unification, J. Symbolic Comput. 7(3&4):427-444, March/April 1989.

[Kanger 1963] S. Kanger, A simplified proof method for elementary logic, In Computer Programming and Formal Systems, ed. P. Braffort and D. Hirschberg, North-Holland Publ., Amsterdam, 1963, pp. 87-94; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 364-371.

[Kapitonova 1972] Y.V. Kapitonova, V.F. Kostyrko, A.V. Lyaletskii, A.I. Degtyarev, A.I. Malashonok, A brief review and bibliography of investigations into automation of search of theorem proofs in formal theories, Kibernetika 8(5):7-18, USSR, September 1972.

*[Kaplan 1983] S. Kaplan, Conditional rewrite rules, Report no. 150, CNRS, France, December 1983; also Theoretical Computer Science 33(1984):175-193;

*[Kaplan 1984] S. Kaplan, Fair conditional term rewriting systems: Unification, termination and confluence, Tech. Report 194, Laboratoire de Recherche en Informatique, Universite de Paris-Sud, Orsay, France, November 1984; also Proc. 3rd Workshop on Theory and Applications of Abstract Data Types (Selected Papers) - Recent Trends in Data Type Specifications, Informatik-Fachberichte 116, ed. H.-J. Kreowski, Springer-Verlag, Berlin, 1985, pp. 136-155.

*[Kaplan 1986a] S. Kaplan, Rewriting with a nondeterministic choice operator: From algebra to proofs, Proc. ESOP 86, 1st European Symp. on Programming (Saarbrucken, FRG, 17-19 March 1986), ed. B. Robinet and R. Wilhelm, LNCS 213, Springer-Verlag, Berlin, 1986, pp. 351-374; also Theor. Comput. Sci 56(1):37-57, January 1988.

[Kaplan 1986b] S. Kaplan, Simplifying conditional term rewriting systems, Internal report, Weizmann Institute, Israel, 1986.

[Kaplan 1987a] S. Kaplan, A compiler for conditional term rewriting systems, Report ESPRIT Project METEOR, task 11; also Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 25-41.

*[Kaplan 1987b] S. Kaplan, Simplifying conditional term rewriting systems: Unification, termination and confluence, J. of Symbolic Computation 4(3):295-334, Academic Press Limited, December 1987.

*[Kaplan 1988a] S. Kaplan, J.-P. Jouannaud, eds., Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems (Orsay, France, 8-10 July 1987), LNCS 308, Springer-Verlag, Berlin, 1988.

*[Kaplan 1988b] S. Kaplan, Positive/negative conditional rewriting, Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems (Orsay, France, 8-10 July 1987), ed. S. Kaplan and J.-P. Jouannaud, LNCS 308, Springer-Verlag, Berlin, 1988, pp. 129-143.

*[Kaplan 1989a] S. Kaplan, C. Choppy, Abstract rewriting with concrete operators, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 178-186.

*[Kaplan 1989b] S. Kaplan, J.-L. Remy, Completion algorithms for conditional rewriting systems, In: Resolution of Equations in Algebraic Structures: Vol 2, Rewriting Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 141-170.

[Kapur 1980] D. Kapur, Krishnamurthy, P. Narendran, A linear algorithm for unification, General Electric Rep. 82CRD-100, NY, 1980.

[Kapur 1983] D. Kapur, P. Narendran, The Knuth-Bendix completion procedure and Thue-systems, Record of the 3rd Conf. on Foundations of Software Technology and Theoretical Computer Science (Bangalore, India, 12-14 December 1983), pp. 363-385; also SIAM J. of Computations 14(4):1052-1070, 1985.

[Kapur 1984a] D. Kapur, B. Krishnamurthy, A natural proof system based on rewriting techniques, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 53-64.

[Kapur 1984b] D. Kapur, G. Sivakumar, Experiments with an architecture of RRL, a Rewrite Rule Laboratory, Report 84GEN008, General Electric Research and Development, April 1984; also 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. 33-56.

[Kapur 1984c] D. Kapur, D.R. Musser, Proof by consistency, 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. 245-267; also GE report 84GEN008, April 1984; also Artificial Intelligence 31(2):125-157, February 1987.

[Kapur 1984d] D. Kapur, B. Krishnamurthy, A natural proof system based on rewriting techniques, 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. 337-348.

[Kapur 1985a] D. Kapur, P. Narendran, G. Sivakumar, A path ordering for proving termination of term rewriting systems, Proc. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Mathematical Foundations of Software Development (Berlin, March 1985), ed. H. Ehrig, C. Floyd, M. Nivat, and T. Thatcher, LNCS 185, Springer-Verlag, Berlin, 1985, pp. 173-187; also 10th Coll. on Trees in Algebra and Programming, 1985.

[Kapur 1985b] D. Kapur, M. Srivas, A rewrite rule based approach for synthesizing abstract data types, Tech. Rep. 84/080, Dept. of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794, July 1984; also Proc. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Mathematical Foundations of Software Development (Berlin, March 1985), ed. H. Ehrig, C. Floyd, M. Nivat, and T. Thatcher, LNCS 185, Springer-Verlag, Berlin, 1985, pp. 188-207.

[Kapur 1985c] D. Kapur, P. Narendran, An equational approach to theorem proving in first-order predicate calculus, Rep. 84CRD322, General Electric Corporate Research and Development, Schenectady, NY, September 1985; also Proc. 7th IJCAI, Los Angeles, August 1985, pp. 1146-1153.

[Kapur 1985d] D. Kapur, M. Krishnamoorthy, R. McNaughton, P. Narendran, An O(|T|3) algorithm for testing the Church-Rosser property of Thue systems, Theoret. Comput. Sci. 35(1):109-114, 1985.

*[Kapur 1985e] D. Kapur, M. Krishnamoorthy, R. McNaughton, P. Narendran, The Church-Rosser property and special Thue systems, Theoretical Computer Science 39(2-3):123-133, August 1985.

[Kapur 1985f] D. Kapur, P. Narendran, A finite Thue system with decidable word problem and without equivalent finite canonical system, Theoretical Computer Science 35(1985):337-344.

[Kapur 1985g] D. Kapur, P. Narendran, H. Zhang, On sufficient completeness and related properties of term rewriting systems, Tech. report, General Electric Company, Corporate Research and Development, Computer Science Branch, Schenectady, NY, 1985; also Acta Informatica 24(4):395-415, 1987.

[Kapur 1986a] D. Kapur, D.R. Musser, Inductive reasoning with incomplete specifications, Proc. IEEE Symp. on Logic in Computer Science, Cambridge, MA, 16-18 June 1986, pp. 367-377.

[Kapur 1986b] D. Kapur, P. Narendran, H. Zhang, Proof by induction using test sets, 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. 99-117.

*[Kapur 1986c] D. Kapur, P. Narendran, NP-completeness of the set unification and matching 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. 489-495.

[Kapur 1986d] D. Kapur, G. Sivakumar, H. Zhang, RRL: A Rewrite Rule Laboratory, 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. 691-692.

[Kapur 1986e] D. Kapur, H. Zhang, RRL: A Rewrite Rule Laboratory - User's Manual, Unpublished manuscript, General Electric Corporate Research and Development, Schenectady, NY, March 1986; Published April 1987; also Report 89-03, Dept. of Computer Science, Univ. of Iowa, May 1989.

*[Kapur 1986f] D. Kapur, Geometry theorem proving using Hilbert's Nullstellensatz, Proc. 1986 ACM-SIGSAM Symp. on Symbolic and Algebraic Computation (SYMSAC '86, Univ. of Waterloo, Waterloo, Ontario, 21-23 July 1986), ed. B.W. Char, ACM, New York, NY, 1986, pp. 202-208. [Kapur 1986g] D. Kapur, Using Grobner bases to reason about geometry problems, J. of Symbolic Computation 2(4):399-408, December 1986.

[Kapur 1986h] D. Kapur, P. Narendran, NP-Completeness of associative-commutative unification check and related problems, General Electric Company, Schenectady, NY, 1987.

[Kapur 1986i] D. Kapur, P. Narendran, F. Otto, On ground-confluence of term rewriting systems, Tech. Report 87-6, Dept. of Computer Science State Univ. of New York, Albany, NY, and General Electric R & D Center, Schenectady, NY, 1987.

*[Kapur 1986j] D. Kapur, J.L. Mundy, Wu's method and its application to perspective viewing, Proc. Workshop on Geometric Reasoning, Oxford Univ., June 30-July 3, 1986, In: Artificial Intelligence 37(1-3):15-36, December 1988.

*[Kapur 1986k] D. Kapur, A refutational approach to geometry theorem proving, Proc. Workshop on Geometric Reasoning, Oxford Univ., June 30 - July 3, 1986, In: Artificial Intelligence 37(1-3):61-93, December 1988.

*[Kapur 1987a] D. Kapur, P. Narendran, Matching, unification and complexity, SIGSAM Bulletin 21(4):6-9, November 1987.

[Kapur 1987b] D. Kapur, P. Narendran, D.J. Rosenkrantz, H. Zhang, Sufficient-completeness, quais-reducibility and their complexity, Tech. Report, Dept. of Computer Science, State Univ. of New York, Albany, NY. 1987.

*[Kapur 1988a] D. Kapur, H. Zhang, RRL: A rewrite rule laboratory, 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. 768-769.

*[Kapur 1988b] D. Kapur, D.R. Musser, P. Narendran, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Tech. Report, General Electric Company, Corporate Research and Development, Computer Science Branch, Schenectady, NY (update of 1985 draft); also J. of Symbolic Computation 6(1):19-36, August 1988.

*[Kapur 1988c] D. Kapur, H. Zhang, Proving equivalence of different axiomatizations of free groups, J. Automated Reasoning 4(3):331-352, September 1988.

*[Kapur 1989a] D. Kapur, H. Zhang, An overview of Rewrite Rule Laboratory (RRL), Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 559-563.

[Kapur 1989b] D. Kapur, H. Zhang, Rewrite rule laboratory user's manual, Tech. Report 89-03, Dept. of Computer Science, Univ. of Iowa, 1989.

[Kapur 1989c] D. Kapur, J.L. Mundy (ed.) Geometric reasoning, MIT Press, June 1989.

[Kapur 1989d] D. Kapur, P. Narendran, F. Otto, On ground confluence of term rewriting systes, Inform. Comput. 86(1):14-31, 1989.

*[Kapur 1990] D. Kapur, H.K. Wan, Refutational proofs of geometry theorems via characteristic set computation, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, pp. 277-284.

*[Kapur 1992] D. Kapur, ed. Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992.

*[Kapur 1994] D. Kapur, X. Nie, Reasoning about numbers in Tecton, Institute for Programming and Logics, Dept. of Computer Science, State University of New York at Albany, June 1992, revised March 1994.

[Karp 1972] M. Karp, Rosenberg, Rapid identification of repeated patterns in strings, trees and arrays, ACM Symp. on Th. of Com. 4., 1972.

[Karp 1985] R.M. Karp, E. Upfal, A. Wigderson, Constructing a perfect matching is in random NC, Proc. 17th ACM STOC, 1985, pp. 22-32.

[Karr 1985] M. Karr, "Delayability" in proofs of strong normalizability in the typed lambda calculus, Proc. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Mathematical Foundations of Software Development (Berlin, March 1985), ed. H. Ehrig, C. Floyd, M. Nivat, and T. Thatcher, LNCS 185, Springer-Verlag, Berlin, 1985, pp. 208-222.

[Kaufl 1985] Th. Kaufl, The simplifier of the program verifier "Tatzelwurm", Proc. Osterreichische Artificial Intelligence-Tagung, Wien (24-27 September 1985), Informatik-Fachberichte 106, Springer-Verlag, Berlin, 1985, pp. 185-193.

[Kaufl 1986] Th. Kaufl, Program verifier `Tatzelwurm': Reasoning about systems of linear inequalities, Tech. Report 16/87, Univ. of Karlsruhe, Institut fur Logik, Komplexitat und Deduktionssystme, 1987; also 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. 300-305.

*[Kaufl 1988a] T. Kaufl, Reasoning about systems of linear inequalities, 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. 563-572.

[Kaufl 1988b] T. Kaufl, Simplification and decision of linear inequalities over the integers, Tech. Report 9/88, Univ. of Karlsruhe, Institut fur Logik, Komplexitat und Deduktionssysteme, 1988.

[Kaufl 1989] T. Kaufl, Cooperation of decision procedures in a tableau-based theorem prover, Tech. Report 16/89, Univ. of Karlsruhe, Institut fur Logik, Komplexitat und Deduktionssysteme, 1988.

*[Kaufl 1990] T. Kaufl, N. Zabel, The theorem prover of the program verifier Tatzelwurm (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. 657-658.

[Kaufmann 1987] M. Kaufmann, A user's manual for an interactive enhancement to the Boyer-Moore Theorem Prover, Tech. Report 60, Institute for Computing Science, Univ. of Texas at Austin, Austin, Texas, August 1987; also Tech. Report 19, Computational Logic, Inc., May 1988.

*[Kaufmann 1988] M. Kaufmann, An interactive enhancement to the Boyer-Moore Theorem Prover, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 735-736.

[Kaufmann 1989a] M. Kaufmann, A user's manual for RCL, Internal Note 157, Computational Logic, Inc., October 1989.

[Kaufmann 1989b] M. Kaufmann, Addition of free variables to an interactive enhancement of the Boyer-Moore Theorem Prover, Tech. Report 42, Computational Logic, Inc., Austin, Texas, May 1989.

[Kaufmann 1989c] M. Kaufmann, DEFN-SK: An extension of the Boyer-Moore theorem prover to handle first-order quantifiers, Tech. Report 43, Computational Logic, Inc., Austin, Texas, June 1989.

*[Kaufmann 1990a] M. Kaufmann, RCL: A Lisp verification 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. 659-660.

*[Kaufmann 1990b] M. Kaufmann, Generalization in the presence of free variables: a mechanically-checked correctness proof for one algorithm, Tech. Report 53, Computational Logic, Inc., Austin, Texas, 1990; also J. Automated Reasoning 7(1):109-158, March 1991.

[Kaufmann 1990c] M. Kaufmann, An integer library for NQTHM, Internal Note 182, Computational Logic, Inc., 1990.

[Kedem 1988] Z.M. Kedem, K.V. Palem, Optimal parallel algorithms for forest and term matching, Tech. report, IBM Thomas J. Watson Research Center, June 1988.

[Keller 1986] R.M. Keller and M.R. Sleep, Applicative caching. ACM Transactions on Programming Languages and Systems 8(1):88-108, January 1986.

[Kellerman 1971] E. Kellerman, Unification algorithm for theorem proving, IBM Tech. Disclosure Bull. 13(11), April 1971

[Kerber 1989] M. Kerber, Some aspects of analogy in mathematical reasoning, SEKI Report SR-89-12, Universitat Kaiserslautern, 1989.

*[Kerber 1990] M. Kerber, How to prove higher order theorems in first order logic, SEKI Report 90-19, Fachbereich Informatik, Universitat Kaiserslautern, Kaiserslautern, Germany, 1990; also Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1 (IJCAI-91, Darling Harbour, Sydney, Australia, 24-30 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp. 137-142.

[Kerchner 1983] H. Kerchner, A general completion algorithm for equational term rewriting systems and its proof of correctness. Rep. CRIN, Nancy, 1983.

*[Kesner 1992] D. Kesner, Free sequentiality in orthogonal order-sorted rewriting systems with constructors, 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. 603-617.

[Ketonen 1983a] J. Ketonen, J. Weening, EKL - An interactive proof checker, Users' Reference Manual, Dept. of Computer Science, Stanford Univ., 1983, 40 pp.; also Tech. Report 1006, Stanford Univ., 1984.

[Ketonen 1983b] J. Ketonen, J. Weening, The language of an interactive proof checker, Stanford Univ., CS Report STAN-CS-83-992, 1983, 34pp.

[Ketonen 1983c] J. Ketonen, R. Weyhrauch, A semidecision procedure for predicate calculus, to appear in the J. of Theoretical Computer Science, 1984, 16pp.

[Ketonen 1983d] J. Ketonen, A mechanical proof of Ramsey theorem, Stanford Univ., CA, October 1983.

[Ketonen 1984a] J. Ketonen, EKL - A mathematically oriented proof checker, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 65-79.

[Ketonen 1984b] J. Ketonen, R. Weyhrauch, A decidable fragment of predicate calculus, Theoretical Computer Science 32(1984):297-307.

[Ketonen 1986] J. Ketonen, G. Bellin, Experiments in Automatic Theorem Proving, STAN-CS-87-1155, Stanford Univ. Computer Science, December 1986.

*[Khoshnevisan 1989] H. Khoshnevisan, K.M. Sephton, InX: An automatic function inverter, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 564-568.

*[Kim 1989] M.Y. Kim, Visual reasoning in geometry theorem proving, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 1617-1622.

[King 1969] J.C. King, A program verifier, PhD thesis, Carnegie-Mellon Univ., 1969.

[King 1970] J.C. King, R.W. Floyd, An interpretation-oriented theorem prover over the integers, Proc. 2nd ACM Symp. on Comput. Theory, 1970, pp. 169-179; also J. of Computer and System Sciences 6(1972):305-323.

[Kirchner 1981] C. Kirchner, H. Kirchner, J.P. Jouannaud, Algebraic manipulations as a unification and matching strategy for linear equations in signed binary trees, Proc. 7th IJCAI, Vancouver, Canada, 1981.

[Kirchner 1983] C. Kirchner, A new unification method in equational theories and its application to the MINUS theories, Internal report CRIN, 1983.

[Kirchner 1984a] C. Kirchner, A new equational unification method: A generalization of Martelli-Montanari's algorithm, 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. 77-100; also Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 224-247.

[Kirchner 1984b] H. Kirchner, A general inductive completion algorithm and application to abstract data types, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 282-302.

*[Kirchner 1984c] C. Kirchner, H. Kirchner, Implementation of a general completion procedure parameterized by built-in theories and strategies (demonstration), Rapport Crin 84-R-85, 1984; also 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. 402-404.

[Kirchner 1984d] C. Kirchner, Standardizations of equational unification: Abstract and examples, Internal Report 84-R-074, Centre de Recherche en Informatique, Nancy, France, 1984.

[Kirchner 1986] C. Kirchner, Computing unification algorithms, Proc. 1st IEEE Symp. on Logic in Computer Science (Cambridge, MA, 16-18 June 1986), IEEE Computer Society, 1986, pp. 206-216.

[Kirchner 1987a] C. Kirchner, Methods and tools for equational unification, CNRS technical report Nr. 87-R-008, Univ. of Nancy I, 1987.

[Kirchner 1987b] C. Kirchner, P. Lescanne, Solving disequations, Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca, NY, 22-25 June 1987, pp. 347-352.

[Kirchner 1987c] H. Kirchner, Schematization of infinite sets of rewrite rules: Application of the divergence of completion processes, Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), ed. P. Lescanne, LNCS 256, Springer-Verlag, Berlin, 1987, pp. 180-191.

[Kirchner 1987d] C. Kirchner, H. Kirchner, REVEUR-3: Implementation of a general completion procedure parameterized by built-in theories and strategies, J. Sci. Comput. Programming, 8(1):69-86, 1987.

[Kirchner 1987e] C. Kirchner, ed. Proc. on a workshop on unification, Centre de Recherche en Informatique de Nancy, BP 239, 54506 Vandoeuver-les-Nancy, France, 1987.

[Kirchner 1989a] C. Kirchner, ed., Special Issue on Unification, J. of Symbolic Computation, 1989.

[Kirchner 1989b] H. Kirchner, Schematization of infinite sets of rewrite rules generated by divergent completion processes, Theoretical Computer Science 67(2,3):303-332, October 1989.

*[Kirchner 1989c] C. Kirchner, From unification in combination of equational theories to a new AC-unification algorithm, In: Resolution of Equations in Algebraic Structures: Vol 2, Rewriting Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 171-210.

[Kirchner 1989d] C. Kirchner, H. Kirchner, Constrained equational reasoning, Report CRIN 89-R-220, 1989; also Proc. ACM-SIGSAM 1989 Intl. Symp. on Symbolic and Algebraic Computation (Portland, Oregon), ACM Press, pp. 382-389.

*[Kirchner 1990a] C. Kirchner, Equational unification (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. 682.

*[Kirchner 1990b] C. Kirchner, F. Klay, Syntactic theories and unification, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 270-277.

[Kirchner 1990c] C. Kirchner (ed), Unification, Academic Press, San Diego, 1990.

[Kirchner 1990d] C. Kirchner, P. Viry, Implementing parallel rewriting, Research report, CRIN, 1990.

[Klaeren 1987] H. Klaeren, K. Indermark, A new technique for compiling recursive function definitions, To appear in Proc. of the METEOR Workshop, Algebraic Methods: Theory, Tools And Applications, Passau, 1987.

[Klahr 1979] P. Klahr, Partial proofs and partial answers, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 115-121.

[Kleene 1952] S.C. Kleene, Introduction to Metamathematics, Van Nostrand, Princeton, NJ, 1952.

[Kleer 1984a] J. De Kleer, J.S. Brown, A qualitative physics based on confluences, Artificial Intelligence 24(1984):7-83.

[Kleer 1984b] J. De Kleer, Choices without backtracking, AAAI-84, 1984, pp. 79-85.

[Kleine Buning 1985a] H. Kleine Buning, Complexity results for classes of first-order formulas with identity and conjunctive quantificational form, Forschungsberichte der Universitat Karlsruhe, 1985.

[Kleine Buning 1985b] H. Kleine Buning, T. Lettmann, First-order formulas in conjunctive quantificational form, Forschungsberichte der Universitat Karlsruhe, 1985.

[Kleine Buning 1986] H. Kleine Buning, T. Lettmann, Classes of first order formulas under various satisfiability definitions, 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. 553-563.

*[Kliger 1990] S. Kliger, E. Shapiro, From decision trees to decision graphs, Logic Programming: Proc. of the 1990 North American Conf., ed. S. Debray and M. Hermenegildo, MIT Press, 1990, pp. 97-116.

[Kling 1969] R.E. Kling, An information processing approach to reasoning by analogy, Artificial Intelligence Group TN10, Stanford Research Institute, Menlo Park, CA, June 1969.

[Kling 1970] R.E. Kling, Design implications of theorem proving strategies, AI Group Tech. Note 44, Stanford Research Institute, Menlo Park, CA, 1970.

*[Kling 1971] R.E. Kling, A paradigm for reasoning by analogy, Proc. 2nd IJCAI, Imperial College, London, 1-3 September 1971, pp. 568-585; also Artificial Intelligence 2(1971):147-178.

[Kling 1972] R.E. Kling, C.V. Freiman, Reasoning by analogy as an aid to heuristic theorem proving, Information Processing 71, Proc. IFIP Congress 1971, vol 1:195-200, North-Holland, 1972.

[Klop 1980] J.W. Klop, Combinatory reduction systems, PhD thesis, Mathematisch Centrum, Amsterdam, 1980.

[Klop 1987a] J.W. Klop, Term rewriting systems: A tutorial, Rep. IR 126, Centre for Math. and C.S., Amsterdam, 1987; also Bulletin of the European Association for Theoretical Computer Science 32, June 1987, pp. 143-182.

[Klop 1987b] J.W. Klop, A. Middeldorp, Strongly sequential term rewriting systems, Report CS-R8730, Centre for Mathematics and Computer Science, Amsterdam, 1987.

[Klop 1990a] J.W. Klop, Term rewriting systems: From Church-Rosser to Knuth-Bendix and beyond, Proc. 17th Intl. Colloquium on Automata, Languages and Programming, LNCS 443, Springer-Verlag, Berlin, pp. 350-369.

[Klop 1990b] J.W. Klop, Term rewriting systems, In: Handbook of Logic in Computer Science, ed. S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, Oxford, Oxford University Press, To appear.

[Knight 1989] K.Knight, Unification: A multidisciplinary survey, ACM Computing Surveys 21(1), 1989.

[Knoblock 1986] T. Knoblock, R.L. Constable, Formalized metareasoning in type theory, Tech. Report TR-86-742, Dept. of Computer Science, Cornell Univ., 1986; also Proc. 1st Annual IEEE Symp. on Logic in Computer Science, ed. A.K. Chandra and A.R. Meyer, 1986, pp. 237-248.

[Knuth 1970] D. Knuth, P. Bendix, Simple word problems in universal algebras, in Computational Problems in Abstract Algebras, ed. J. Leech, Pergamon Press, Oxford, 1970, pp. 263-297; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 342-376.

[Knuth 1974] M. Knuth, Pratt, Fast Pattern Matching in Strings, Stan-CS-74-440, Stanford Univ., Comp. Sci. Dept., 1974.

[Ko 1985a] H.-P. Ko, M.A. Hussain, ALGE-Prover: An algebraic geometry theorem proving software, Tech. report 85CRD139, General Electric Corporate Research and Development, Schenectady, NY, 1985.

[Ko 1985b] H.-P. Ko, M.A. Hussain, A study of Wu's method - A method to prove certain theorems in elementary geometry. Congr. Numer. 48(1985):225-242.

*[Ko 1986a] H.P. Ko, Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle, Proc. Workshop on Geometric Reasoning, Oxford Univ., June 30 - July 3, 1986, In: Artificial Intelligence 37(1-3):95-122, December 1988.

[Ko 1986b] H.-P. Ko, ALGE-prover II: A new edition of ALGE-prover, Tech. Report 86CRD081, General Electric Company, Schenectady, NY, 1986.

[Ko 1989] H.P. Ko, S.C. Shou, A decision method for certain algebraic geometry problems, Rocky Mountain J. of Mathematics 19(3):709-724, 1989.

*[Kobayashi 1986] H. Kobayashi, A. Furukawa, T. Sasaki, Grobner bases of ideals of convergent power series, Proc. 1986 ACM-SIGSAM Symp. on Symbolic and Algebraic Computation (SYMSAC '86, Univ. of Waterloo, Waterloo, Ontario, 21-23 July 1986), ed. B.W. Char, ACM, New York, NY, 1986, pp. 225-227.

[Kodratoff 1983] Y. Kodratoff, J. Castaing, Trivializing the proof of trivial theorems, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 930-932.

*[Kolyada nd] S.V. Kolyada Systems for symbolic computations in boolean algebra, Glushkov Institute fo Cybernetics, nd (after 1989).

[Konolige 1982] K. Konolige, A first-order formalism of knowledge and action for a multi-agent planning system, Machine Intelligence 9, ed. Hayes, Michie and Pao, Ellis Harwood Ltd., Chichester, 1982, pp. 41-72.

[Konolige 1986a] K. Konolige, Resolution and quantified epistemic logics, 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. 199-208.

[Konolige 1986b] K. Konolige, A Deduction Model of Belief, Morgan-Kaufmann Pub., 1986.

[Konolige 1986c] K. Konolige, A resolution method for quantified modal logics of knowledge and belief, Proc. 1986 Conf. on Reasoning about Knowledge, ed. J.Y. Halpern, pp. 309-324.

*[Korf 1985a] R.E. Korf, Depth-first iterative-deepening: an optimal admissible tree search, Artificial Intelligence 27(1):97-109, September 1985.

*[Korf 1985b] R.E. Korf, Iterative-Deepening-A: An optimal admissible tree search, Proc. 9th Intl. Joint Conf. on Artificial Intelligence, Vol. 2 (IJCAI-85, 18-23 August 1985), pp. 1034-1036.

[Korf 1986] R.E. Korf, Learning to solve problems by searching for macro-operators, Research Notes in Artificial Intelligence 5, Pitman Publ. Ltd., London, 1985.

*[Korf 1992] R.E. Korf, Linear-space best-first search: summary of results, Proc. 10th National Conf. on Artificial Intelligence (AAAI-92, 12-16 July 1992), AAAI Press, Menlo Park, CA, 1992, pp. 533-538.

[Kott 1982] L. Kott, McCarthy's recursion induction principle: `oldy' but `goody', Univ. of Paris VII LITP 2, Paris, France, March 1982.

[Kounalis 1985] E. Kounalis, H. Zhang, A general completeness test for equational specifications, CRIN (85-R-05), Nancy, France, January 1985.

*[Kounalis 1988a] E. Kounalis, M. Rusinowitch, On word problems in Horn theories, Proc. 1st Intl. Workshop on Conditional Term Rewriting Systems (Orsay, France, 8-10 July 1987), ed. S. Kaplan and J.-P. Jouannaud, LNCS 308, Springer-Verlag, Berlin, 1988, pp. 144-160; 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. 527-537.

*[Kounalis 1990] E. Kounalis, M. Rusinowitch, Mechanizing inductive reasoning, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 240-245; also Bull. EATCS 41(1990):216-226.

[Kowalski 1968] R. Kowalski, An exposition of paramodulation with refinements, Univ. of Edinburgh, Edinburgh, Scotland, DCL Memo No. 19, October 1968.

[Kowalski 1969] R. Kowalski, P. Hayes, Semantic trees in automatic theorem-proving, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 87-101; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 217-232.

[Kowalski 1970a] R. Kowalski, Studies in the completeness and efficiency of theorem-proving by resolution, PhD, Univ. of Edinburgh, Edinburgh, Scotland, 1970.

[Kowalski 1970b] R. Kowalski, Search strategies for theorem-proving, Machine Intelligence 5, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1970, pp. 181-201.

[Kowalski 1970c] R. Kowalski, The case for using equality axioms in automatic demonstration, Symp. on Automatic Demonstration, Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 112-127; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 377-398.

[Kowalski 1971a] R. Kowalski, D. Kuhner, Linear resolution with selection function, Artificial Intelligence 2(3-4):227-260, Winter 1971; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 542-577.

[Kowalski 1971b] R. Kowalski, P.J. Hayes, Lecture notes on automatic theorem proving, DCL Memo 40, Univ. of Edinburgh, 1971.

[Kowalski 1972] R.A. Kowalski, And-or graphs, theorem proving graphs and bi-directional search, Machine Intelligence 7, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, 1972, pp. 167-194.

[Kowalski 1974] R. Kowalski, Predicate logic as a programming language, Information Processing 74, NY: Elsevier North-Holland, 1974, pp. 569-574.

[Kowalski 1975] R. Kowalski, A proof procedure using connection graphs, JACM 22(4):572-595, October 1975.

[Kowalski 1979] R.A. Kowalski, Logic for Problem Solving, Elsevier North-Holland Inc., NY, 1979.

[Kozen 1981] D. Kozen, Positive first-order logic is NP-complete, IBM J. Res. Dev. 25(4):327-332, 1981.

[Krafft 1981a] D.B. Krafft, AVID: A system for the interactive development of verifiably correct programs, Doctoral Dissertation, Computer Science Dept., Cornell Univ., 1981.

[Krafft 1981b] D.B. Krafft, A.J. Demers, Determining logical dependency in a decision procedure for equality, TR 81-458, Dept. of Computer Science, Cornell Univ., Ithaca, NY, April 18, 1981.

[Krafft 1981c] D.B. Krafft, A computer system for creating proofs, PhD thesis, Cornell Univ., August 1981.

[Kramer 1989] F.-J. Kramer, A decision procedure for Presburger arithmetic with functions and equality, SEKI Working Paper SWP-89-04, Universitat Kaiserslautern, 1989.

[Kramosil 1975] I. Kramosil, A note on deductive rules with negative premises, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975, pp. 53-56.

[Kreisel 1970] G. Kreisel Hilbert's program and the search for automatic proof procedures, In Symp. on Automatic Demonstration, Lecture Notes in Mathematics 125, Springer-Verlag, NY, 1970, pp. 128-146.

[Kreisel 1981] G. Kreisel Neglected possibilities of processing assertions and proofs mechanically: Choice of problems and data, in U.-Level Computer-Assisted Instruction at Stanford; 1968-1980, ed. Patrick Suppes, IMSSS, Stanford, 1981.

[Kreitz 1986] C. Kreitz, Constructive automata theory implemented with the Nuprl Proof Development Systems, Report 86-779, Dept. of Computer Science, Cornell Univ., September 1986;

[Krishnamurthy 1981] B. Krishnamurthy, R.N. Moll, Examples of hard tautologies in the propositional calculus, Proc. 13th ACM Symp. on Th. of Computing, 1981, pp. 28-37.

*[Krishnamurthy 1985] B. Krishnamurthy, Short proofs for tricky formulas, Acta Informatica 22(3):253-275, August 1985.

[Kroger 1976] F. Kroger, Logical rules for natural reasoning about programs, Proc. Automata, Languages and Programming, ed. Michaelson and Milner, Edinburgh Press, Edinburgh, 1976, pp. 87-98.

[Kuchlin 1982a] W. Kuchlin, Some reduction strategies for algebraic term rewriting, SIGSAM Bulletin 16(4):13-23, Issue 64, November 1982.

[Kuchlin 1982b] W. Kuchlin, A theorem-proving approach to the Knuth-Bendix completion algorithm, In Computer Algebra, Proc. EUROSAM 1982 (April 1982), ed. J. Calmet, LNCS 144, Springer-Verlag, pp. 101-108; also J. of Computer and System Science 23(1), 1981.

[Kuchlin 1982c] W. Kuchlin, An implementation and investigation of the Knuth-Bendix completion procedure, Interner Bericht 17/82, Institut fur Informatik, Universitat Karlsruhe, April 1982.

*[Kuchlin 1985] W. Kuchlin, A confluence criterion based on the generalised Newman lemma (full paper: demonstration), 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. 390-399.

[Kuchlin 1986a] W. Kuchlin, Equational completion by proof simplification, Tech. Report 86-02, Dept. of Mathematics, ETH, Zurich, Switzerland, 1986.

[Kuchlin 1986b] W. Kuchlin, Equational completion by proof transformation, PhD thesis, Dept. of Mathematics, Swiss Federal Institute of Technology (ETH), CH-8092, Zurich, Switzerland, June 1986.

[Kuchlin 1986c] W. Kuchlin, A generalized Knuth-Bendix algorithm, Tech. Report 86-01, Dept. of Mathematics, Swiss Federal Institute of Technology (ETH), Zurich, Switzerland, 1986.

*[Kuchlin 1987] W. Kuchlin, Inductive completion by ground proof transformation, Tech. Report 87-08, Dept. of Computer and Information Sciences, Univ. of Delaware, Newark, DE, February 1987; In: Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, ed. H. Ait-Kaci and M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 211-244.

*[Kuhn 1990] N. Kuhn, K. Madlener, F. Otto, A test for lambda-confluence for certain prefix rewriting systems with applications to the generalized word problem, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, pp. 8-15.

[Kuhner 1969] D. Kuhner, Bi-Directional Search with Horn Clauses, DCL Memo No. 20, Univ. of Edinburgh, Scotland, 1969.

[Kuhner 1971] D.G. Kuhner, A note on the relation between resolution and Maslov's inverse method, Machine Intelligence 6, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1971, pp. 73-90.

[Kuhner 1972] D. Kuhner, Some special purpose resolution systems, Machine Intelligence 7, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1972, pp. 117-128.

[Kuhner 1977] S. Kuhner, C. Mathis, P. Raulefs, J. Siekmann, Unification of idempotent function, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, p. 528.

[Kuhner 1980] D. Kuhner, Theorem proving by reducing connection graphs, Proc. 3rd Biennial Conf. of the Canadian Society for Computational Studies of Intelligence, Univ. of Victoria, Victoria, B.C., May 1980, pp. 49-54.

*[Kundu 1986] S. Kundu, Tree resolution and generalized semantic tree, Proc. of the ACM SIGART Intl. Symp. on Methodologies for Intelligent Systems, ed. Z.W. Ras and M. Zemankova, Knoxville, TN, 22-24 October 1986, pp. 270-278.

*[Kuper 1988] G.M. Kuper, K.W. McAloon, K.V. Pallem, K.J. Perry, Efficient parallel algorithms for anti-unification and relative complement, Tech. report IBM, 1987; also Proc. 3rd Annual Symp. on Logic in Computer Science (Edinburgh, Scotland, 5-8 July 1988), IEEE, 1988, pp. 112-120.

*[Kusche 1987] K. Kusche, B. Kutzler, H. Mayr, Implementation of a geometry theorem proving package in SCRATCHPAD II, 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. 246-257.

[Kutzler 1986a] B. Kutzler, S. Stifter, A geometry theorem prover based on Buchberger's algorithm, 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. 693-694.

[Kutzler 1986b] B. Kutzler, S. Stifter, Collection of computerized proofs of geometry theorems, Technical report 86-12.0, Res. Inst. Symbol. Comput., Univ. Linz, Austria, 1986.

[Kutzler 1986c] B. Kutzler, S. Stifter, New approaches to computerized proofs of geometry theorems, Preprint, Univ. Linz, 1986; also Proc. Computers and Mathematics, ed. R. Gebauer and J. Davenport, Stanford, USA, July 1986.

[Kutzler 1986d] B. Kutzler, S. Stifter, On the application of Buchberger's algorithm to automated geometry theorem proving, J. of Symbolic Computation 2(4):389-397, December 1986.

*[Kutzler 1986e] B. Kutzler, S. Stifter, Automated geometry theorem proving using Buchberger's algorithm, Proc. 1986 ACM-SIGSAM Symp. on Symbolic and Algebraic Computation (SYMSAC '86, Univ. of Waterloo, Waterloo, Ontario, 21-23 July 1986), ed. B.W. Char, ACM, New York, NY, 1986, pp. 209-214.

[Kutzler 1987] B. Kutzler, Implementation of a geometry proving package in SCRATCH-PAD II, Proc. EUROCAL '87 Conf., Leipzig, 2-5 June 1987, to appear.

[Kutzler 1988] B. Kutzler, Algebraic methods for geometric theorem proving, PhD thesis. Univ. Linz, Austria, 1988.

[Kuvoda 1960] S. Kuvoda, An investigation of the logical structure of maths, XIII, A Method of Programming Proofs in Maths for Electr. Computers, Magoya Mathem. J. 16(1960):195-203.

[Ladner 1977] R.E. Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM J. Computing 6(3):467-480, 1977.

[Lafon 1985] E. Lafon, C.B. Schwind, A theorem prover for action performance, Proc. ECAI'88, 1988.

*[Lai 1989] M. Lai, On how to move mountains `associatively and commutatively', Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 187-202.

*[Laird 1990] P. Laird, E. Gamble, Extending EBG to term-rewriting systems, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990, 1990), Vol. 2, AAAI Press/The MIT Press, Menlo Park/Cambridge, pp. 929-935.

[Lakatos 1976] I. Lakatos, Proofs and refutations: The logic of mathematical discovery, Cambridge Univ. Press, London, 1976.

[Lam 1990] C.W.H. Lam, How reliable is a computer-based proof? Mathematical Intelligence 12(1), 1990.

[Lamping 1990] J. Lamping, An algorithm for optimal lambda calculus reduction, Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages (San Francisco, CA, 17-19 January 1990), ACM, 1990, pp. 16-30.

[Lankford 1972] D. Lankford, Equality atom term locking, PhD thesis, Univ. of Texas at Austin, December 1972, 88pp.

[Lankford 1975a] D.S. Lankford, Canonical algebraic simplification in computational logic, Technical Report ATP-25, Automatic Theorem Proving Project, Univ. of Texas at Austin, Math. Dept., May 1975.

[Lankford 1975b] D.S. Lankford, Canonical inference, Tech. Report ATP-32, Automatic Theorem Proving Project, Dept. Mathematics and Computer Science, Univ. of Texas at Austin, December 1975.

[Lankford 1977a] D. Lankford, A. Ballantyne, Decision procedures for simple equational theories with permutative equations: Complete sets of permutative reductions, Rep. ATP-37, Dept. Math. and Comput. Sci., Univ. of Texas at Austin, 1977; also Workshop on Automatic Deduction, MIT, Cambridge, MA, 1977.

[Lankford 1977b] D.S. Lankford, A.M. Ballantyne, Decision procedures for simple equational theories with commutative axioms: Complete sets of commutative reductions, Rep. ATP-35, Dept. Math. and Comput. Sci., Univ. of Texas at Austin, March 1977.

[Lankford 1977c] D.S. Lankford, A.M. Ballantyne, Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions, Rep. ATP-39, Dept. Math. and Comput. Sci., Univ. of Texas, August 1977.

[Lankford 1977d] D.S. Lankford, Some approaches to equality for computational logic: A survey and assessment. Memo ATP-36, Automatic Theorem Proving Project, Univ. of Texas at Austin, 1977.

[Lankford 1978] D. Lankford, D. Musser, On semideciding first order validity and invalidity, Report, USC Information Sciences Institute, July 1978.

[Lankford 1979a] D.S. Lankford, A unification algorithm for Abelian group theory, MTP-1, Math. Dept., Louisiana Tech. Univ., Ruston, 1979.

[Lankford 1979b] D.S. Lankford, Mechanical theorem proving in field theory, MTP-2, Math. Dept., Louisiana Tech. Univ., January 1979.

[Lankford 1979c] D.S. Lankford, On proving term rewriting systems are Noetherian, Tech. report MTP-3, Math. Dept., Louisiana Tech. Univ., Ruston, May 1979.

[Lankford 1979d] D.S. Lankford, Some new approaches to the theory and application of conditional term rewriting systems, Research report MTP-6, Math. Dept., Louisiana Tech. Univ., Ruston, Louisiana, August 1979.

[Lankford 1979e] D.S. Lankford, M. Ballantyne, The refutation completeness of blocked permutative narrowing and resolution, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979.

[Lankford 1980a] D.S. Lankford, A new complete FPA-unification algorithm, Tech. Report MTP-8, Louisiana Tech. Univ., Ruston, 1980.

[Lankford 1980b] D.S. Lankford, Some remarks on inductionless induction, Tech. Report MTP-11, Louisiana Tech. Univ., Ruston, LA, 1980.

[Lankford 1981] D.S. Lankford, A simple explanation of inductionless induction, Tech. Report MTP-14, Math. Dept., Louisiana Tech. Univ., Ruston, LA, August 1981.

[Lankford 1983] D.S. Lankford, G. Butler, B. Brady, Abelian group unification algorithms for elementary terms, Math. Dept. Louisiana Tech. Univ., Ruston, Louisiana 71272, 1983; also Contemporary Math. 29(1984):193-199; also 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. 101-108.

[Lankford 1984a] D. Lankford, G. Butler, A. Ballantyne, A progress report on new decision algorithms for finitely presented Abelian groups, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 128-141; also 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. 137-154.

[Lankford 1984b] D. Lankford, G. Butler, B. Brady Abelian group unification algorithms for elementary terms, Contemporary Mathematics 29, 1984.

[Lankford 1985] D.S. Lankford, New non-negative integer basis algorithms for linear equations with integer coefficients, Internal Report, Louisiana Tech. Univ., Ruston, LA, 1985.

[Lankford 1986] D. Lankford, Generalized Grobner bases: Theory and applications. Math. Dept., Louisiana Tech. Univ., Ruston, LA 71272, December 1986.

*[Lankford 1989a] D. Lankford, Generalized Grobner Bases: Theory and applications. A condensation, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 203-221.

*[Lankford 1989b] D. Lankford, Non-negative integer basis algorithms for linear equations with integer coefficients, Tech. Report, Louisiana Tech. University, Ruston, LA 71272, 1987; also J. Automated Reasoning 5(1):25-35, March 1989.

*[Lassez 1986a] J.-L. Lassez, M.J. Maher, K.G. Marriott, Unification revisited, Tech. Report RC 12395 (#55630), IBM Thomas J. Watson Research Center, Yorktown Heights, NY, December 1986; also 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. 67-113; also Foundations of Deductive Databases and Logic Programming, ed. J. Minker, Morgan Kauffman, Los Altos, CA, 1988, pp. 587-625.

[Lassez 1986b] J.-L. Lassez, K. Marriot, Explicit representation of terms defined by counter examples, Proc. FST and TCS Conf., LNCS 241, December 1986; also J. of Automated Reasoning 3(3):301-317, September 1987.

[Lassez 1988a] J.L. Lassez, M.J. Maher, On Fourier's algorithm for linear arithmetic constraints, IBM Research Report, T.J. Watson Research Center, 1988.

[Lassez 1988b] J.L. Lassez, K. McAloon, Applications of a canonical form for generalized linear constraints, Proc. of the FGCS Conf., Tokyo, December 1988, pp. 703-710.

*[Lassez 1989a] J.L. Lassez, T. Huynh, K. McAloon, Simplification and elimination of redundant linear arithmetic constraints, Logic Programming: Proc. of the North American Conf., 1989, Vol. 1, ed. E.L. Lusk, R.A. Overbeek, MIT Press, 1989, pp. 37-51.

[Lassez 1989b] J.L. Lassez, K. McAloon, Independence of negative constraints, TAPSOFT 89, Advance Seminar on Foundations of Innovative Software Development, LNCS 351, Springer-Verlag, 1989.

*[Lassez 1990] J.-L. Lassez, Parametric queries, linear constraints and variable elimination, Proc. Intl. Symp. on Design and Implementation of Symbolic Computation Systems (DISCO '90, Capri, Italy 10-12 April 1990), LNCS 429, ed. A Miola, Springer-Verlag, 1990, pp. 164-173.

*[Latch 1989] D.M. Latch, R. Sigal, A local termination property for term rewriting systems, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 222-233.

[Laudet 1970] M. Laudet, D. Lacombe, L. Nolin, M. Schutzenberger, eds. Symp. on Automatic Demonstration (Versailles, France, 1968), Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970.

[Laurent 1979] J.H. Laurent, Adding dynamic paramodulation to rewrite algorithms, Tech. Rep. CSL-102, SRI International, Menlo Park, December 1979.

[Laville 1987] A. Laville, Lazy pattern matching, Tech. Report, Univ. of Reims, Framce, 1987.

[Laville 1988a] A. Laville, Comparison of priority rules in pattern matching and term rewriting, No. 878, INRIA, July 1988.

[Laville 1988b] A. Laville, Implementation of lazy pattern matching algorithms, Proc. ESOP'88, LNCS 300, ed. H. Ganzinger, March 1988, pp. 298-316.

[Lawrence 1974] J.D. Lawrence, J.D. Starkey, Experimental tests for resolution-based theorem proving strategies, Tech. Report, Computer Science Dept., Washington State Univ., Pullman, Washington, April 1974.

[Lawrence 1976] J.D. Lawrence, J.D. Starkey, Experimental tests for resolution-based theorem proving, Inf. Sciences 10(2):131-154, 1976.

[Lazrek 1986] A. Lazrek, P. Lescanne, J.-J. Thiel, Proving inductive equalities, algorithms and implementation, Internal Report CRIN 86-R-087, Centre de Recherche en Informatique de Nancy, 1986; to be published in Information and Control.

[Le Chenadec 1984] P. Le Chenadec, Canonical forms in finitely presented algebras, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 142-165.

*[Le Chenadec 1988a] P. Le Chenadec, Normalization and linearity in unification logic, INRIA, No. 922, October 1988.

[Le Chenadec 1988b] P. Le Chenadec, On positive occur-checks in unification, Proc. MFCS, LNCS 324, Springer-Verlag, 1988, pp. 433-444.

[Lederberg 1967] J. Lederberg, E.A. Feigenbaum, Mechanization of Inductive Inference in Organic Chemistry, A.I. Memo No. 54, Stanford Univ., Palo Alto, CA, August 1967.

[Lee 1967] R.C.T. Lee, A completeness theorem and a computer program for finding theorems derivable from given axioms, PhD thesis, Univ. of California at Berkeley, CA, 1967.

[Lee 1971] R.C.T. Lee, C.L. Chang, Program analysis and theorem proving, Div. of Comput. Res. and Technol., Nat. Institute of Health, Bethesda, Maryland, 1971.

[Lee 1972] R.C.T. Lee, Fuzzy logic and the resolution principle, JACM 19(1):109-119, 1972.

[Lee 1981] S.J. Lee, S.L. Gerhart, eds., AFFIRM User's Guide, USC Information Sciences Institute, Marina Del Ray, CA, 1981.

*[Lee 1989a] S.J. Lee, D. Plaisted, Theorem proving using hyper-matching strategy, Proc. 4th Methodologies for Intelligent Systems (12-14 October 1989, Charlotte, North Carolina), ed. Z.W. Ras, Elsevier Science Publishing Co., NY, NY, 1989, pp. 467-476.

[Lee 1989b] S.J. Lee, D. Plaisted, An intelligent decision procedure for propositional logic, Dept. of Computer Science, Univ. of North Carolina at Chapel Hill, 1989.

*[Lee 1990a] S.H. Lee, L.J. Henschen, Substitution-based compilation of extended rules in deductive databases, 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. 57-71.

*[Lee 1990b] S.J. Lee, D.A. Plaisted, New applications of a fast propositional calculus decision procedure, Proc. 8th Biennial Conf. of the Canadian Society for Computational Studies of Intelligence (CSCSI-90, Univ. of Ottawa, Ottawa, Canada, 22-25 May 1990), published by CSCSI, 1990, pp. 204-211.

[Lee 1990c] S.-J. Lee, CLIN: An automated reasoning system using clause linking, PhD thesis, Univ. of North Carolina at Chapel Hill, 1990.

*[Lee 1990d] S.J. Lee, D.A. Plaisted, Eliminating duplication with the hyper-linking strategy, TR90-032, Dept. of Computer Science, Univ. of North Carolina at Chapel Hill, August 1990.

[Lehmer 1963] D.H. Lehmer, Some high-speed logic, Proc. Symp. in Appl. Maths, Amer. Maths Soc., Vol. 15, 1963.

*[Leitsch 1990] A. Leitsch and G. Gottlob, Deciding Horn clause implication problems by ordered semantic resolution, Proc. Intl. Symp. `Computational Intelligence 89' (Milan, Italy, 25-27 September 1989), In Computational Intelligence, II, ed. F. Gardin, G. Mauri, and M. Filippini, North-Holland, Amsterdam, 1990, pp. 19-26.

[Lenat 1976] D.B. Lenat, AM: An artificial intelligence approach to discovery in mathematics as heuristic search, Stanford AI Lab. Memo AIM-286, Stanford University, July 1976; also in Knowledge-based Systems in Artificial Intelligence, McGraw Hill, 1982.

[Lenat 1977a] D.B. Lenat, Automated theory formation in mathematics, Proc. 5th IJCAI, MIT, Cambridge, MA, August 1977, pp. 833-842.

[Lenat 1977b] D.B. Lenat, The ubiquity of discovery, Proc. 5th IJCAI, MIT, Cambridge, MA, August 1977, pp. 1093-1105.

[Lenat 1982] D. Lenat, AM: Discovery in mathematics as heuristic search, Knowledge-Based Systems in Artificial Intelligence, ed. Davis and Lenat, McGraw-Hill, 1982, pp. 3-149.

[Lenat 1983] D.B. Lenat, EURISKO: A program that learns new heuristics and domain concepts, the nature of heuristics III: Program desing results, Artificial Intelligence 21(1,2):61-98, 1983.

[Lenat 1986] D. Lenat, M. Prakash, M. Shepherd, CYC: Using common sense knowledge to overcome brittleness and knowledge acquisition bottlenecks, AI Magazine, VI, Winter 1986.

[Lenat 1987] D. Lenat, E.A. Feigenbaum, On the thresholds of knowledge, IJCAI-87.

[Lescanne 1981] P. Lescanne, Decomposition ordering as a tool to prove the termination of rewriting systems, Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, August 1981, pp. 548-550.

[Lescanne 1982] P. Lescanne, Some properties of decomposition orderings; A simplification ordering to prove termination of rewriting systems, RAIRO Informatique theorique, No. 4, 1982.

[Lescanne 1983] P. Lescanne, Computer experiments with the REVE term rewriting system generator, Proc. 10th ACM Symp. on Principles of Programming Languages (Austin, Texas), January 1983, pp. 99-108.

[Lescanne 1984a] P. Lescanne, Term rewriting systems and algebra, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 166-174.

[Lescanne 1984b] P. Lescanne, Uniform termination of term rewriting systems: Recursive decomposition ordering with status, Proc. 6th Colloquium on Trees in Algebra and Programming (Bordeaux, France), ed. B. Courcelle, Cambridge Univ. Press, March 1984, pp. 181-194; also as How to prove termination: An approach to the implementation of a new recursive decomposition 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. 109-121.

[Lescanne 1986] P. Lescanne, REVE: A Rewrite Rule Laboratory, 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. 695-696; also in Proc. 4th STACS (Passau, FRG), ed. F.J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, LNCS 247, Springer-Verlag, 1987, pp. 482-483.

[Lescanne 1987a] P. Lescanne, ed., Proc. 2nd Intl. Conf. on Rewriting Techniques and Applications (Bordeaux, France, 25-27 May 1987), LNCS 256, Springer-Verlag, Berlin, 1987.

[Lescanne 1987b] P. Lescanne, Current trends in rewriting techniques and related problems, Proc. Trends in Computer Algebra, Intl. Symp. (Bad Neuenahr, 19-21 May 1987), ed. R. Janssen, LNCS 296, Springer-Verlag, Berlin, pp. 38-51.

[Lescanne 1989] P. Lescanne, Completion procedures as transition rules + control, In TAPSOFT'89 (vol. 1), ed. M. Diaz and F. Orejas, LNCS 351, Springer-Verlag, 1989, pp. 28-41.

*[Lescanne 1990a] P. Lescanne, ORME: An implementation of completion procedures as sets of transitions rules (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. 661-662.

*[Lescanne 1990b] P. Lescanne, On the recursive decomposition ordering with lexicographical status and other related orderings, J. of Automated Reasoning 6(1):39-49, March 1990.

*[Lescanne 1990c] P. Lescanne, Well rewrite orderings, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 249-256.

[Leszczylowski 1980a] J. Leszczylowski, An experiment with Edinburgh LCF, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980, pp. 170-181.

[Leszczylowski 1980b] J. Leszczylowski, Theory of FP systems in Edinburgh LCF, Internal Report, CSR-61-80, Univ. of Edinburgh, Dept. of Computer Sci., Edinburgh, April 1980.

[Leszczylowski 1980c] J. Leszczylowski, On proving laws of the algebra of FP-systems in Edinburgh LCF, Proc. 1st Natl Conf. on Artificial Intelligence, Stanford Univ., August 1980, pp. 84-86.

[Letz 1988] R. Letz, J. Schumann, S. Bayerl, SETHEO - A sequential theorem prover for first-order logic, Technische Universitat Munchen, 1988.

*[Letz 1993] R. Letz, On the polynomial transparency of resolution, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 123-137.

*[Leung 1989] K.S. Leung, W. Lam, A fuzzy expert system shell using both exact and inexact reasoning, J. of Automated Reasoning 5(2):207-233, June 1989.

[Levi 1988] G. Levi, Object level reflection of ingerence rules by partial evaluation, In Metalevel architectures and reflection, ed. P. Maes and D. Nardi, North Holland Publishers, Amsterdam, 1988, pp. 313-328.

[Levine 1967] R.E. Levine, M.E. Maron, A Computer System for Inference Execution and Data Retrieval, CACM 10(11):715-721, 1967.

*[Levitt 1993] K. Levitt, T. Leung, E.T. Schubert, M. Heckman, Formal verification of a microcoded VIPER microprocessor using HOL, NASA contractor report 4489, February 1993.

[Levy 1992] B. Levy, I. Filippenko, L. Marcus, and T. Menas, Using the State Delta Verification System (SDVS) for Hardware Verification, In Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience: Nijmegen, The Netherlands, pp. 337--360, North-Holland, June 1992.
(source: Leo Marcus)

*[Levy 1993] A.Y. Levy, Y. Sagiv, Exploiting irrelevance reasoning to guide problem solving, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 138-145.

[Lewis 1975] H. Lewis, Cycles of unifiability and decidability by resolution, Tech. Report, Aiken Comp. Lab., Harvard Univ., 1975.

[Lewis 1978] H.R. Lewis, Renaming a set of clauses as a Horn set, JACM 25(1):134-135, January 1978.

[Lewis 1980] H.R. Lewis, Complexity results for classes for quantificational formulas, J. Comp. Syst. Sci. 21(1980):317-353.

[Lewis 1982] H.R. Lewis, R. Statman, Unifiability is complete for co-NLOGSPACE, Information Processing Letters 15(1982):220-222.

[Lifschitz 1986] V. Lifschitz, Mechanical theorem proving in the U.S.S.R.: The Leningrad School, Delphic Associates, Falls Church, VA, 1986.

*[Lifschitz 1987] V. Lifschitz, What is the inverse method? Memo, Stanford Univ. CS Dept. June 1987; also J. Automated Reasoning 5(1):1-23, March 1989.

[Lifsic 1968] V.A. Lifsic, Specialization of the form of deduction in the predicate calculus with equality and function symbols, Proc. Steklov Inst. Math. 98, 1968, 1-23.

*[Ligeza 1993] A. Ligeza, A note on backware dual resolution and its application to proving completeness of rule-based systems, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 132-137.

[Lim 1985a] Y. Lim, A new hyperparamodulation strategy for the equality clauses, Ph. D. dissertation at Northwestern Univ., 1985.

[Lim 1985b] Y. Lim, L.J. Henschen, A new hyperparamodulation strategy for the equality relation, Proc. 9th IJCAI, Los Angeles, CA, 1985, pp. 1138-1145.

[Lim 1986] Y. Lim, The heuristics and experimental results of a new hyperparamodulation: HL-resolution, 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. 240-253.

*[Lincoln 1988] P. Lincoln, J. Christian, Adventures in associative-commutative unification (A summary), Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310, Springer-Verlag, Berlin, 1988, pp. 358-367; also J. Symbolic Computation 8(1 and 2):217-240, 1989 (special issue on unification, part 2).

*[Lindenstrauss 1989] N. Lindenstrauss, A parallel implementation of rewriting and narrowing, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 569-573.

*[Lindsay 1987a] P.A. Lindsay, R.C. Moore, B. Ritchie, Review of existing theorem provers, Tech. Report UMCS-87-8-2, Dept. of Computer Science, Univ. of Manchester, 1987.

*[Lindsay 1987b] P.A. Lindsay, Logical frames for interactive theorem proving, Tech. Report UMCS-87-12-7, Dept. of Computer Science, Univ. of Manchester, 1987.

*[Lingenfelder 1986] C. Lingenfelder, Transformation of refutation graphs into natural deduction proofs, SEKI Report SR-86-10, Universitat Kaiserslautern, 1986.

*[Lingenfelder 1988] C. Lingenfelder, Structuring computer generated proofs, SEKI Report SR-88-19, Universitat Kaiserslautern, 1988; also in Proc. 11th IJCAI, ed. N.S. Sridharan, Morgan Kaufmann, 1989, pp. 378-383.

*[Lingenfelder 1989] C. Lingenfelder, Structuring computer generated proofs, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 378-383.

[Lingenfelder 1990] C. Lingenfelder, Transformation and structuring of computer generated proofs, PhD thesis, Univ. of Kaiserslautern, 1990.

*[Lingenfelder 1991] C. Lingenfelder, A. Pracklein, Proof transformation with built-in equality predicate, Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1 (IJCAI-91, Darling Harbour, Sydney, Australia, 24-30 August 1991), Morgan Kaufmann Publ., Inc., 1991, pp. 165-170.

[Lins 1986] R.D. Lins, A new formula for the execution of categorical combinators, 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. 89-98.

[Litvintchouk 1977] S.D. Litvintchouk, V.R. Pratt, A proof-checker for dynamic logic, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 552-558.

[Liu 1985] X.H. Liu, H. Xiao, Operator fuzzy logic and fuzzy resolution, Proc. 15th ISMVL, Canada, 5(1986):68-75.

[Liu 1986a] X.H. Liu, Generalized resolution using paramodulation, Kexue Tongbao (English edition) 31(21):1441-1444, 1986.

[Liu 1986b] X.H. Liu, K.Y. Fang, Fuzzy reasoning on lambda-horn set, Proc. 16th ISMCL, USA, 5(1986):248-251.

[Liu 1986c] X.H. Liu, C.K. Chang, J.J.-P. Tsai, Fuzzy reasoning base on lambda-LH-resolution, Proc. IEEE 10th Intern. Computer Software Application Conf., USA, 10(1986):154-157.

*[Liu 1987] P. Liu, R.-J. Chang, A new structural induction scheme for proving properties of mutually recursive concepts, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, pp. 144-148.

*[Liu 1990] P. Lui, A theoretical analysis of recurrence goals, Proc. 9th ECAI (Stockholm, Sweden, 6-10 August 1990), ed. L.C. Aiello, Pitman Publishing, London, 1990, pp. 413-418.

[Livesey 1975] M. Livesey, J. Siekmann, Termination and decidability results for string-unification, Univ. of Essex, Memo CSM-12, August 1975.

[Livesey 1976a] M. Livesey, J. Siekmann, Unification of A+C terms (bags) and A+C+I terms (sets), Interner Bericht Nr. 5/76, Inst. fur Informatik, Univ. Karlsruhe, 1976.

[Livesey 1976b] M. Livesey, J.H. Siekmann, Unification of sets and multisets, SEKI Report, Univ. of Karlsruhe, 1976.

[Livesey 1976c] M. Livesey, J. Siekmann, Unification of bags and sets, Interner 3/76, Inst. fur Informatik, Univ. Karlsruhe, 1976.

[Livesey 1977] M. Livesey, J. Siekmann, Unification of sets, Internal Report 3/76, Institut fur Informatik I, Univ. Karlsruhe, 1977.

[Livesey 1979] M. Livesey, J. Siekmann, P. Szabo, Unification problems for combinations of associativity, commutativity, distributivity and idempotence axioms, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 175-184.

[Llopis 1983] R. Llopis de Trias, Canonical forms for residue classes of polynomial ideals and term rewriting systems, Dept. U. Simon Bolivar, Caracas, Venezuela, rep. 84-03, 1983.

*[Llopis 1985] R. Llopis de Trias, An overview of completion algorithms, 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. 424-428.

[Lloyd 1984] J.W. Lloyd, Foundations of logic programming, Symbolic Computation, Springer-Verlag, Heidelberg, 1984; Second edition 1987.

[Loganantharaj 1985a] R. Loganantharaj, R.A. Muller, R.R. Oldehoeft, Connection graph refutation: aspects of AND-parallelism, Tech. Report CS-85-10, Dept. of Computer Science, Colorado State Univ., 1985.

[Loganantharaj 1985b] R. Loganantharaj, R.A. Muller, R.R. Oldehoeft, Some theoretical and implementational aspects of Dcdp-parallelism in connection graph refutation, Tech. Report CS-85-9, Dept. of Computer Science, Colorado State Univ., 1985.

[Loganantharaj 1986a] R. Loganantharaj, Theoretical and implementational aspects of parallel link resolution in connection graphs, PhD thesis, Dept. of Computer Science, Colorado State Univ., 1985.

[Loganantharaj 1986b] R. Loganantharaj, R.A. Muller, Parallel theorem proving with connection graphs, 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. 337-352.

[Longo 1974] G. Longo, M.V. Zilli, Complexity of theorem proving procedures: Some general properties, Rev. Fr. Autom. Inf. Rech. Oper. 8(December 1974):5-18, France.

[Loos 1981] R. Loos, Term reduction systems and algebraic algorithms, Proc. GWAI-81, Informatik-Fachberichte 47, ed. Siekmann, Springer-Verlag, Berlin, 1981, pp. 214-234.

[Loveland 1968] D.W. Loveland, Mechanical theorem proving by model elimination, JACM 15(2):236-251, April 1968; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 117-134.

[Loveland 1969a] D.W. Loveland, A simplified format for the model elimination theorem-proving procedure, JACM 16(3):349-363, July 1969; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 233-248.

[Loveland 1969b] D. Loveland, Theorem-provers combining model elimination and resolution, Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 73-86; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 249-263.

[Loveland 1970a] D.W. Loveland, Some linear Herbrand proof procedures: An analysis, Dept. of Comput. Sci., Carnegie-Mellon Univ., Pittsburgh, Pennsylvania, 1970.

[Loveland 1970b] D.W. Loveland, A linear format for resolution, Proc. IRIA Symp. in Automatic Demonstration (Versailles, France, 1968), Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 147-162; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 399-416.

[Loveland 1972] D. Loveland, A unifying view of some linear Herbrand procedures, JACM 19(2):366-384, April 1972.

[Loveland 1973] D.W. Loveland, M.E. Sickel, A hole in goal trees: Some guidance from resolution theory, Proc. 3rd IJCAI, Stanford Univ., Stanford, August 1973, pp. 153-161; also IEEE Transactions on Computer C-25(4):335-341, April 1976.

[Loveland 1978] D.W. Loveland, Automatic Theorem Proving: A Logical Basis, North-Holland, Amsterdam.

[Loveland 1980] D.W. Loveland, R.E. Shostak, Simplifying interpreted formulas, Tech. Report CSL-117, SRI, Project 8752, 1980; also in Proc. 5th Conf. on Automated Deduction (Les Arcs, France), ed. W. Bibel and R. Kowalski, Springer-Verlag, LNCS 87, 1980, pp. 97-109.

[Loveland 1981] D.W. Loveland, C.R. Reddy, Deleting repeated goals in the problem reduction format, JACM 28(4):646-661, October 1981.

[Loveland 1982] D. Loveland, ed., Proc. 6th Conf. on Automated Deduction, LNCS 138, Springer-Verlag, Berlin, 1982.

[Loveland 1984] D.W. Loveland, Automated theorem-proving: A quarter-century review, 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. 1-45.

*[Loveland 1986] D.W. Loveland, Automated theorem proving: Mapping logic into AI, Proc. of the ACM SIGART Intl. Symp. on Methodologies for Intelligent Systems, ed. Z.W. Ras and M. Zemankova, Knoxville, TN, 22-24 October 1986, pp. 214-229.

[Loveland 1987] D.W. Loveland, Near-Horn Prolog, CS-1987-14, Duke Univ., April 1987; also in Logic Programming: Proceedings of the Fourth Intl Conf., ed. Lassez, The MIT Press, 1987.

*[Loveland 1991] D.W. Loveland, Near-Horn Prolog and beyond, J. Automated Reasoning 7(1):1-26, March 1991.

*[Lownie 1989] T. M. Lownie, Extending reflective architectures, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 446-451.

[Lu 1988] J.J. Lu and V.S. Subrahmanian, Completeness issues in RUE-NRF deduction, Logic Programming LPRG-TR-88-24, Technical Report, Syracuse Univ., 1988.

*[Lu 1990] J.J. Lu, V.S. Subrahmanian, Protected completions of first-order general logic programs, J. of Automated Reasoning 6(2):147-172, June 1990.

[Lucchesi 1972] C.L. Lucchesi, The undecidability of the unification for third order language, CSRR 2059, Dept. of Appl. Analysis and Comput. Sci., Univ. of Waterloo, Waterloo, Canada, 1972.

[Luckham 1967] D. Luckham, The resolution principle in theorem-proving, Machine Intelligence 1, ed. Collins and Michie, American Elsevier, NY, 1967, pp. 47-61.

[Luckham 1968a] D. Luckham, The ancestry filter method in automatic demonstration, Stanford Artificial Intelligence Project Memo, Stanford, 1968.

[Luckham 1968b] D. Luckham, Some tree-paring strategies for theorem-proving, Machine Intelligence 3, ed. Dale and Michie, Oliver and Boyd, Edinburgh, 1968, pp. 95-112.

[Luckham 1970] D. Luckham, Refinement theorems in resolution theory, Proc. IRIA Symp. on Automatic Demonstration (Versailles, France), Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970, pp. 163-190; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 435-465.

[Luckham 1971] D. Luckham, N.J. Nilsson, Extracting information from resolution proof trees, Artificial Intelligence 2(1):27-54, 1971.

[Luckham 1979] D.C. Luckham, et al., Stanford Pascal verifier user manual, Report STAN-CS-79-731, Dept. of Computer Science, Stanford Univ., March 1979.

[Lugiez 1988] D. Lugiez, Disunification and logic programming, Research Report Lifia 74, Univ. Grenoble, 1988.

*[Lugiez 1989] D. Lugiez, A deduction procedure for first order programs, Logic Programming: Proc. 6th Intern. Conf., ed. G. Levi and M. Martelli, The MIT Press, Cambridge, MA, 1989, pp. 585-599.

[Lusk 1977] E. Lusk, R. Overbeek, Experiments with resolution-based theorem-proving algorithms, 3rd Workshop on Automated Deduction, Boston, 1977.

[Lusk 1980] E. Lusk, R. Overbeek, Data structures and control architecture for the implementation of theorem-proving programs, Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 8-11 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87, Springer-Verlag, Berlin, 1980.

[Lusk 1982a] E. Lusk, W. McCune, R. Overbeek, Logic machine architecture: Kernel functions, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 70-84.

[Lusk 1982b] E. Lusk, W. McCune, R. Overbeek, Logic machine architecture: Inference mechanisms, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 85-108.

[Lusk 1982c] E.L. Lusk, R.A. Overbeek, Logic machine architecture inference mechanisms - layer 2 user reference manual, ANL-82-84, Math. and Comput. Sci. Div., Argonne National Lab., Argonne, Illinois, 1982 (release 2.0, 1984).

[Lusk 1982d] E.L. Lusk, R.A. Overbeek, An LMA-based theorem prover, ANL-82-75, Math. and Comput. Sci. Div., Argonne National Lab., Argonne, Illinois, 1982.

[Lusk 1982e] E. Lusk, R. Overbeek, Experiments with resolution-based theorem-proving algorithms, Computers and Mathematics with Applications 8(1982):141-152.

[Lusk 1984a] E.L. Lusk, R.A. Overbeek, A portable environment of research in automated reasoning, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 43-52.

[Lusk 1984b] E.L. Lusk, R.A. Overbeek, The automated reasoning system ITP, ANL-84-27, Argonne National Lab., April 1984.

[Lusk 1984c] E.L. Lusk, R.A. Overbeek, Logic machine architecture inference mechanisms - layer 2 user reference manual release 2.0, Technical report ANL-82-84, Rev. 1, Argonne National Laboratory, April 1984.

[Lusk 1985a] E.L. Lusk, R.A. Overbeek, Non-Horn problems, J. of Automated Reasoning 1(1):103-114, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Lusk 1985b] E.L. Lusk, R.A. Overbeek, Reasoning about equality, J. of Automated Reasoning 1(2):209-220, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Lusk 1986] E. Lusk, W. McCune, R. Overbeek, ITP at Argonne National Laboratory, 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. 697-698.

*[Lusk 1988] E. Lusk, R. Overbeek, eds., Proc. 9th Intl. Conf. on Automated Deduction (CADE-9, Argonne, Illinois, 23-26 May 1988), LNCS 310, Springer-Verlag, Berlin, 1988.

*[Lusk 1990] E. Lusk, W. McCune, High-performance automated theorem proving (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. 681.

[Lusk 1991] E.L. Lusk, W.W. McCune, J.K. Slaney, ROO - a parallel theorem prover, Informal Proc. of the Internat. Workshop on Parallel Processing for AI in Conjunction with IJCAI-91, ed. L.N. Kanal and C.B. Suttner, Sydney, Australia, 1991, pp. 110-116.

*[Lusk 1992a] E.L. Lusk, W.W. McCune, J. Slaney, ROO: A parallel theorem prover, 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. 731-734.

*[Lusk 1992b] E.L. Lusk, L. Wos, Benchmark problems in which equality plays the major role, 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. 781-785.


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