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:56, 1986.
*[Kalkbrener 1987] M. Kalkbrener, Solving systems of algebraic
equations by using Grobner bases, Proc. European Conf. on Computer
Algebra (EUROCAL '87, Leipzig, GDR, 25 June 1987), ed. J.H.
Davenport, LNCS 378, SpringerVerlag, Berlin, 1989, pp. 282292.
[Kallick 1965a] B. Kallick, Automatic TP and game playing: A
dispassionate view, TIT Res. Inst., Chicago, Ill., January 1965.
[Kallick 1965b] B. Kallick, TheoremProving by Computer, TIT
Res. Inst., Chicago, Ill., January 1965.
[Kallick 1966] B. Kallick, Theoremproving 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. 269275.
[Kalman 1983] J.A. Kalman, J.G. Peterson, Computeraided studies
of all possible shortest single axioms for the equivalential
calculus, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp.
933935.
[Kamin 1980a] S. Kamin, J.J. Levy, Attempts for generalising the
recursive path orderings, Unpublished manuscript, Dept. of
Computer Science, Univ. Illinois, UrbanaChampaign, February 1980.
[Kamin 1980b] S. Kamin, J.J. Levy, Two generalizations of the
recursive path ordering, Unpublished manuscript, U. of Illinois at
UrbanaChamgaign, 1980.
[Kanamori 1986] T. Kanamori, H. Fujita, Formulation of induction
formulas in verification of PROLOG 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. 281299.
[KandriRody 1983] A. KandriRody, D. Kapur, On relationship
between Buchberger's Grobner basis algorithm and the KnuthBendix
completion procedure, TIS Report No. 83CRD286, General Electric
Research and Development Center, Schenectady, NY, 1983.
[KandriRodi 1984] A. KandriRodi, D. Kapur, Algorithms for
computing the Grobner bases of polynomial ideals over various
Euclidean rings, Proc. EUROSAM 84 (Cambridge, England, July 911,
1984), ed. Fitch, LNCS 174, SpringerVerlag, 1984, pp. 195208.
[KandriRodi 1985] A. KandriRodi, 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, 2022 May
1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin,
1985. pp. 345364.
*[KandriRody 1988] A. KandriRody, D. Kapur, Computing a
Grobner basis of a polynomial ideal over a Euclidean domain, J. of
Symbolic Computation 6(1):3757, August 1988.
*[KandriRody 1988] A. KandriRody, V. Weispfenning,
Noncommutative Grobner Bases in algebras of solvable type,
MIP8807, Fakultat fur Mathematik und Informatik, Universitat
Passau, March 1988.
[KandriRody 1989] A. KandriRody, D. Mapur, F. Winkler,
KnuthBendix procedure and Buchberger algorithmA synthesis,
Tech. Report 8918, 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):427444, 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, NorthHolland Publ., Amsterdam,
1963, pp. 8794; also Automation of Reasoning  Classical Papers
on Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 364371.
[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):718, USSR,
September 1972.
*[Kaplan 1983] S. Kaplan, Conditional rewrite rules, Report no.
150, CNRS, France, December 1983; also Theoretical Computer
Science 33(1984):175193;
*[Kaplan 1984] S. Kaplan, Fair conditional term rewriting
systems: Unification, termination and confluence, Tech. Report
194, Laboratoire de Recherche en Informatique, Universite de
ParisSud, Orsay, France, November 1984; also Proc. 3rd Workshop
on Theory and Applications of Abstract Data Types (Selected
Papers)  Recent Trends in Data Type Specifications,
InformatikFachberichte 116, ed. H.J. Kreowski, SpringerVerlag,
Berlin, 1985, pp. 136155.
*[Kaplan 1986a] S. Kaplan, Rewriting with a nondeterministic
choice operator: From algebra to proofs, Proc. ESOP 86, 1st
European Symp. on Programming (Saarbrucken, FRG, 1719 March
1986), ed. B. Robinet and R. Wilhelm, LNCS 213, SpringerVerlag,
Berlin, 1986, pp. 351374; also Theor. Comput. Sci 56(1):3757,
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, 2527 May 1987), ed. P. Lescanne, LNCS 256,
SpringerVerlag, Berlin, 1987, pp. 2541.
*[Kaplan 1987b] S. Kaplan, Simplifying conditional term
rewriting systems: Unification, termination and confluence, J. of
Symbolic Computation 4(3):295334, Academic Press Limited,
December 1987.
*[Kaplan 1988a] S. Kaplan, J.P. Jouannaud, eds., Proc. 1st
Intl. Workshop on Conditional Term Rewriting Systems (Orsay,
France, 810 July 1987), LNCS 308, SpringerVerlag, Berlin, 1988.
*[Kaplan 1988b] S. Kaplan, Positive/negative conditional
rewriting, Proc. 1st Intl. Workshop on Conditional Term Rewriting
Systems (Orsay, France, 810 July 1987), ed. S. Kaplan and J.P.
Jouannaud, LNCS 308, SpringerVerlag, Berlin, 1988, pp. 129143.
*[Kaplan 1989a] S. Kaplan, C. Choppy, Abstract rewriting with
concrete operators, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 178186.
*[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.
AitKaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp.
141170.
[Kapur 1980] D. Kapur, Krishnamurthy, P. Narendran, A linear
algorithm for unification, General Electric Rep. 82CRD100, NY,
1980.
[Kapur 1983] D. Kapur, P. Narendran, The KnuthBendix completion
procedure and Thuesystems, Record of the 3rd Conf. on Foundations
of Software Technology and Theoretical Computer Science
(Bangalore, India, 1214 December 1983), pp. 363385; also SIAM J.
of Computations 14(4):10521070, 1985.
[Kapur 1984a] D. Kapur, B. Krishnamurthy, A natural proof system
based on rewriting techniques, Proc. 7th Intl. Conf. on Automated
Deduction (CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS
170, SpringerVerlag, NY, 1984, pp. 5364.
[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. 3356.
[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. 245267; also GE report 84GEN008, April
1984; also Artificial Intelligence 31(2):125157, 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.
337348.
[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, SpringerVerlag, Berlin, 1985, pp. 173187;
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, SpringerVerlag, Berlin,
1985, pp. 188207.
[Kapur 1985c] D. Kapur, P. Narendran, An equational approach to
theorem proving in firstorder predicate calculus, Rep. 84CRD322,
General Electric Corporate Research and Development, Schenectady,
NY, September 1985; also Proc. 7th IJCAI, Los Angeles, August
1985, pp. 11461153.
[Kapur 1985d] D. Kapur, M. Krishnamoorthy, R. McNaughton, P.
Narendran, An O(T3) algorithm for testing the ChurchRosser
property of Thue systems, Theoret. Comput. Sci. 35(1):109114,
1985.
*[Kapur 1985e] D. Kapur, M. Krishnamoorthy, R. McNaughton, P.
Narendran, The ChurchRosser property and special Thue systems,
Theoretical Computer Science 39(23):123133, 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):337344.
[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):395415, 1987.
[Kapur 1986a] D. Kapur, D.R. Musser, Inductive reasoning with
incomplete specifications, Proc. IEEE Symp. on Logic in Computer
Science, Cambridge, MA, 1618 June 1986, pp. 367377.
[Kapur 1986b] D. Kapur, P. Narendran, H. Zhang, Proof by
induction using test sets, Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp.
99117.
*[Kapur 1986c] D. Kapur, P. Narendran, NPcompleteness of the
set unification and matching 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. 489495.
[Kapur 1986d] D. Kapur, G. Sivakumar, H. Zhang, RRL: A Rewrite
Rule Laboratory, Proc. 8th Intl. Conf. on Automated Deduction
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 691692.
[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 8903, Dept. of Computer
Science, Univ. of Iowa, May 1989.
*[Kapur 1986f] D. Kapur, Geometry theorem proving using
Hilbert's Nullstellensatz, Proc. 1986 ACMSIGSAM Symp. on Symbolic
and Algebraic Computation (SYMSAC '86, Univ. of Waterloo,
Waterloo, Ontario, 2123 July 1986), ed. B.W. Char, ACM, New York,
NY, 1986, pp. 202208. [Kapur 1986g] D. Kapur, Using Grobner bases
to reason about geometry problems, J. of Symbolic Computation
2(4):399408, December 1986.
[Kapur 1986h] D. Kapur, P. Narendran, NPCompleteness of
associativecommutative unification check and related problems,
General Electric Company, Schenectady, NY, 1987.
[Kapur 1986i] D. Kapur, P. Narendran, F. Otto, On
groundconfluence of term rewriting systems, Tech. Report 876,
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 30July 3, 1986, In: Artificial
Intelligence 37(13):1536, 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(13):6193, December 1988.
*[Kapur 1987a] D. Kapur, P. Narendran, Matching, unification and
complexity, SIGSAM Bulletin 21(4):69, November 1987.
[Kapur 1987b] D. Kapur, P. Narendran, D.J. Rosenkrantz, H.
Zhang, Sufficientcompleteness, quaisreducibility 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 (CADE9,
Argonne, Illinois, 2326 May 1988), ed. E. Lusk and R. Overbeek,
LNCS 310, SpringerVerlag, Berlin, 1988, pp. 768769.
*[Kapur 1988b] D. Kapur, D.R. Musser, P. Narendran, Only prime
superpositions need be considered in the KnuthBendix 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):1936, August 1988.
*[Kapur 1988c] D. Kapur, H. Zhang, Proving equivalence of
different axiomatizations of free groups, J. Automated Reasoning
4(3):331352, 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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 559563.
[Kapur 1989b] D. Kapur, H. Zhang, Rewrite rule laboratory user's
manual, Tech. Report 8903, 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):1431,
1989.
*[Kapur 1990] D. Kapur, H.K. Wan, Refutational proofs of
geometry theorems via characteristic set computation, Proc. ISSAC
'90 (Tokyo, Japan, 2024 August 1990), ACM, NY, NY, 1990, pp.
277284.
*[Kapur 1992] D. Kapur, ed. Proc. 11th Intl. Conf. on Automated
Deduction (CADE11, Saratoga Springs, NY, USA, June 1992), Lecture
Notes in Artificial Intelligence 607, SpringerVerlag, 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.
2232.
[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, SpringerVerlag, Berlin, 1985, pp. 208222.
[Kaufl 1985] Th. Kaufl, The simplifier of the program verifier "Tatzelwurm",
Proc. Osterreichische Artificial IntelligenceTagung, Wien (2427
September 1985), InformatikFachberichte 106, SpringerVerlag,
Berlin, 1985, pp. 185193.
[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 (CADE8,
Oxford, England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS
230, SpringerVerlag, Berlin, 1986, pp. 300305.
*[Kaufl 1988a] T. Kaufl, Reasoning about systems of linear
inequalities, 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. 563572.
[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
tableaubased 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 (CADE10, Kaiserslautern, FRG, July 1990),
Lecture Notes in Artificial Intelligence 449, ed. M.E. Stickel,
SpringerVerlag, Berlin, 1990, pp. 657658.
[Kaufmann 1987] M. Kaufmann, A user's manual for an interactive
enhancement to the BoyerMoore 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
BoyerMoore Theorem Prover, Proc. 9th Intl. Conf. on Automated
Deduction (CADE9, Argonne, Illinois, 2326 May 1988), ed. E. Lusk
and R. Overbeek, LNCS 310, SpringerVerlag, Berlin, 1988, pp.
735736.
[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 BoyerMoore Theorem Prover, Tech.
Report 42, Computational Logic, Inc., Austin, Texas, May 1989.
[Kaufmann 1989c] M. Kaufmann, DEFNSK: An extension of the
BoyerMoore theorem prover to handle firstorder 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
(CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes in
Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 659660.
*[Kaufmann 1990b] M. Kaufmann, Generalization in the presence of
free variables: a mechanicallychecked correctness proof for one
algorithm, Tech. Report 53, Computational Logic, Inc., Austin,
Texas, 1990; also J. Automated Reasoning 7(1):109158, 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):88108,
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 SR8912, Universitat Kaiserslautern, 1989.
*[Kerber 1990] M. Kerber, How to prove higher order theorems in
first order logic, SEKI Report 9019, Fachbereich Informatik,
Universitat Kaiserslautern, Kaiserslautern, Germany, 1990; also
Proc. 12th Intl. Conf. on Artificial Intelligence, Vol 1
(IJCAI91, Darling Harbour, Sydney, Australia, 2430 August 1991),
Morgan Kaufmann Publ., Inc., 1991, pp. 137142.
[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
ordersorted rewriting systems with constructors, 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. 603617.
[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
STANCS83992, 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
(CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170,
SpringerVerlag, NY, 1984, pp. 6579.
[Ketonen 1984b] J. Ketonen, R. Weyhrauch, A decidable fragment
of predicate calculus, Theoretical Computer Science
32(1984):297307.
[Ketonen 1986] J. Ketonen, G. Bellin, Experiments in Automatic
Theorem Proving, STANCS871155, 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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
564568.
*[Kim 1989] M.Y. Kim, Visual reasoning in geometry theorem
proving, Proc. 11th IJCAI (Detroit, Michigan, USA, 2025 August
1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 16171622.
[King 1969] J.C. King, A program verifier, PhD thesis,
CarnegieMellon Univ., 1969.
[King 1970] J.C. King, R.W. Floyd, An interpretationoriented
theorem prover over the integers, Proc. 2nd ACM Symp. on Comput.
Theory, 1970, pp. 169179; also J. of Computer and System Sciences
6(1972):305323.
[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 MartelliMontanari'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. 77100; also Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 224247.
[Kirchner 1984b] H. Kirchner, A general inductive completion
algorithm and application to abstract data types, Proc. 7th Intl.
Conf. on Automated Deduction (CADE7, Napa, CA, May 1984), ed.
R.E. Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 282302.
*[Kirchner 1984c] C. Kirchner, H. Kirchner, Implementation of a
general completion procedure parameterized by builtin theories
and strategies (demonstration), Rapport Crin 84R85, 1984; also
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. 402404.
[Kirchner 1984d] C. Kirchner, Standardizations of equational
unification: Abstract and examples, Internal Report 84R074,
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,
1618 June 1986), IEEE Computer Society, 1986, pp. 206216.
[Kirchner 1987a] C. Kirchner, Methods and tools for equational
unification, CNRS technical report Nr. 87R008, Univ. of Nancy I,
1987.
[Kirchner 1987b] C. Kirchner, P. Lescanne, Solving disequations,
Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca, NY,
2225 June 1987, pp. 347352.
[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, 2527 May 1987), ed. P. Lescanne,
LNCS 256, SpringerVerlag, Berlin, 1987, pp. 180191.
[Kirchner 1987d] C. Kirchner, H. Kirchner, REVEUR3:
Implementation of a general completion procedure parameterized by
builtin theories and strategies, J. Sci. Comput. Programming,
8(1):6986, 1987.
[Kirchner 1987e] C. Kirchner, ed. Proc. on a workshop on
unification, Centre de Recherche en Informatique de Nancy, BP 239,
54506 VandoeuverlesNancy, 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):303332, October 1989.
*[Kirchner 1989c] C. Kirchner, From unification in combination
of equational theories to a new ACunification algorithm, In:
Resolution of Equations in Algebraic Structures: Vol 2, Rewriting
Techniques, ed. H. AitKaci, M. Nivat, Academic Press, Inc., San
Diego, 1989, pp. 171210.
[Kirchner 1989d] C. Kirchner, H. Kirchner, Constrained
equational reasoning, Report CRIN 89R220, 1989; also Proc.
ACMSIGSAM 1989 Intl. Symp. on Symbolic and Algebraic Computation
(Portland, Oregon), ACM Press, pp. 382389.
*[Kirchner 1990a] C. Kirchner, Equational unification (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. 682.
*[Kirchner 1990b] C. Kirchner, F. Klay, Syntactic theories and
unification, Proc. 5th Annual IEEE Symp. on Logic Computer Science
(Philadelphia, PA, 47 June 1990), IEEE Computer Society Press,
Los Alamitos, CA, 1990, pp. 270277.
[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 (CADE4, Austin, Texas, 13
February 1979), ed. W.H. Joyner, 1979, pp. 115121.
[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):783.
[Kleer 1984b] J. De Kleer, Choices without backtracking,
AAAI84, 1984, pp. 7985.
[Kleine Buning 1985a] H. Kleine Buning, Complexity results for
classes of firstorder formulas with identity and conjunctive
quantificational form, Forschungsberichte der Universitat
Karlsruhe, 1985.
[Kleine Buning 1985b] H. Kleine Buning, T. Lettmann, Firstorder
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 (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 553563.
*[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. 97116.
[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, 13 September 1971, pp.
568585; also Artificial Intelligence 2(1971):147178.
[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:195200, NorthHolland, 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. 143182.
[Klop 1987b] J.W. Klop, A. Middeldorp, Strongly sequential term
rewriting systems, Report CSR8730, Centre for Mathematics and
Computer Science, Amsterdam, 1987.
[Klop 1990a] J.W. Klop, Term rewriting systems: From
ChurchRosser to KnuthBendix and beyond, Proc. 17th Intl.
Colloquium on Automata, Languages and Programming, LNCS 443,
SpringerVerlag, Berlin, pp. 350369.
[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 TR86742, 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. 237248.
[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. 263297;
also Automation Of Reasoning  Classical Papers On Computational
Logic, Vol. II, 19671970, ed. J. Siekmann And G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 342376.
[Knuth 1974] M. Knuth, Pratt, Fast Pattern Matching in Strings,
StanCS74440, Stanford Univ., Comp. Sci. Dept., 1974.
[Ko 1985a] H.P. Ko, M.A. Hussain, ALGEProver: 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):225242.
*[Ko 1986a] H.P. Ko, Geometry theorem proving by decomposition
of quasialgebraic sets: An application of the RittWu principle,
Proc. Workshop on Geometric Reasoning, Oxford Univ., June 30 
July 3, 1986, In: Artificial Intelligence 37(13):95122, December
1988.
[Ko 1986b] H.P. Ko, ALGEprover II: A new edition of
ALGEprover, 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):709724, 1989.
*[Kobayashi 1986] H. Kobayashi, A. Furukawa, T. Sasaki, Grobner
bases of ideals of convergent power series, Proc. 1986 ACMSIGSAM
Symp. on Symbolic and Algebraic Computation (SYMSAC '86, Univ. of
Waterloo, Waterloo, Ontario, 2123 July 1986), ed. B.W. Char, ACM,
New York, NY, 1986, pp. 225227.
[Kodratoff 1983] Y. Kodratoff, J. Castaing, Trivializing the
proof of trivial theorems, Proc. 8th IJCAI, Karlsruhe, W. Germany,
August 1983, pp. 930932.
*[Kolyada nd] S.V. Kolyada Systems for symbolic computations in
boolean algebra, Glushkov Institute fo Cybernetics, nd (after
1989).
[Konolige 1982] K. Konolige, A firstorder formalism of
knowledge and action for a multiagent planning system, Machine
Intelligence 9, ed. Hayes, Michie and Pao, Ellis Harwood Ltd.,
Chichester, 1982, pp. 4172.
[Konolige 1986a] K. Konolige, Resolution and quantified
epistemic logics, Proc. 8th Intl. Conf. on Automated Deduction
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 199208.
[Konolige 1986b] K. Konolige, A Deduction Model of Belief,
MorganKaufmann 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. 309324.
*[Korf 1985a] R.E. Korf, Depthfirst iterativedeepening: an
optimal admissible tree search, Artificial Intelligence
27(1):97109, September 1985.
*[Korf 1985b] R.E. Korf, IterativeDeepeningA: An optimal
admissible tree search, Proc. 9th Intl. Joint Conf. on Artificial
Intelligence, Vol. 2 (IJCAI85, 1823 August 1985), pp. 10341036.
[Korf 1986] R.E. Korf, Learning to solve problems by searching
for macrooperators, Research Notes in Artificial Intelligence 5,
Pitman Publ. Ltd., London, 1985.
*[Korf 1992] R.E. Korf, Linearspace bestfirst search: summary
of results, Proc. 10th National Conf. on Artificial Intelligence
(AAAI92, 1216 July 1992), AAAI Press, Menlo Park, CA, 1992, pp.
533538.
[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 (85R05), 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, 810 July 1987), ed. S. Kaplan
and J.P. Jouannaud, LNCS 308, SpringerVerlag, Berlin, 1988, pp.
144160; 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. 527537.
*[Kounalis 1990] E. Kounalis, M. Rusinowitch, Mechanizing
inductive reasoning, Proc. 8th National Conf. on Artificial
Intelligence (AAAI90, July 29August 3, 1990), AAAI Press/MIT
Press, 1990, pp. 240245; also Bull. EATCS 41(1990):216226.
[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 theoremproving, Machine Intelligence 4, ed. B. Meltzer
and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 87101;
also Automation Of Reasoning  Classical Papers On Computational
Logic, Vol. II, 19671970, ed. J. Siekmann And G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 217232.
[Kowalski 1970a] R. Kowalski, Studies in the completeness and
efficiency of theoremproving by resolution, PhD, Univ. of
Edinburgh, Edinburgh, Scotland, 1970.
[Kowalski 1970b] R. Kowalski, Search strategies for
theoremproving, Machine Intelligence 5, ed. B. Meltzer and D.
Michie, Edinburgh Univ. Press, Edinburgh, 1970, pp. 181201.
[Kowalski 1970c] R. Kowalski, The case for using equality axioms
in automatic demonstration, Symp. on Automatic Demonstration,
Lecture Notes in Math. 125, SpringerVerlag, Berlin, 1970, pp.
112127; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 377398.
[Kowalski 1971a] R. Kowalski, D. Kuhner, Linear resolution with
selection function, Artificial Intelligence 2(34):227260, Winter
1971; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 542577.
[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, Andor graphs, theorem proving
graphs and bidirectional search, Machine Intelligence 7, ed. B.
Meltzer and D. Michie, Edinburgh Univ. Press, 1972, pp. 167194.
[Kowalski 1974] R. Kowalski, Predicate logic as a programming
language, Information Processing 74, NY: Elsevier NorthHolland,
1974, pp. 569574.
[Kowalski 1975] R. Kowalski, A proof procedure using connection
graphs, JACM 22(4):572595, October 1975.
[Kowalski 1979] R.A. Kowalski, Logic for Problem Solving,
Elsevier NorthHolland Inc., NY, 1979.
[Kozen 1981] D. Kozen, Positive firstorder logic is
NPcomplete, IBM J. Res. Dev. 25(4):327332, 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 81458, 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
SWP8904, Universitat Kaiserslautern, 1989.
[Kramosil 1975] I. Kramosil, A note on deductive rules with
negative premises, Proc. 4th IJCAI, Tbilisi, Georgia, USSR, 1975,
pp. 5356.
[Kreisel 1970] G. Kreisel Hilbert's program and the search for
automatic proof procedures, In Symp. on Automatic Demonstration,
Lecture Notes in Mathematics 125, SpringerVerlag, NY, 1970, pp.
128146.
[Kreisel 1981] G. Kreisel Neglected possibilities of processing
assertions and proofs mechanically: Choice of problems and data,
in U.Level ComputerAssisted Instruction at Stanford; 19681980,
ed. Patrick Suppes, IMSSS, Stanford, 1981.
[Kreitz 1986] C. Kreitz, Constructive automata theory
implemented with the Nuprl Proof Development Systems, Report
86779, 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. 2837.
*[Krishnamurthy 1985] B. Krishnamurthy, Short proofs for tricky
formulas, Acta Informatica 22(3):253275, 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.
8798.
[Kuchlin 1982a] W. Kuchlin, Some reduction strategies for
algebraic term rewriting, SIGSAM Bulletin 16(4):1323, Issue 64,
November 1982.
[Kuchlin 1982b] W. Kuchlin, A theoremproving approach to the
KnuthBendix completion algorithm, In Computer Algebra, Proc.
EUROSAM 1982 (April 1982), ed. J. Calmet, LNCS 144,
SpringerVerlag, pp. 101108; also J. of Computer and System
Science 23(1), 1981.
[Kuchlin 1982c] W. Kuchlin, An implementation and investigation
of the KnuthBendix 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,
13 April 1985), Vol. 2: Research Contributions, ed. B.F.
Caviness, LNCS 204, SpringerVerlag, Berlin, pp. 390399.
[Kuchlin 1986a] W. Kuchlin, Equational completion by proof
simplification, Tech. Report 8602, 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), CH8092, Zurich, Switzerland, June
1986.
[Kuchlin 1986c] W. Kuchlin, A generalized KnuthBendix
algorithm, Tech. Report 8601, Dept. of Mathematics, Swiss Federal
Institute of Technology (ETH), Zurich, Switzerland, 1986.
*[Kuchlin 1987] W. Kuchlin, Inductive completion by ground proof
transformation, Tech. Report 8708, 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. AitKaci and M. Nivat, Academic
Press, Inc., San Diego, 1989, pp. 211244.
*[Kuhn 1990] N. Kuhn, K. Madlener, F. Otto, A test for
lambdaconfluence for certain prefix rewriting systems with
applications to the generalized word problem, Proc. ISSAC '90
(Tokyo, Japan, 2024 August 1990), ACM, NY, NY, 1990, pp. 815.
[Kuhner 1969] D. Kuhner, BiDirectional 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.
7390.
[Kuhner 1972] D. Kuhner, Some special purpose resolution
systems, Machine Intelligence 7, ed. B. Meltzer and D. Michie,
Edinburgh Univ. Press, Edinburgh, 1972, pp. 117128.
[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. 4954.
*[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,
2224 October 1986, pp. 270278.
*[Kuper 1988] G.M. Kuper, K.W. McAloon, K.V. Pallem, K.J. Perry,
Efficient parallel algorithms for antiunification and relative
complement, Tech. report IBM, 1987; also Proc. 3rd Annual Symp. on
Logic in Computer Science (Edinburgh, Scotland, 58 July 1988),
IEEE, 1988, pp. 112120.
*[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, 25
June 1987), ed. J.H. Davenport, LNCS 378, SpringerVerlag, Berlin,
1989, pp. 246257.
[Kutzler 1986a] B. Kutzler, S. Stifter, A geometry theorem
prover based on Buchberger's algorithm, Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 693694.
[Kutzler 1986b] B. Kutzler, S. Stifter, Collection of
computerized proofs of geometry theorems, Technical report
8612.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):389397, December 1986.
*[Kutzler 1986e] B. Kutzler, S. Stifter, Automated geometry
theorem proving using Buchberger's algorithm, Proc. 1986
ACMSIGSAM Symp. on Symbolic and Algebraic Computation (SYMSAC
'86, Univ. of Waterloo, Waterloo, Ontario, 2123 July 1986), ed.
B.W. Char, ACM, New York, NY, 1986, pp. 209214.
[Kutzler 1987] B. Kutzler, Implementation of a geometry proving
package in SCRATCHPAD II, Proc. EUROCAL '87 Conf., Leipzig, 25
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):195203.
[Ladner 1977] R.E. Ladner, The computational complexity of
provability in systems of modal propositional logic, SIAM J.
Computing 6(3):467480, 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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 187202.
*[Laird 1990] P. Laird, E. Gamble, Extending EBG to
termrewriting systems, Proc. 8th National Conf. on Artificial
Intelligence (AAAI90, July 29August 3, 1990, 1990), Vol. 2, AAAI
Press/The MIT Press, Menlo Park/Cambridge, pp. 929935.
[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 computerbased 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, 1719
January 1990), ACM, 1990, pp. 1630.
[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 ATP25,
Automatic Theorem Proving Project, Univ. of Texas at Austin, Math.
Dept., May 1975.
[Lankford 1975b] D.S. Lankford, Canonical inference, Tech.
Report ATP32, 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. ATP37, 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. ATP35, 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
commutativeassociative axioms: Complete sets of
commutativeassociative reductions, Rep. ATP39, 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 ATP36,
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, MTP1, Math. Dept., Louisiana Tech. Univ.,
Ruston, 1979.
[Lankford 1979b] D.S. Lankford, Mechanical theorem proving in
field theory, MTP2, Math. Dept., Louisiana Tech. Univ., January
1979.
[Lankford 1979c] D.S. Lankford, On proving term rewriting
systems are Noetherian, Tech. report MTP3, 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 MTP6, 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 (CADE4, Austin, Texas,
13 February 1979), ed. W.H. Joyner, 1979.
[Lankford 1980a] D.S. Lankford, A new complete FPAunification
algorithm, Tech. Report MTP8, Louisiana Tech. Univ., Ruston,
1980.
[Lankford 1980b] D.S. Lankford, Some remarks on inductionless
induction, Tech. Report MTP11, Louisiana Tech. Univ., Ruston, LA,
1980.
[Lankford 1981] D.S. Lankford, A simple explanation of
inductionless induction, Tech. Report MTP14, 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):193199; 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.
101108.
[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
(CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170,
SpringerVerlag, NY, 1984, pp. 128141; 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.
137154.
[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 nonnegative 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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
203221.
*[Lankford 1989b] D. Lankford, Nonnegative integer basis
algorithms for linear equations with integer coefficients, Tech.
Report, Louisiana Tech. University, Ruston, LA 71272, 1987; also
J. Automated Reasoning 5(1):2535, 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, 1519 December 1986), ed. M. Boscarol, L.C.
Aiello, and G. Levi, LNCS 306, SpringerVerlag, 1988, pp. 67113;
also Foundations of Deductive Databases and Logic Programming, ed.
J. Minker, Morgan Kauffman, Los Altos, CA, 1988, pp. 587625.
[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):301317, 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. 703710.
*[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.
3751.
[Lassez 1989b] J.L. Lassez, K. McAloon, Independence of negative
constraints, TAPSOFT 89, Advance Seminar on Foundations of
Innovative Software Development, LNCS 351, SpringerVerlag, 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 1012 April 1990), LNCS 429, ed. A Miola,
SpringerVerlag, 1990, pp. 164173.
*[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, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
222233.
[Laudet 1970] M. Laudet, D. Lacombe, L. Nolin, M.
Schutzenberger, eds. Symp. on Automatic Demonstration (Versailles,
France, 1968), Lecture Notes in Math. 125, SpringerVerlag,
Berlin, 1970.
[Laurent 1979] J.H. Laurent, Adding dynamic paramodulation to
rewrite algorithms, Tech. Rep. CSL102, 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. 298316.
[Lawrence 1974] J.D. Lawrence, J.D. Starkey, Experimental tests
for resolutionbased 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 resolutionbased theorem proving, Inf. Sciences 10(2):131154,
1976.
[Lazrek 1986] A. Lazrek, P. Lescanne, J.J. Thiel, Proving
inductive equalities, algorithms and implementation, Internal
Report CRIN 86R087, 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
(CADE7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170,
SpringerVerlag, NY, 1984, pp. 142165.
*[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 occurchecks in
unification, Proc. MFCS, LNCS 324, SpringerVerlag, 1988, pp.
433444.
[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):109119, 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
hypermatching strategy, Proc. 4th Methodologies for Intelligent
Systems (1214 October 1989, Charlotte, North Carolina), ed. Z.W.
Ras, Elsevier Science Publishing Co., NY, NY, 1989, pp. 467476.
[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, Substitutionbased
compilation of extended rules in deductive databases, 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. 5771.
*[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 (CSCSI90, Univ. of Ottawa, Ottawa, Canada, 2225 May
1990), published by CSCSI, 1990, pp. 204211.
[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 hyperlinking strategy, TR90032, Dept. of Computer
Science, Univ. of North Carolina at Chapel Hill, August 1990.
[Lehmer 1963] D.H. Lehmer, Some highspeed 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, 2527
September 1989), In Computational Intelligence, II, ed. F. Gardin,
G. Mauri, and M. Filippini, NorthHolland, Amsterdam, 1990, pp.
1926.
[Lenat 1976] D.B. Lenat, AM: An artificial intelligence approach
to discovery in mathematics as heuristic search, Stanford AI Lab.
Memo AIM286, Stanford University, July 1976; also in
Knowledgebased 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.
833842.
[Lenat 1977b] D.B. Lenat, The ubiquity of discovery, Proc. 5th
IJCAI, MIT, Cambridge, MA, August 1977, pp. 10931105.
[Lenat 1982] D. Lenat, AM: Discovery in mathematics as heuristic
search, KnowledgeBased Systems in Artificial Intelligence, ed.
Davis and Lenat, McGrawHill, 1982, pp. 3149.
[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):6198,
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, IJCAI87.
[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. 548550.
[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. 99108.
[Lescanne 1984a] P. Lescanne, Term rewriting systems and
algebra, Proc. 7th Intl. Conf. on Automated Deduction (CADE7,
Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, SpringerVerlag,
NY, 1984, pp. 166174.
[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. 181194; 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. 109121.
[Lescanne 1986] P. Lescanne, REVE: A Rewrite Rule Laboratory,
Proc. 8th Intl. Conf. on Automated Deduction (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 695696; also in Proc. 4th
STACS (Passau, FRG), ed. F.J. Brandenburg, G. VidalNaquet, and M.
Wirsing, LNCS 247, SpringerVerlag, 1987, pp. 482483.
[Lescanne 1987a] P. Lescanne, ed., Proc. 2nd Intl. Conf. on
Rewriting Techniques and Applications (Bordeaux, France, 2527 May
1987), LNCS 256, SpringerVerlag, Berlin, 1987.
[Lescanne 1987b] P. Lescanne, Current trends in rewriting
techniques and related problems, Proc. Trends in Computer Algebra,
Intl. Symp. (Bad Neuenahr, 1921 May 1987), ed. R. Janssen, LNCS
296, SpringerVerlag, Berlin, pp. 3851.
[Lescanne 1989] P. Lescanne, Completion procedures as transition
rules + control, In TAPSOFT'89 (vol. 1), ed. M. Diaz and F.
Orejas, LNCS 351, SpringerVerlag, 1989, pp. 2841.
*[Lescanne 1990a] P. Lescanne, ORME: An implementation of
completion procedures as sets of transitions rules (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. 661662.
*[Lescanne 1990b] P. Lescanne, On the recursive decomposition
ordering with lexicographical status and other related orderings,
J. of Automated Reasoning 6(1):3949, March 1990.
*[Lescanne 1990c] P. Lescanne, Well rewrite orderings, Proc. 5th
Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 47
June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990,
pp. 249256.
[Leszczylowski 1980a] J. Leszczylowski, An experiment with
Edinburgh LCF, Proc. 5th Conf. on Automated Deduction (Les Arcs,
France, 811 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87,
SpringerVerlag, Berlin, 1980, pp. 170181.
[Leszczylowski 1980b] J. Leszczylowski, Theory of FP systems in
Edinburgh LCF, Internal Report, CSR6180, Univ. of Edinburgh,
Dept. of Computer Sci., Edinburgh, April 1980.
[Leszczylowski 1980c] J. Leszczylowski, On proving laws of the
algebra of FPsystems in Edinburgh LCF, Proc. 1st Natl Conf. on
Artificial Intelligence, Stanford Univ., August 1980, pp. 8486.
[Letz 1988] R. Letz, J. Schumann, S. Bayerl, SETHEO  A
sequential theorem prover for firstorder logic, Technische
Universitat Munchen, 1988.
*[Letz 1993] R. Letz, On the polynomial transparency of
resolution, Proc. 13th IJCAI (Chambery, France, 28 August3
September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp.
123137.
*[Leung 1989] K.S. Leung, W. Lam, A fuzzy expert system shell
using both exact and inexact reasoning, J. of Automated Reasoning
5(2):207233, 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. 313328.
[Levine 1967] R.E. Levine, M.E. Maron, A Computer System for
Inference Execution and Data Retrieval, CACM 10(11):715721, 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.
337360, NorthHolland, 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 August3 September 1993), Vol 1, ed. R. Bajscy, IJCAI,
Inc., 1993, pp. 138145.
[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):134135, January 1978.
[Lewis 1980] H.R. Lewis, Complexity results for classes for
quantificational formulas, J. Comp. Syst. Sci. 21(1980):317353.
[Lewis 1982] H.R. Lewis, R. Statman, Unifiability is complete
for coNLOGSPACE, Information Processing Letters 15(1982):220222.
[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):123, 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, 123.
*[Ligeza 1993] A. Ligeza, A note on backware dual resolution and
its application to proving completeness of rulebased systems,
Proc. 13th IJCAI (Chambery, France, 28 August3 September 1993),
Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 132137.
[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. 11381145.
[Lim 1986] Y. Lim, The heuristics and experimental results of a
new hyperparamodulation: HLresolution, Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 240253.
*[Lincoln 1988] P. Lincoln, J. Christian, Adventures in
associativecommutative unification (A summary), Proc. 9th Intl.
Conf. on Automated Deduction (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 358367; also J. Symbolic Computation 8(1 and
2):217240, 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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 569573.
*[Lindsay 1987a] P.A. Lindsay, R.C. Moore, B. Ritchie, Review of
existing theorem provers, Tech. Report UMCS8782, Dept. of
Computer Science, Univ. of Manchester, 1987.
*[Lindsay 1987b] P.A. Lindsay, Logical frames for interactive
theorem proving, Tech. Report UMCS87127, Dept. of Computer
Science, Univ. of Manchester, 1987.
*[Lingenfelder 1986] C. Lingenfelder, Transformation of
refutation graphs into natural deduction proofs, SEKI Report
SR8610, Universitat Kaiserslautern, 1986.
*[Lingenfelder 1988] C. Lingenfelder, Structuring computer
generated proofs, SEKI Report SR8819, Universitat
Kaiserslautern, 1988; also in Proc. 11th IJCAI, ed. N.S.
Sridharan, Morgan Kaufmann, 1989, pp. 378383.
*[Lingenfelder 1989] C. Lingenfelder, Structuring computer
generated proofs, Proc. 11th IJCAI (Detroit, Michigan, USA, 2025
August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 378383.
[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 builtin equality predicate, Proc. 12th Intl.
Conf. on Artificial Intelligence, Vol 1 (IJCAI91, Darling
Harbour, Sydney, Australia, 2430 August 1991), Morgan Kaufmann
Publ., Inc., 1991, pp. 165170.
[Lins 1986] R.D. Lins, A new formula for the execution of
categorical combinators, Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 8998.
[Litvintchouk 1977] S.D. Litvintchouk, V.R. Pratt, A
proofchecker for dynamic logic, Proc. 5th IJCAI, MIT, Cambridge,
MA, 1977, pp. 552558.
[Liu 1985] X.H. Liu, H. Xiao, Operator fuzzy logic and fuzzy
resolution, Proc. 15th ISMVL, Canada, 5(1986):6875.
[Liu 1986a] X.H. Liu, Generalized resolution using
paramodulation, Kexue Tongbao (English edition) 31(21):14411444,
1986.
[Liu 1986b] X.H. Liu, K.Y. Fang, Fuzzy reasoning on lambdahorn
set, Proc. 16th ISMCL, USA, 5(1986):248251.
[Liu 1986c] X.H. Liu, C.K. Chang, J.J.P. Tsai, Fuzzy reasoning
base on lambdaLHresolution, Proc. IEEE 10th Intern. Computer
Software Application Conf., USA, 10(1986):154157.
*[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, 1317 July 1987, pp. 144148.
*[Liu 1990] P. Lui, A theoretical analysis of recurrence goals,
Proc. 9th ECAI (Stockholm, Sweden, 610 August 1990), ed. L.C.
Aiello, Pitman Publishing, London, 1990, pp. 413418.
[Livesey 1975] M. Livesey, J. Siekmann, Termination and
decidability results for stringunification, Univ. of Essex, Memo
CSM12, 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 (CADE4, Austin, Texas, 13 February 1979),
ed. W.H. Joyner, 1979, pp. 175184.
[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. 8403, 1983.
*[Llopis 1985] R. Llopis de Trias, An overview of completion
algorithms, 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. 424428.
[Lloyd 1984] J.W. Lloyd, Foundations of logic programming,
Symbolic Computation, SpringerVerlag, Heidelberg, 1984; Second
edition 1987.
[Loganantharaj 1985a] R. Loganantharaj, R.A. Muller, R.R.
Oldehoeft, Connection graph refutation: aspects of
ANDparallelism, Tech. Report CS8510, Dept. of Computer Science,
Colorado State Univ., 1985.
[Loganantharaj 1985b] R. Loganantharaj, R.A. Muller, R.R.
Oldehoeft, Some theoretical and implementational aspects of
Dcdpparallelism in connection graph refutation, Tech. Report
CS859, 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 (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 337352.
[Longo 1974] G. Longo, M.V. Zilli, Complexity of theorem proving
procedures: Some general properties, Rev. Fr. Autom. Inf. Rech.
Oper. 8(December 1974):518, France.
[Loos 1981] R. Loos, Term reduction systems and algebraic
algorithms, Proc. GWAI81, InformatikFachberichte 47, ed.
Siekmann, SpringerVerlag, Berlin, 1981, pp. 214234.
[Loveland 1968] D.W. Loveland, Mechanical theorem proving by
model elimination, JACM 15(2):236251, April 1968; also Automation
Of Reasoning  Classical Papers On Computational Logic, Vol. II,
19671970, ed. J. Siekmann And G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 117134.
[Loveland 1969a] D.W. Loveland, A simplified format for the
model elimination theoremproving procedure, JACM 16(3):349363,
July 1969; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 233248.
[Loveland 1969b] D. Loveland, Theoremprovers combining model
elimination and resolution, Machine Intelligence 4, ed. B. Meltzer
and D. Michie, Edinburgh Univ. Press, Edinburgh, 1969, pp. 7386;
also Automation Of Reasoning  Classical Papers On Computational
Logic, Vol. II, 19671970, ed. J. Siekmann And G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 249263.
[Loveland 1970a] D.W. Loveland, Some linear Herbrand proof
procedures: An analysis, Dept. of Comput. Sci., CarnegieMellon
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, SpringerVerlag, Berlin, 1970,
pp. 147162; also Automation Of Reasoning  Classical Papers On
Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 399416.
[Loveland 1972] D. Loveland, A unifying view of some linear
Herbrand procedures, JACM 19(2):366384, 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. 153161; also IEEE
Transactions on Computer C25(4):335341, April 1976.
[Loveland 1978] D.W. Loveland, Automatic Theorem Proving: A
Logical Basis, NorthHolland, Amsterdam.
[Loveland 1980] D.W. Loveland, R.E. Shostak, Simplifying
interpreted formulas, Tech. Report CSL117, SRI, Project 8752,
1980; also in Proc. 5th Conf. on Automated Deduction (Les Arcs,
France), ed. W. Bibel and R. Kowalski, SpringerVerlag, LNCS 87,
1980, pp. 97109.
[Loveland 1981] D.W. Loveland, C.R. Reddy, Deleting repeated
goals in the problem reduction format, JACM 28(4):646661, October
1981.
[Loveland 1982] D. Loveland, ed., Proc. 6th Conf. on Automated
Deduction, LNCS 138, SpringerVerlag, Berlin, 1982.
[Loveland 1984] D.W. Loveland, Automated theoremproving: A
quartercentury 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.
89118, pp. 145.
*[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, 2224 October 1986, pp. 214229.
[Loveland 1987] D.W. Loveland, NearHorn Prolog, CS198714,
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, NearHorn Prolog and beyond, J.
Automated Reasoning 7(1):126, March 1991.
*[Lownie 1989] T. M. Lownie, Extending reflective architectures,
Proc. 11th IJCAI (Detroit, Michigan, USA, 2025 August 1989), ed.
N.S. Sridharan, IJCAI Inc., 1989, pp. 446451.
[Lu 1988] J.J. Lu and V.S. Subrahmanian, Completeness issues in
RUENRF deduction, Logic Programming LPRGTR8824, Technical
Report, Syracuse Univ., 1988.
*[Lu 1990] J.J. Lu, V.S. Subrahmanian, Protected completions of
firstorder general logic programs, J. of Automated Reasoning
6(2):147172, 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
theoremproving, Machine Intelligence 1, ed. Collins and Michie,
American Elsevier, NY, 1967, pp. 4761.
[Luckham 1968a] D. Luckham, The ancestry filter method in
automatic demonstration, Stanford Artificial Intelligence Project
Memo, Stanford, 1968.
[Luckham 1968b] D. Luckham, Some treeparing strategies for
theoremproving, Machine Intelligence 3, ed. Dale and Michie,
Oliver and Boyd, Edinburgh, 1968, pp. 95112.
[Luckham 1970] D. Luckham, Refinement theorems in resolution
theory, Proc. IRIA Symp. on Automatic Demonstration (Versailles,
France), Lecture Notes in Math. 125, SpringerVerlag, Berlin,
1970, pp. 163190; also Automation Of Reasoning  Classical Papers
On Computational Logic, Vol. II, 19671970, ed. J. Siekmann And G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 435465.
[Luckham 1971] D. Luckham, N.J. Nilsson, Extracting information
from resolution proof trees, Artificial Intelligence 2(1):2754,
1971.
[Luckham 1979] D.C. Luckham, et al., Stanford Pascal verifier
user manual, Report STANCS79731, 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. 585599.
[Lusk 1977] E. Lusk, R. Overbeek, Experiments with
resolutionbased theoremproving algorithms, 3rd Workshop on
Automated Deduction, Boston, 1977.
[Lusk 1980] E. Lusk, R. Overbeek, Data structures and control
architecture for the implementation of theoremproving programs,
Proc. 5th Conf. on Automated Deduction (Les Arcs, France, 811
July 1980), ed. W. Bibel and R. Kowalski, LNCS 87,
SpringerVerlag, Berlin, 1980.
[Lusk 1982a] E. Lusk, W. McCune, R. Overbeek, Logic machine
architecture: Kernel functions, Proc. 6th Conf. on Automated
Deduction, ed. D. Loveland, LNCS 138, SpringerVerlag, Berlin,
1982, pp. 7084.
[Lusk 1982b] E. Lusk, W. McCune, R. Overbeek, Logic machine
architecture: Inference mechanisms, Proc. 6th Conf. on Automated
Deduction, ed. D. Loveland, LNCS 138, SpringerVerlag, Berlin,
1982, pp. 85108.
[Lusk 1982c] E.L. Lusk, R.A. Overbeek, Logic machine
architecture inference mechanisms  layer 2 user reference manual,
ANL8284, Math. and Comput. Sci. Div., Argonne National Lab.,
Argonne, Illinois, 1982 (release 2.0, 1984).
[Lusk 1982d] E.L. Lusk, R.A. Overbeek, An LMAbased theorem
prover, ANL8275, Math. and Comput. Sci. Div., Argonne National
Lab., Argonne, Illinois, 1982.
[Lusk 1982e] E. Lusk, R. Overbeek, Experiments with
resolutionbased theoremproving algorithms, Computers and
Mathematics with Applications 8(1982):141152.
[Lusk 1984a] E.L. Lusk, R.A. Overbeek, A portable environment of
research in automated reasoning, Proc. 7th Intl. Conf. on
Automated Deduction (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 4352.
[Lusk 1984b] E.L. Lusk, R.A. Overbeek, The automated reasoning
system ITP, ANL8427, 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 ANL8284, Rev. 1, Argonne National
Laboratory, April 1984.
[Lusk 1985a] E.L. Lusk, R.A. Overbeek, NonHorn problems, J. of
Automated Reasoning 1(1):103114, D. Reidel Publ. Co., Dordrecht,
Holland, 1985.
[Lusk 1985b] E.L. Lusk, R.A. Overbeek, Reasoning about equality,
J. of Automated Reasoning 1(2):209220, 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
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 697698.
*[Lusk 1988] E. Lusk, R. Overbeek, eds., Proc. 9th Intl. Conf.
on Automated Deduction (CADE9, Argonne, Illinois, 2326 May
1988), LNCS 310, SpringerVerlag, Berlin, 1988.
*[Lusk 1990] E. Lusk, W. McCune, Highperformance automated
theorem proving (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. 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 IJCAI91, ed.
L.N. Kanal and C.B. Suttner, Sydney, Australia, 1991, pp. 110116.
*[Lusk 1992a] E.L. Lusk, W.W. McCune, J. Slaney, ROO: A parallel
theorem prover, 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. 731734.
*[Lusk 1992b] E.L. Lusk, L. Wos, Benchmark problems in which
equality plays the major role, 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. 781785.
