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 C to E

[Caferra 1982] R. Caferra, Proof by matrix reduction as plan + validation, Proc. 6th Conf. on Automated Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982, pp. 309-325.

[Caferra 1984] R. Caferra, E. Eder, B. Frohoefer, W. Bibel, Extension of PROLOG through matrix reduction, ECAI-84, ed. T. O'Shea, North-Holland, Amsterdam, 1984, pp. 101-104.

*[Caferra 1992] R. Caferra, S. Demri, Semantic entailment in non classical logics based on proofs found in classical logic, 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. 385-399.

*[Caferra 1993] R. Caferra, S. Demri, Cooperation between direct method and translation method in non classical logics: some results in propositional S5, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 74-79.

[Campbell 1984] J.A. Campbell, Implementations of Prolog, Ellis Horwood, Chishester, England, 1984.

[Cantarella 1969] R.G. Cantarella, Efficient maximal semantic resolution proofs based upon binary semantic trees, PhD thesis, TR-69-3, Electrical Engineering Dept., Syracuse Univ., Syracuse, NY, June 1969.

[Cantone 1985] D.A. Cantone, A decision procedure for a class of unquantified formulae of set theory. VI. Multilevel syllogistic extended by the powerset operator, Comm. Pure Appl. Math. 38(1985):549-571.

[Cantone 1987a] D.A. Cantone, A decision procedure for a class of unquantified formulae of set theory involving the powerset and singleton operators, PhD thesis, Courant Institute of Mathematical Sciences, New York Univ., January 1987.

[Cantone 1987b] D. Cantone, A. Ferro, G. Sorace, B. Micale, Decision procedures for elementary sublanguages of set theory. IV. Formulae involving a rank operator or one occurrence of \sum(x) = {{y}|y \element x }, Comm. Pure Appl. Math. 37(1987):37-77.

[Cantone 1987c] D. Cantone, A. Ferro, J.T. Schwartz, Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator, J. Comp. Syst. Sci. 34(1):1-18, 1987.

[Cantone 1987d] D. Cantone, A. Ferro, E.G. Omodeo, J.T. Schwartz, Decision algorithms for some fragments of analysis and related areas, Comm. Pure App. Math. 40(1987):281-300.

[Cantone 1988a] D. Cantone, Decision procedures for elementary sublanguages of set theory, X. Multilevel syllogistic extended by the singleton and powerset operators, Tech. Report 373, Comp. Sci. Dept., New York Univ., May 1988; also J. Automated Reasoning 7:193-230.

*[Cantone 1988b] D. Cantone, V. Cutello, A. Ferro, Decision procedures for elementary sublanguages of set theory, XIV. Three languages involving rank related constructs, Proc. Intl. Symp. Symbolic and Algebraic Computation (ISSAC '88, Rome, Italy, 4-8 July 1988), ed. P. Gianni, LNCS 358, Springer-Verlag, Berlin, 1989, pp. 407-422.

[Cantone 1988c] D. Cantone, S. Ghelfo, E. Omodeo, The automation of syllogistic. I. Syllogistic normal forms, J. Symbolic Computation 6(1):83-98, 1988.

[Cantone 1988d] D. Cantone, A. Ferro, E.G. Omodeo, Decision procedures for elementary sublanguages of set theory, VIII. A semidecision procedure for finite satisfiability of unquantified set-theoretic formulae, Comm. Pure Appl. Math 51(1988):105-120.

*[Cantone 1989a] D. Cantone, A. Ferro, E. Omodeo, Computable Set Theory, Volume 1, Clarendon Press, Oxford, 1989.

*[Cantone 1989b] D. Cantone, E.G. Omodeo, On the decidability of formulae involving continuous and closed functions, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 425-430.

[Cantone 1989c] D. Cantone, E.G. Omodeo, Topological syllogistic with continuous and closed functions, Comm. Pure Appl. Math. 42(1989):1175-1188.

*[Cantone 1990a] D. Cantone, E.G. Omodeo, A. Policriti, The automation of syllogistic, II. Optimization and complexity issues, J. of Automated Reasoning 6(2):173-187, June 1990.

*[Cantone 1990b] D. Cantone, V. Cutello, Decision procedures for elementary sublanguages of set theory. XV. Multilevel syllogistic extended by the predicate finite and the operators singleton and pred, J. of Automated Reasoning 6(2):189-201, June 1990.

*[Cantone 1990c] D. Cantone, V. Cutello, A decidable fragment of the elementary theory of relations and some applications, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, p. 24-29.

*[Cantone 1991a] D. Cantone, Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset, J. of Automated Reasoning 7(2):193-230, June 1991.

*[Cantone 1991b] D. Cantone, J.T. Schwartz, Decision procedures for elementary sublanguages of set theory: XI. Multilevel syllogistic extended by the some elementary map constructs, J. of Automated Reasoning 7(2):231-256, June 1991.

[Carbonell 1983] J.G. Carbonell, Learning by analogy: Formulating and generalizing plans from past experience, Machine Learning, An Artificial Intelligence Approach, Vol. I, ed. Michalski, Carbonell, and Mitchell, Tioga Publishers, Palo Alto, CA, 1983, pp. 137-161.

[Cardelli 1982] L. Cardelli, ML under Unix, Bell Laboratories, Murray Hill, New Jersey, 1982.

[Cardelli 1986] L. Cardelli, A polymorphic lambda-calculus with type:type, DEC SCR Report, Digital Equipment Corp., Palo Alto, CA, 1986.

[Cardoza 1975] E. Cardoza, Computational complexity of the word problem for commutative semigroups, M.Sc. thesis, MIT, Cambridge, MA, August 1978; also MAC Tech, Memo 67, October 1975.

[Carlsson 1987] M. Carlsson, Freeze, indexing, and other implementation issues in the WAM, Proc. 4th Intl. Conf. on Logic Programming, 1987, p. 40.

[Cartwright 1976] R. Cartwright, A practical formal semantic definition and verification system for typed LISP, PhD thesis, Stanford Univ., 1976.

[Carvalho 1974] R.L. de Carvalho, Some results in automatic theorem-proving with applications in elementary set theory and topology, PhD thesis, Tech. Rep. 71, Dept. of C.S., Univ. of Toronto, Canada, November 1974.

*[Casanova 1989] M.A. Casanova, R Guerreiro, A. Silva, Logic programming with general clauses and defaults based on model elimination, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 395-400.

[Casley 1986] R. Casley, A proof editor for propositional temporal logic, STAN-CS-86-1109, Dept. of Computer Science, Stanford Univ., May 1986.

[Castaing 1980] J. Castaing, Y. Kodratoff, P. Degano, Theorem proving by the study of example proof traces, Proc. Intl. Workshop in Program Construction Bonas, 1980.

[Castaing 1984] J. Castaing, Y. Kodratoff, P. Degano, Theorem proving by the study of example proof traces or theorem proving by a correct theorem statement, In Automatic Program Construction Techniques, ed. A.W. Biermann, G. Guiho, Y. Kodratoff, 1984, pp. 421-431.

[Castaing 1985] J. Castaing, How to facilitate the proof of theorems by using the induction-matching, and by generalization, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985, pp. 1208-1213.

[Catach 1991] L. Catach, TABLEAUX: A general theorem prover for modal logics, J. Automated Reasoning 7(4):489-510, December 1991.

[Cavalli 1984] A.R. Cavalli, L. Farinas del Cerro, A decision method for linear temporal logic, Proc. 7th Intl. Conf. on Automated Deduction (CADE-7, Napa, CA, May 1984), ed. R.E. Shostak, LNCS 170, Springer-Verlag, NY, 1984, pp. 113-127.

[Cavenathi 1987] M. Cavenathi, M. de Zanet, G. Mauri, MC-OBJ: a C interpreter for OBJ, Tech. Report draft, Depmentarto Scienze dell'Informazione, Universita de Milano, 1987.

[Caviness 1967] Caviness, On canonical form and simplification, PhD Dissertation, Pittsburgh, Carnegie-Mellon Univ., 1967; also JACM 17(2):385-396, 1970.

[Champeaux 1978] D. de Champeaux, A theorem prover dating a semantic network, Proc. AISB/GI Conf. on Artificial Intelligence, Hamburg, W. Germany, July 1978, pp. 82-92.

[Champeaux 1979] D. de Champeaux, Sub-problem finder and instance checker - Two cooperating preprocessors for theorem provers, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 110-114; also Proc. 6th IJCAI, Tokyo, 1979, pp. 191-196.

[Champeaux 1981a] D. de Champeaux, Challenge problem 1 without search, ACM SIGART 76, April 1981, pp. 12-13.

[Champeaux 1981b] D. Champeaux, B. Domolki, T. Gergely, Other directions for automatic theorem proving, Mathematical Logic in Computer Science, North-Holland, 1981.

[Champeaux 1981c] D. de Champeaux, J. de Bruin, Symbolic evaluation of Lisp functions with side effects for verification, Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, August 1981, pp. 519-527.

[Champeaux 1982] D. de Champeaux, A note on resolution, connection graphs and subsumption, ACM SIGART Newsletter 81, July 1982, pp. 15-17.

[Champeaux 1986a] D. de Champeaux, Sub-problem finder and instance checker, two cooperating modules for theorem provers, JACM 33(4):633-657, October 1986.

[Champeaux 1986b] D. de Champeaux, About the Paterson-Wegman linear unification algorithm, J. of Computer and System Sciences 32(1986):79-90.

*[Chan 1977] Tat-Hung Chan, An algorithm for checking PL/CV arithmetic inferences, Tech. Report 77-326, Computer Science Dept., Cornell Univ., October 1977; also In: An Introduction to the PL/CV2 Programming Logic, ed. Constable, Johnson and Eichenlaub, LNCS 135, Springer-Verlag, Berlin, 1982, Appendix D, pp. 227-264.

[Chandru 1991] V. Chandru, J.N. Hooker, Extended Horn sets in propositional logic, JACM 38(1):205-221, January 1991.

[Chang 1970a] C. Chang, The unit proof and the input proof in theorem proving, JACM 17(October 1970):698-707; also Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 331-341.

[Chang 1970b] C. Chang., Renamable paramodulation for automatic theorem proving with equality, Artificial Intelligence 1(Winter 1970):47-256.

[Chang 1970c] C.L. Chang, R.C.T. Lee, J.R. Slagle, A new algorithm for generating prime implicants, IEEE Trans. on Computers C-19(4):304-310, 1970.

[Chang 1970d] C.L. Chang, R.C.T. Lee, Notes on theorem proving, Div. of Computer Res. and Tech., National Institute of Health, Bethesda, MD, 1970.

[Chang 1971a] C. Chang, J. Slagle, Completeness of linear resolution for theories of equality, JACM 18(January 1971):125-136.

[Chang 1971b] C.L. Chang, Theorem proving by generation of Pseudo-semantic trees, Div. of Computer Res. and Tech. Nat. Inst. of Health, Bethesda, Maryland, 1971.

[Chang 1972a] C.L. Chang, Theorem proving with variable-constrained resolution, Information Sci. 4(1972):217-231.

[Chang 1972b] C. Chang, The decomposition principle for theorem proving systems, Proc. 10th Annual Allerton Conf. on Circuit and System Theory, Univ. of Illinois, 1972, pp. 20-28.

[Chang 1973a] C. Chang, R. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, NY, 1973.

[Chang 1973b] C.L. Chang, R.C.T. Lee, J.K. Dixon, The specialization of programs by theorem proving, SIAM J. Comput. 2(1):7-15, March 1973.

[Chang 1979a] C.L. Chang, J.R. Slagle, Using rewriting rules for connection graphs to prove theorems, Artificial Intelligence 12(2):159-180, 1979.

[Chang 1979b] C.L. Chang, Resolution plans in theorem proving, Proc. 6th IJCAI, Tokyo, August 20-23, 1979, pp. 143-148.

[Chapman 1985] D. Chapman, Planning for conjunctive goals, Memo AI-802, AI Lab, MIT, 1985.

[Char 1983] B.W. Char, K.O. Geddes, W.M. Gentleman, G.H. Gonnet, The design of Maple: A compact, portable, and powerful computer algebra system, Proc. EUROCAL '83, LNCS 162, 1983, pp. 101-115.

[Char 1985] B.W. Char, K.O. Geddes, G.H. Gonnet, S.M. Watt, Maple User's Guide, WATCOM Publications, Waterloo, Ontario, 1985.

*[Char 1989] B.W. Char, A.r. Macnaughton, P.A. Strooper, Discovering inequality conditions in the analytic solution of optimization problems, J. Automated Reasoning 5(3):339-362, September 1989.

[Char 1990] B.W. Char, K.O. Geddes, G.H. Gonnet, M.B. Monagan, S.M. Watt, Maple Reference Manual, 5th ed., Waterloo Maple Publ., Waterloo, Ontario, Canada, 1990.

*[Charminade 1988] G. Charminade, Some computational aspects of an order-sorted calculus: order-sorted unification using compact representation of clauses, Proc. 8th ECAI, Institut fur Informatik der Technischen Universitat Munchen, 1-5 August 1988, pp. 625-630.

*[Charniak 1985] E. Charniak, D. McDermott, Introduction to Artificial Intelligence, Addison-Wesley, Reading, MA 1985.

[Chen 1986] T.Y. Chen, J.-L. Lassez, G.S. Port, Maximal unifiable subsets and minimal non-unifiable subsets, New Generation Computing 4(1986):133-152.

*[Chen 1992] W.Z. Chen, Tactic-based theorem proving and knowledge-based forward chaining: An experiment with Nuprl and Ontic, 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. 552-566.

[Cheng 1986] P.D. Cheng, A parallel theorem prover based on connection graph, Master's thesis, Northwestern Univ., Evanston, Illinois, December 1986.

*[Cheng 1987] P.D. Cheng, J.Y. Juang, A parallel resolution procedure based on connection graph, Proc. 6th Natl Conf. on Artificial Intelligence (AAAI 87), Seattle, Washington, 13-17 July 1987, pp. 13-17.

[Cherifa 1986] A.B. Cherifa, P. Lescanne, An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations, 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. 42-51.

[Cherifa 1987] A.B. Cherifa, P. Lescanne, Terminiation of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming 9(2), October 1987, pp. 137-160.

[Chester 1976] D. Chester, The translation of formal proofs into English, Artificial Intelligence 7(3):261-278, 1976.

[Chew 1980] L.P. Chew, An improved algorithm for computing with equations, Proc. 21st Annual Symp. on Foundations of Computer Science (Los Angeles, CA), IEEE, 1980, pp. 108-117.

[Chew 1981] L.P. Chew, Unique normal roms in term rewriting systems with repeated variables, Proc. 13th Annual ACM Symp. on Theory of Computing, 1981, pp. 7-18.

*[Chi 1988] S. Chi, L.J. Henschen, Recursive query answering with non-Horn clauses, 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. 294-312.

[Chinlund 1964] T.J. Chinlund, M. Davis, P.G. Hineman, M.D. McIlroy, Theorem proving by matching, Technical Report, Bell Laboratory, Murray Hill, NJ, 1964.

*[Chirimar 1992] J. Chirimar, C.A. Gunter, M. VanInwegen, Xpnet: A graphical interface to proof nets with an efficient proof checker, 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. 711-715.

*[Chisholm 1989] G.H. Chisholm, B.T. Smith, A.S. Wojcik, An automated reasoning problem associated with proving claims about programs using Floyd-Hoare inductive assertion methods, J. Automated Reasoning 5(4):533-540, December 1989.

*[Cholvy 1993] L. Cholvy, Proving theorems in a multi-source environment, Proc. 13th IJCAI (Chambery, France, 28 August-3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp. 66-73.

[Choppy 1985] C. Choppy, C. Johnen, Petrireve: Proving Petri net properties with rewriting systems, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 271-286.

[Choppy 1987] C. Choppy, S. Kaplan, M. Soria, Algorithmic complexity of term rewriting systems, 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. 256-273.

[Choque 1984] G. Choque, How to compute a complete set of minimal incrementations with the recursive decomposition ordering? Internal report 84-R-056, Centre de Recherche en Informatique de Nancy, Nancy, France, 1984.

[Chou 1983] S.-C. Chou, Topics in Wu's method, Automatic Theorem Proving Project, Dept. of Mathematics and Computer Sciences, Univ. of Texas at Austin, ATP 76, 1983.

[Chou 1984] S.-C. Chou, Proving elementary geometry theorems using Wu's algorithm, In: Automated Theorem Proving: After 25 Years, ed. W.W. Bledsoe and D.W. Loveland, American Mathethematical Society Contemporary Mathematics Series 29(1984):243-286.

[Chou 1985] S.-C. Chou, Proving and discovering theorems in elementary geometries using Wu's method, PhD thesis, Dept. of Mathematics, Univ. of Texas at Austin, TX, December 1985.

[Chou 1986a] S.-C. Chou, W.F. Schelter, Proving geometry theorems with rewrite rules, J. of Automated Reasoning 2(3):253-273, September 1986.

[Chou 1986b] S.C. Chou, H.P. Ko, On mechanical theorem proving in Minkowshian plane geometry, Proc. IEEE Symp. on Logic in Computer Science, Cambridge, MA, 16-18 June 1986, pp. 187-192.

[Chou 1986c] S.C. Chou, GEO-Prover - A geometry theorem prover developed at UT, 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. 679-680.

[Chou 1986e] S.C. Chou, A step toward mechanical proving geometry theorems involving inequality - experimental results, Preprint, Institute for Computing Science, Univ. of Texas at Austin, March 1986.

[Chou 1986f] S.-C. Chou, Proving geometries using Wu's method: A collection of geometry theorems proved mechanically, Tech. Report 50, Institute for Computing Science, Univ. of Texas at Austin, July 1986. (366 theorems)

[Chou 1986g] S.-C. Chou, J.-G. Yang, On the algebraic formulation of geometry theorems, Presented at International Workshop on Geometry Reasoning, Oxford, England, 1986.

[Chou 1987] S.-C. Chou, A method for the mechanical derivation of formulas in elementary geometry, J. of Automated Reasoning 3(3):291-299, September 1987.

*[Chou 1988a] S.-C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Holland, 1988.

*[Chou 1988b] S.-C. Chou, An introduction to Wu's method for mechanical theorem proving in geometry, J. Automated Reasoning 4(3):237-267, September 1987.

[Chou 1989a] S.-C. Chou, S.-S. Gao, Mechanical theorem proving in differential geormetry, TR-89-08, Dept. of Computer Sciences, Univ. of Texas at Austin, Texas, March 1989.

*[Chou 1989b] S.C. Chou, X.S. Gao, Ritt-Wu's decomposition algorithm and geometry theorem proving, TR-89-09, Dept. of Computer Sciences, Univ. of Texas at Austin, Texas, March 1989; also 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. 207-220.

[Chou 1989c] S.-C. Chou, S.-S. Gao, Automated reasoning in mechanics using Ritt-Wu's methods, TR-89-11, Dept. of Computer Sciences, Univ. of Texas at Austin, Texas, April 1989.

[Chou 1989d] S.C. Chou, X.S. Gao, A class of geometry statements of constructive type and geometry theorem proving, TR-89-37, Computer Sciences Dept., Univ. of Texas at Austin, November 1989.

[Chou 1989e] S.C. Chou, X.S. Gao,N. McPhee, A combination of Ritt-Wu's method and Collins' method, TR-89-28, Computer Sciences Dept., Univ. of Texas at Austin, October 1989.

[Chou 1989f] S.C. Chou, X.S. Gao, Mechanical formula derivation in elementary geometries, TR-89-21, Computer Sciences Dept., Univ. of Texas at Austin, August 1989.

[Chou 1989g] S.C. Chou, X.S. Gao, A collection of 120 computer solved geometry problems in mechanical formula derivation, TR-89-22, Computer Sciences Dept., Univ. of Texas at Austin, August 1989.

[Chou 1989h] S.C. Chou, X.S. Gao, On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving, Algorithmica 4(1989):237-262.

*[Chou 1989i] S.-C. Chou, W.F. Schelter, J.G. Yang, Characteristic sets and Grobner bases in geometry theorem proving, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 33-92.

[Chou 1990a] S.-C. Chou, X.S. Gao, Techniques for Ritt-Wu's decomposition algorithm, TR-90-2, Computer Sciences Dept., Univ. of Texas at Austin, February 1990.

*[Chou 1990b] S.-C. Chou, Automated reasoning in geometries using the characteristic set method and Grobner basis method, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, pp. 255-260.

*[Chou 1990c] S.-C. Chou, Methods for mechanical geometry formula deriving, Proc. ISSAC '90 (Tokyo, Japan, 20-24 August 1990), ACM, NY, NY, 1990, pp. 265-270.

*[Chou 1992a] S.-C. Chou, X.-S. Gao, Proving geometry statements of constructive type, 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. 20-34.

*[Chou 1992b] S.-C. Chou, A geometry theorem prover for Macintoshes, 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. 686-690.

*[Chouraqui 1982] E. Chouraqui, Construction of a model for reasoning by analogy, Proc. ECAI-82, Univ. Paris-Sud, Orsay, France, 12-14 July 1982, pp. 48-53.

[Christian 1987] J. Christian, P. Lincoln, Adventures in associative-commutative unification, MCC Tech. Report ACA-ST-275-87, Microelectronics and Computer Technology Corp., Austin, TX, October 1987.

*[Christian 1989a] J. Christian, Fast Knuth-Bendix commpletion: summary, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 551-555.

[Christian 1989b] J. Christian, High performance permutative completion, Tech. Report ACT-AI-303-89, MCC, August 1989, PhD thesis.

*[Christian 1992] J. Christian, Some termination criteria for narrowing and E-narrowing, 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. 582-587.

[Church 1940] A. Church, A formulation of the simple theory of types, Symbolic Logic 5(1):56-68, 1940.

[Church 1951] A. Church, The calculi of lambda-conversion, Annals of Mathematics Studies, No. 6, Princeton Univ. Press, Princeton, NJ, 1951.

[Church 1952] A. Church, Special cases of the decision problem, Revue Philosophique de Louvain 49, 1951, A Correction ibid. 50, 1952.

[Chvatal 1988] V. Chvatal, E. Szemeredi, Many hard examples for resolution, JACM 35(4):759-768, October 1988.

[Cialdea 1986] M. Cialdea, Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic, Information Processing Letters 22(2):87-90, 1986.

[Cialdea 1991] M. Cialdea, Resolution for some first-order modal systems, Theor. Comput. Sci. 85(2):213-229, August 1991.

*[Cichon 1992] A. Cichon, P. Lescanne, Polynomial interpretations and the complexity of algorithms, 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. 139-147.

[Clark 1982] K. Clark, S.A. Tarnlund, eds., Logic Programming, Academic Press, 1982.

*[Clarke 1992] E. Clarke, X. Zhao, Analytica - A theorem prover in mathematica, 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. 761-765.

[Clausen 1987] M. Clausen, A. Fortenbacher, Efficient solution of linear diophantine equations, Internal Report 32/87, Universitat Karlsruhe, 1987; also J. Symbolic Computation 8(1 and 2):201-216, 1989 (special issue on unification, part 2).

[Cline 1989] M.P. Cline, A fast parallel algorithm for N-ary unification with A.I. applications, PhD thesis, Clarkson Univ. Potsdam, NY 13676, April 1989.

[Clocksin 1981] W.F. Clocksin, C.S. Mellish, Programming in Prolog, Springer-Verlag, NY, 1981.

[Cochet 1976] Y. Cochet, Church-Rosser congruences on free semigroups, Coll. Math. Soc. Janos Bolyai: Algebraic Theory of Semigroups 20(1976): 51-60.

[Coelho 1974] H. Coelho, An inquiry on the geometry machine and its extensions with a review of previous work, Working report 1 for INVOTAN, 1974.

[Coelho 1979] H. Coelho, L.M. Pereira, GEOM: A Prolog geometry theorem prover, Laboratorio Nacional de Engenharia Civil, Memoria 525, Portugal, 1979.

[Coelho 1980] H. Coelho, J.C. Cotta, L.M. Pereira, How to solve it with Prolog, Laboratorio Nacional de Engenharia Civil, Lisboa, Portugal, 1980.

[Coelho 1986] H. Coelho, L.M. Pereira, Automated reasoning in geometry theorem proving with Prolog, J. of Automated Reasoning 2(4):329-390, December 1986.

*[Cohen 1971] J. Cohen, A. Rubin, An interactive system for proving theorems in the predicate calculus, Proc. 2nd Symp. on Symbolic and Algebraic Manipulation (Los Angeles, CA, March 23-25), ed. S.R. Petrick, ACM, NY, 1971, pp. 268-280.

[Cohen 1974] J. Cohen, L. Trilling, P. Wegner, A nucleus of a theorem-prover described in ALGOL-68, Intl. J. of Computer and Information Sciences, vol. 3, no. 1, 1974.

[Cohen 1980] D.N. Cohen, Knowledge Based Theorem Proving and Learning, PhD thesis, Carnegie Mellon Univ., 1980; also UMI Research Press, Ann Arbor, Michigan, 1982.

[Cohen 1982] P.R. Cohen, E.A. Feigenbaum, The Handbook of Artificial Intelligence 3, William Kaufmann Inc., Los Altos, CA, 1982, pp. 75-124.

[Cohn 1979] A. Cohn, Machine assisted proofs of recursion implementation, PhD thesis, Dept. of Computer Science, Univ. of Edinburgh, 1979.

[Cohn 1979b] A. Cohn, High level proof in LCF, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979, pp. 73-80.

[Cohn 1981] A. Cohn, The equivalence of two semantic definitions: A case study in LCF, Report CSR-76-81, Computer Science Dept., Univ. of Edinburgh, Scotland, 1981.

[Cohn 1982] A. Cohn, R. Milner, On using Edinburgh LCF to prove the correctness of a parsing algorithm, Internal Report, CSR-113-82, Univ. of Edinburgh, Dept. of Computer Sci., Edinburgh, 1982.

[Cohn 1983a] A.G. Cohn, Improving the expressiveness of many sorted logic, Proc. 3rd Natl Conf. on Artificial Intelligence, Washington, D.C., August 1983, pp. 84-87.

[Cohn 1983b] A.G. Cohn, Mechanising a particularly expressive many sorted logic, PhD dissertation, Dept. of Computer Science, Univ. of Essex, Essex, England, January 1983.

[Cohn 1985] A.G. Cohn, On the solution of Schubert's steamroller in many-sorted logic, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 18-23 August 1985, W. Kaufmann, Inc., pp. 1169-1174.

[Cohn 1987] A.G. Cohn, A more expressive formulation of many sorted logic, J. of Automated Reasoning 3(2):113-200, June 1987.

*[Cohn 1989a] A. Cohn, The notion of proof in hardware verification, J. of Automated Reasoning 5(2):127-139, June 1989.

[Cohn 1989b] A.G. Cohn, On the appearance of sortal literals: a non substitutional framework for hybrid reasoning, Proc. 1st Intl. Conf. on Principles of Knowledge Representation and Reasoning, ed. R.J. Brachman, H.J. Levesque and R. Reiter, Toronto, Ontario, 1989, pp. 55-66.

*[Cohn 1992] A.G. Cohn, A many sorted logic with possibly empty sorts, 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. 633-647.

[Coleman 1987] D. Coleman, R.M. Gallimore, V.S. Stavridou, The design of a rewrite rule interpreter from algebraic specifications, IEEE Software Engineering J. (July 1987):95-104.

[Collins 1962] G.E. Collins, Computational reductions in Tarski's decision method for elementary algebra, IBM Corp., Yorktown Heights, 1962.

[Colmerauer 1984] A. Colmerauer, Equations and inequations on finite and infinite trees, Proc. Conf. on Future Generations Computer Systems (FGCS'84), ICOT, November 1984, pp. 85-99.

*[Colussi 1992] L. Colussi, E. Marchiori, A predicate transformer for unification, Proc. Joint Intl. Conf. and Symp. on Logic Programming, ed. K. Apt, The MIT Press, Cambridge, MA, 1992, pp. 67-81.

[Comon 1986] H. Comon, Sufficient completeness, term rewriting systems and "anti-unification", 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. 128-140.

[Comon 1988] H. Comon, P. Lescanne, Equational problems and disunification, Universite de Grenoble and Centre de Rech. en Inform. de Nancy, 1988.

*[Comon 1989] H. Comon, Inductive proofs by specification transformations, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 76-91.

*[Comon 1990] H. Comon, Solving inequations in term algebras, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 62-69.

*[Conry 1990] S.E. Conry, D.J. MacIntosh, and R.A. Meyer, DARES: A Distributed Automated REasoning System, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 78-85.

[Constable 1971] R.L. Constable, Constructive mathematics and automatic programs writers, Proc. IFIP congress, Ljubljana, 1971, pp. 229-233.

[Constable 1977] R.L. Constable, A constructive programming logic, Information Processing 77, NY: North-Holland, 1977, pp. 733-738.

[Constable 1978] R.L. Constable, M.J. O'Donnell, A Programming Logic, Winthrop Publ., Cambridge, MA, 1978.

[Constable 1980] R.L. Constable, D. Zlatin, Report on the PL/CV3 programming logic, Cornell Univ., Dept. of Comput. Sci., Tech. Report, June 1980.

*[Constable 1982] R.L. Constable, S.D. Johnson, C.D. Eichenlaub, An Introduction to PL/CV2 Programming Logic, LNCS 135, Springer-Verlag, Berlin, 1982.

[Constable 1983a] R.L. Constable, J.L. Bates, Proofs as programs, Dept. of Computer Science, Cornell Univ., February 1983.

[Constable 1983b] R.L. Constable, Proofs as programs: a synopsis, Information Processing Letters 16(3):105-112, 1983.

[Constable 1983c] R.L. Constable, J.L. Bates, The nearly ultimate PRL, TR-83-551, Dept. of Computer Science, Cornell Univ., Ithaca, December 1983.

[Constable 1985a] R.L. Constable, T.B. Knoblock, and J.L. Bates, Writing programs that construct proofs, J. of Automated Reasoning 1(3):285-326, D. Reidel Publ. Co., Dordrecht, Holland, 1985.

[Constable 1985b] R.L. Constable, J.L. Bates, Proofs as programs, ACM Trans. Prog. Lang. Sys., 7(1):113-136, 1985.

[Constable 1985c] R.L. Constable, Constructive mathematics as a programming logic I: some principles of theory, Annuals of Discrete Math. 24(1985):21-38.

[Constable 1985d] R.L. Constable, N.P. Mendler, Recursive definitions in type theory, Proc. Logics of Programs Conf., LNCS, Springer-Verlag, NY, 1985, pp. 66-78.

*[Constable 1986] R. Constable, et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, Englewood Cliffs, NJ, 1986.

*[Constable 1990] R.L. Constable, D.J. Howe, Implementing metamethematics as an approach to automatic theorem proving, In Formal Techniques in Artificial Intelligence: A Sourcebook, ed. R.B. Banerji, Elsevier Science Publishers, Amsterdam, 1990, pp. 45-75.

[Cook 1965] S.A. Cook, Algebraic techniques and the mechanization of number theory, RM-4319-PR, RAND Corp., Santa Monica, CA, 1965.

[Cook 1971] S.A. Cook, The complexity of theorem proving procedures, Proc. 3rd ACM Symp. on Theory of Computing, 1971, pp. 151-158.

[Cook 1974] S.A. Cook, R.A. Reckhow, On the lengths of proofs in the propositional calculus, Proc. 6th ACM STOC, 1974, pp. 135-148; Corrections in: ACM SIGACT News 6(3):15-22, 1974.

[Cook 1975] S.A. Cook. Feasibility constructive proofs in the propositional calculus, Proc. 7th Annual ACM Symp. on Th. of Computing, pp. 83-97, 1975. [Cook 1976] S.A. Cook, A short proof on the Pigeon-hole principle using extended resolution, ACM SIGACT News 8(October - December 1976):28-32.

[Cook 1979] S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, J. of Symbolic Logic 44(1979):36-50.

[Cook 1990] J.V. Cook, Verification of the C/30 Microcode Using the State Delta Verification System (SDVS), In Proceedings of the 13th National Computer Security Conference (Washington, D. C.), pp. 20--31, National Institute of Standards and Technology/National Computer Security Center, October 1990.
(source: Leo Marcus)

[Cook 1991] J.V. Cook, I.V. Filippenko, B.H. Levy, L.G. Marcus, and T.K. Menas, Formal Computer Verification in the State Delta Verification System (SDVS), In Proceedings of the AIAA Computing in Aerospace Conference (Baltimore, MD), American Institute of Aeronautics and Astronautics, October 1991.
(source: Leo Marcus)

[Cooper 1966] D.C. Cooper, Theorem proving in computers, Advances in programming and non-numerical computation, ed. Fox, Pergamon Press, Oxford, 1966, pp. 155-182.

[Cooper 1967] D.C. Cooper, Mathematical proofs about computer programs, Machine Intelligence 1, ed. Collins and Michie, American Elsevier, NY, 1967, pp. 17-30.

[Cooper 1971] D.C. Cooper, Programs for mechanical program verification, Machine Intelligence 6, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1971, pp. 43-59.

[Cooper 1972] D.C. Cooper, Theorem proving in arithmetic without multiplication, Machine Intelligence 7, ed. B. Meltzer and D. Michie, Univ. of Edinburgh, 1972, pp. 91-99.

*[Cooperman 1986] G. Cooperman, A semantic matcher for computer algebra, 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. 132-134.

[Copi 1959] K. Copi, M. Beard, Programming an idealized general purpose computer to decide questions of truth and falsehood, Rep. 2144-402-T, Willow Run Lab., Univ. of Michigan, 1959.

[Coquand 1984] T. Coquand, G. Huet, A theory of constructions, Preliminary version, Presented at the Intl. Symp. on Semantics of Data Types, Sophia-Antipolis, June 1984.

*[Coquand 1985] T. Coquand, G. Huet, Constructions: A higher order proof system for mechanizing mathematics, Proc. European Conf. on Computer Algebra (EUROCAL'85, Linz, Austria, 1-3 April 1985), Vol. 1: Invited Lectures, ed. B. Buchberger, LNCS 203, Springer-Verlag, Berlin, 1985, pp. 151-184.

[Coquand 1988] T. Coquand, G. Huet, The calculus of constructions, Information and Computation 76(1988):95-120.

[Corbin 1983] J. Corbin, M. Bidoit, A rehabilitation of Robinson's unification algorithm, Proc. IFIP 83, ed. R.E.A. Mason, Elsevier Science Publ., September 1983, pp. 909-914; 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, p. 73.

[Coscai 1988] P. Coscai, P. Franceschi, G. Levi, G. Sardu, L. Torre, Meta-level definition and compilation of inference engines in the epsilon logic programming environment. Proc. 5th Intl. Conf. and Symp. on Logic Programming, ed. R. Kowalski and K.A. Bowen, Seattle, 1988, pp. 359-373.

[Cosmadakis 1985] S. Cosmadakis, P. Kanellakis, Two applications of equational theories to data base theory, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 107-123.

*[Costa 1982] E.J.F. Costa, Weakly commuting term rewriting systems: application to automatic recursion removal, Proc. ECAI-82, Paris-Sud, Orsay, France, 12-14 July 1982, pp. 87-90.

*[Costa 1990] N.C.A. da Costa, L.J. Henschen, J.J. Lu, V.S. Subrahmanian, Automatic theorem proving in paraconsistent logics: Theory and implementation, 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. 72-86.

*[Courcelle 1989] B. Courcelle, On recognizable sets and tree automata, In: Resolution of Equations in Algebraic Structures: Vol 1, Algebraic Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 93-126.

[Cowan 1979] R.M. Cowan, M.L. Griss, Hashing - The key to rapid pattern matching, Symbolic and Algebraic Computation, Eurosam '79, An Intl. Symp. on Symbolic and Algebraic Manipulation, EUROSAM, New York, 1979, pp. 266-278.

[Cox 1976] P. Cox, T. Pietrzykowski, A graphical deduction system, Dept. of Comput. Sci., Univ. of Waterloo, Canada, 1976.

[Cox 1977] P.T. Cox, Deduction plans: a graphical proof procedure for the first order predicate calculus, PhD, Dept. Comput. Sci., Univ. of Waterloo, 1977.

[Cox 1978] P.T. Cox, Locating the source of unification failure, Proc. 2nd Natl Conf. Canadian Soc. for Computational Studies of Intelligence, Toronto, July 1978, pp. 20-29.

[Cox 1979] P.T. Cox, Representational economy in a mechanical theorem prover, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979.

[Cox 1980] P.T. Cox, T. Pietrzykowski, A complete, nonredundant algorithm for reversed skolemization, 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. 374-385.

[Cox 1981a] P.T. Cox, T. Pietrzykowski, Deduction plans: A basis for intelligent backtracking, IEEE Trans. on Pattern Analysis and Machine Intelligence PAMI-3(1):52-65, January 1981.

[Cox 1981b] P.T. Cox, On determining the causes of non-unifiability, Auckland Computer Science Report No. 23, Univ. of Auckland, 1981; also J. Logic Programming 4(1987):33-58.

[Cox 1984] P.T. Cox, T. Pietrzykowski, A complete, nonredundant algorithm for reversed skolemization, Theoretical Computer Science 28(1984):239-261.

[Cox 1985] P.T. Cox, T. Pietrzykowski, Surface deduction: a uniform mechanism for logic programming, Proc. 1985 Logic Prog. Symp., Boston, 1985, pp. 220-227.

[Cox 1986a] P.T. Cox, T. Pietrzykowski, Causes for events: their computation and applications, 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. 608-621.

[Cox 1986b] P.T. Cox, T. Pietrzykowski, Incorporating equality in logic programming via surface deduction, Annals of Pure and Applied Logic 31(1986):177-189.

[Craig 1957a] W. Craig, Linear reasoning: A new form of the Herbrand-Gentzen theorem, J. Symbolic Logic 22(1957):250-268.

[Craig 1957b] W. Craig, Three uses of the Herbrand-Gentzen theorem relating model theorem to proof theorem, J. Symbolic Logic 22(1957):269-286.

[Craigen 1987] D. Craigen, et al., m-EVES: A tool for verifying software, TR-87-5402-26, I.P. Sharp Associates Limited, August 1987; also in Proc. 10th Intl. Conf. on Software Engineering, Singapore, 11-15 April 1987.

*[Craigen 1992] D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, M. Saaltink, EVES system description, 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. 771-775.

[Crone-Rawe 1989] B. Crone-Rawe, Unification algorithms for Boolean rings, SEKI Working Paper SWP-89-01, Universitat Kaiserslautern, 1989.

[Cunningham 1983a] R.J. Cunningham, S. Zappacosta-Amboldi, Software tools for first-order logic, Software Practice and Experience 13(1983):1019-1025.

[Cunningham 1983b] R.J. Cunningham, A.J.J. Dick, Rewrite systems on a lattice of types, Rep. No. DOC 83/7, Imperial College, London SW7, 1983; also Acta Informatica 22, 1985, pp. 149-169.

[Curry 1958] H.B. Curry, R. Feys, W. Craig, Combinatory Logic, Vol. 1, North-Holland, Amsterdam, 1958.

[Curry 1972] H.B. Curry, J.R. Hindley, J.P. Seldin, Combinatory Logic, Vol. 2, North-Holland, Amsterdam, 1972.

*[Cvetkovic 1988] D. Cvetkovic, I. Pevac, Man-machine theorem proving in graph theory, Artificial Intelligence 35(1):1-24, May 1988.

[Cybulka 1985] J. Cybulka, J. Bartoszek, The proof checking component for the Pleats programming system enabling specification of theories, Proc. Intl. Spring School, Mathematical Methods of Specification and Synthesis of Software Systems '85 (Wendisch-Rietz, GDR, April 1985), ed. W. Bibel and K.P. Jantke, LNCS 215 Springer-Verlag, Berlin, 1985, pp. 149-155.

[Cyrluk 1987] D.A. Cyrluk, D. Kapur, J. Mundy, V. Nguyen, Formation of partial 3D models from 2D projections - An application of algebraic reasoning, Proc. DARPA Workshop on Image Understanding, Los Angeles, CA, February 1987, pp. 798-809.

*[Cyrluk 1988] D.A. Cyrluk, R.M. Harris, D. Kapur, GEOMETER: A theorem prover for algebraic geometry, 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. 770-771.

*[Czapor 1986] S.R. Czapor, K.O. Geddes, On implementing Buchberger's algorithm for Grobner bases, 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. 233-238.

*[Czapor 1987] S.R. Czapor, Solving algebraic equations via Buchberger's algorithm, 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. 260-269.

[Daalen 1974] D.T. van Daalen, The language theory of AUTOMATH, Proc. Symp. on APL, ed. P. Braffort, Paris, 1974; also PhD dissertation, Technological Univ. of Eindhoven, The Netherlands, 1980.

[Dabija 1981] V. Dabija, On an if-then-else technique for automated theorem proving in propositional calculus, Bul. Inst. Politeh. 'Gheorghe Gheorghiu-Dej' Bucuresti 43(2):95-100, Rumania, June 1981.

*[Dafa 1992] L. Dafa, A natural deduction automated theorem proving system, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 668-672.

[Darlington 1962] J.L. Darlington, A Comit program for Davis-Putnam algorithm, Research Lab. Electron. Mech. Translation Group, MIT, 1962.

[Darlington 1964] J.L. Darlington, Translating ordinary language into symbolic logic, MAC-M-149, MIT, Cambridge, MA, March 1964.

[Darlington 1965] J.L. Darlington, Machine methods for proving logical arguments expressed in English, Mech. Transl. 8(1965):41-67.

[Darlington 1968a] J.L. Darlington, Some theorem-proving strategies based on the resolution principal, Machine Intelligence 2. ed. Dale and Michie, American Elsevier, NY, 1968, pp. 57-71.

[Darlington 1968b] J. Darlington, Automatic theorem-proving with equality substitutions and mathematical induction, Machine Intelligence 3, ed. Dale and Michie, Oliver and Boyd, Edinburgh, 1968, pp. 113-127.

[Darlington 1969a] J.L. Darlington, Theorem proving and information retrieval, Machine Intelligence 4, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1969, pp. 173-181.

[Darlington 1969b] J.L. Darlington, Theorem provers as question answerers, Proc. 1st IJCAI, Washington, D.C., May 1969, p. 317.

[Darlington 1971] J.L. Darlington, A partial mechanization of second-order logic, Machine Intelligence 6, ed. B. Meltzer and D. Michie, American Elsevier, NY, 1971, pp. 91-100.

[Darlington 1972] J.L. Darlington, Deductive plan formation in higher-order logic, Machine Intelligence 7, ed. B. Meltzer and D. Michie, Univ. of Edinburgh Press, 1972, pp. 129-137.

[Darlington 1977] J.L. Darlington, Improving the efficiency of higher order unification, Proc. 5th IJCAI, MIT, Cambridge, MA, 1977, pp. 520-525.

[Darlington 1978] J.L. Darlington, Connection graphs and fact nets, Intl. Rep., GMD Bonn, I.S.T., 1978.

[Darlington 1979] J.L. Darlington, A net based theorem proving procedure for program verification and synthesis, 4th Workshop on Artificial Intelligence, Bad Honnef, 1979.

*[Darlington 1989] J. Darlington, Y.-k. Guo, Narrowing and unification in functional programming---an evaluation mechanism for absolute set abstraction, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 92-108.

[Dassow ] J. Dassow, Comparison of some types of regulated rewriting, Proc. Math. Soc. (Janos Bolyai), in Algebra, Combinatorics and Logic in Computer Science, Vol. I, II (Gyor, Hungary, 1983), Vol. 42, North-Holland, Amsterdam-New York, 1986, pp. 301-313.

[Dauchet 1985] M. Dauchet, S. Tison, Decidability of confluence for ground term rewriting systems, Proc. Fundamentals of Computation Theory - FCT '85 (Cottbus, GDR, September 1985), ed. L. Budach, LNCS 199, Springer-Verlag, Berlin, pp. 80-89.

[Dauchet 1987b] M. Dauchet, S. Tison, T. Heuillard, P. Lescanne, Decidability of the confluence of ground term rewriting systems, Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca, NY, 22-25 June 1987, pp. 353-359.

[Dauchet 1987c] M. Dauchet, F. De Comite, A gap between linear and non-linear term-rewriting systems, 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. 95-104.

[Dauchet 1988] M. Dauchet, Termination of rewriting is undecidable in the one-rule case, Proc. 13th Mathematical Foundations of Computer Science, Carlsbad, CSSR, LNCS 324, Springer-Verlag, September 1988, pp. 262-270.

*[Dauchet 1989a] M. Dauchet, Simulation of Turing machines by a left-linear rewrite rule, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 109-120.

*[Dauchet 1989b] M. Dauchet, A. Deruyver, Compilation of ground term rewriting systems and applications, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 556-558.

*[Dauchet 1990] M. Dauchet, S. Tison, The theory of ground rewrite systems is decidable, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 242-248.

[Davies 1987] T.R. Davies, S.J. Russell, A logical approach to reasoning by analogy, In Proc. 10th IJCAI, 1987.

[Davis 1957] M. Davis, A computer program for Presburger's algorithm, Summer Inst. for Symbolic Logic, Cornell Univ., 1957, pp. 215-233; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 41-48.

[Davis 1958] M. Davis, Computability and Unsolvability, McGraw Hill, 1958.

[Davis 1959] M. Davis, H. Putnam, A computational proof procedure, AFOSR TR 59-124, Rensselaer PolyTech. Institution, Troy, NY, 1959.

[Davis 1960a] M. Davis, H. Putnam, A computing procedure for quantification theory, JACM 7(3):201-215, 1960; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 125-139.

[Davis 1960b] M. Davis, A computer program for Presburger's procedure, Summaries of talks presented at the Summer Institute for Symbolic Logic, Institute for Defense Analysis, Princeton, NJ, 1960.

[Davis 1962] M. Davis, G. Logemann, D. Loveland, A machine program for theorem proving, CACM 5(July 1962):394-397; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 267-270.

[Davis 1963] M. Davis, Eliminating the irrelevant from mechanical proofs, In Experimental Arithmetic, High Speed Computing and Mathematics, Proc. Symp. Applied Mathematics, vol. XV, Providence, RI, 1963, pp. 15-30; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 315-330.

[Davis 1968] M. Davis, Invited commentary on new directions in mechanical theorem-proving, Proc. IFIP Congress 1968, Vol. 1, North-Holland, Amsterdam, 1968, pp. 67-68.

[Davis 1973] M. Davis, Hilbert's tenth problem is unsolvable, Amer. Math. Monthly 80(3):233-269, 1973.

[Davis 1979a] M. Davis, J.T. Schwartz, Metamathematical extensibility for theorem verifiers and proof-checkers, Computers and Mathematics with Applications 5(3):217-230, 1979; also Courant Computer Science Report 12, Courant Institute of Mathematical Sciences, NY, 1977.

[Davis 1979b] M. Davis, The prehistory of Automated Deduction, Invited Lecture, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 1-28.

[Davis 1980a] M. Davis, Obvious logical inferences, Proc. Natl Conf. on Artificial Intelligence, 1980; also Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, August 1981, pp. 530-531.

[Davis 1980b] R. Davis, Meta-rules: reasoning about control, Artificial Intelligence 15(1980):179-222.

[Davis 1982] R. Davis, D. Lenat, Knowledge-Based Systems in Artificial Intelligence, McGraw-Hill, NY, 1982.

[Davis 1983] M. Davis, The prehistory and early history of automated deduction, in Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983.

[Davydov 1973] G.V. Davydov, Synthesis of the resolution method with the inverse method, J. Soviet Mathematics 1:12-18, 1973.

[Davydov 1983] G.V. Davydov, S.Yu. Maslov, G.E. Mints, V.P. Orevkov, A.O. Slisenko, A computer algorithm for the determination of deducibility on the basis of the inverse method, in Automation Of Reasoning - Classical Papers On Computational Logic, Vol. II, 1967-1970, ed. J. Siekmann And G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 531-541.

[Dawson 1969] D. Dawson, A note on the feasibility of the Davis/Putnam procedure to elementary theory, MIT, Memo 40, Cambridge, MA, 1969.

[Degano 1980] P. Degano, J. Castaing, Y. Kodratoff, Inductive hypothesis extracted from proof traces, Atti AICA 80(1980):114-116.

[Degano 1985] P. Degano, F. Sirovich, An evaluation based theorem prover, IEEE Transactions of Pattern Analysis and Machine Intelligence PAMI-7(1):70-79, January 1985.

[deGroote 1987] P. deGroote, How I spent my time in Cambridge with Isabelle, Tech. Report RR 87-1, Universite Catholique de Louvain, January 1987.

[Degtyarev 1986] A.I. Degtyarev, A.A. Voronkov, Equality control methods in machine theorem proving, Cybernetics 3(22):298-307, May-June 1986.

[Degtyarev 1986a] A.I. Degtyarev, A.A. Voronkov, Methods of control of equality in mechanical proofs of theorems, Kibernetika (Kiev) 3:34-41, 1986.

[Degtyarev 1986b] A.I. Degtyarev, A.A. Voronkov, Control equality methods in mechanical proofs of theorems, Cybernetics 22(3):298-307, May-June 1986.

*[Delahaye 1987] J.-P. Delahaye, Formal methods in artificial intelligence, Translated by J. Howlett, North Oxford Academic Publishers Ltd., London, 1987.

[Delcher 1988] A.L. Delcher, S. Kasif, Efficient parallel term matching, Computer Science Department, The Johns Hopkins Univ., Baltimore, MB 21218, 1988.

*[Delcher 1990] A.L. Delcher, S. Kasif, Efficient parallel term matching and anti-unification, Logic Programming: Proc. of the 7th Intl. Conf. (ed. D.H.D. Warren and P. Szeredi, MIT Press, 1990, pp. 355-369. [Deliyanni 1979] A. Deliyanni, R.A. Kowalski, Logic and semantic networks, CACM 22(3):184-192, March 1979.

*[Demoen 1989] B. Demoen, A. Marien, A. Callebaut, Indexing Prolog clauses, Logic Programming: Proc. of the North American Conf., 1989, Vol. 2, ed. E.L. Lusk, R.A. Overbeek, MIT Press, 1989, pp. 1001-1012.

*[Demolombe 1991] R. Demolombe, L. Farinas del Cerro, An inference rule for hypothesis generation, 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. 152-157.

[Denzinger 1987] J. Denzinger and J. Muller, THEOPOGLES user manual, Univ. of Kaiserslautern, 1987.

*[Denzinger 1989] J. Denzinger and J. Muller, EQTHEOPOGLES - A completion theorem prover for PLIEQ, Proc. 13 German Workshop on Artificial Intelligence (GWAI-89, Eringerfeld, 18-22 September 1989), ed. D. Metzing, Springer-Verlag, Berlin, 1989, pp. 92-101.

[Dershowitz 1979a] N. Dershowitz, Z. Manna, Proving termination with multiset orderings, Proc. Intl Colloquium on Automata, Languages and Programming, Graz, July 1979, pp. 188-202; CACM 22(8):465-476, August 1979.

[Dershowitz 1979b] N. Dershowitz, A note on simplification orderings, Information Processing Letters 9(5):212-215, 1979.

[Dershowitz 1979c] N. Dershowitz, Orderings for term rewriting systems, Proc. 20th IEEE Symp. on Foundations of Computer Science, San Juan, Puerto Rico, October 1979, pp. 123-131; also Theoretical Computer Science 17(3):279-301, North-Holland, March 1982.

[Dershowitz 1981] N. Dershowitz, Termination of linear rewriting systems, Proc. 8th Intl. Colloquium on Automata, Languages, and Programming (Acre, Israel, July 1981), ed. O. Kariv and S. Even, LNCS 115, Springer, 1981.

[Dershowitz 1982] N. Dershowitz, L. Marcus, Existence and construction of rewrite systems, Report ATR-82(8478)-3, Information Sciences Research Office, The Aerospace Corporation, El Segundo, CA, 1982.

[Dershowitz 1983a] N. Dershowitz, Computing with rewrite systems, Report no. ATR-83 (8478)-1, Inform. Sci. Research Office, The Aerospace Corporation, El Segundo, CA, 1983; 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. 269-298; also Information and Control 64(2/3):122-157, May/June 1985.

[Dershowitz 1983b] N. Dershowitz, Applications of the Knuth-Bendix completion procedure, Technical Report ATR-83(8478)-2, Aerospace Corp., El Segundo, CA, May 1983.

[Dershowitz 1983c] N. Dershowitz, J. Hsiang, N.A. Josephson, D.A. Plaisted, Associative-commutative rewriting, Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, pp. 940-944.

[Dershowitz 1983d] N. Dershowitz, Well-founded orderings, ATR-83(8478)-3, Information Science Research Office, The Aerospace Corporation, El Segundo, CA., May 1983.

[Dershowitz 1983e] N. Dershowitz, J. Hsiang, Rewrite methods for clausal and non-clausal theorem proving, Proc. ICALP 83, LNCS 154, 1983.

[Dershowitz 1984] N. Dershowitz, Equations as programming language, 4th Jerusalem Conf. on Information Technology, Jerusalem, Israel, May 1984, pp. 114-123,

[Dershowitz 1985a] N. Dershowitz, Termination of rewriting, Report No. UIUCDS-R-85-1220, UILU-ENG-85-1728, Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, Urbana, IL, August 1985, 58 pp.; also Proc. 1st Intl. Conf. on Rewriting Techniques and Applications, Dijon, France, May 1985; also J. of Symbolic Computation 3(1 and 2):69-116, February/April 1987; Corrigendum in 4(3):409-410, December 1987.

[Dershowitz 1985b] N. Dershowitz, L. Marcus, A. Tarlecki, Existence, uniqueness, and construction of rewrite systems, Report ATR-85(8354)-7, Lab. Operations, The Aerospace Corp., El Segundo, CA, 1985; also in SIAM J. Computing 17(4):629-639, 1988.

[Dershowitz 1985c] N. Dershowitz, Termination, rewriting techniques and applications, Proc. Conf. Rewriting Techniques and Applications, LNCS 202, Springer-Verlag, 1985, pp. 180-224.

*[Dershowitz 1988a] N. Dershowitz, M. Okada, Proof-theoretic techniques for term rewriting theory, Proc. 3rd Annual Symp. on Logic in Computer Science (Edinburgh, Scotland, 5-8 July 1988), IEEE, 1988, pp. 104-111.

*[Dershowitz 1988b] N. Dershowitz, M. Okada, G. Sivakumar, Canonical conditional rewrite systems, 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. 538-549.

*[Dershowitz 1988c] N. Dershowitz, G. Sivakumar, Goal-directed equation solving, Proc. AAAI-88, 7th National Conf. on Artificial Intelligence, Vol. 1, St. Paul, Minnesota, 21-26 August 1988, pp. 166-170.

*[Dershowitz 1988d] N. Dershowitz, D.A. Plaisted, Equational programming, in Machine Intelligence 11: Logic and the acquisition of knowledge, ed. Hayes, Michie and Richards, Clarendon Press, Oxford, 1988, pp. 21-56.

*[Dershowitz 1988e] N. Dershowitz, M. Okada, G. Sivakumar, Confluence of conditional rewrite systems, 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. 31-44.

*[Dershowitz 1988f] N. Dershowitz, G. Sivakumar, Solving goals in equational language, 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. 45-55.

*[Dershowitz 1989a] N. Dershowitz, S. Kaplan, Rewrite, rewrite, rewrite,..., Proc. 16th Annual ACM Symp. on Principles of Programming (POPL-89, Austin, Texas, 11-13 January 1989), ACM, NY, 1989.

*[Dershowitz 1989b] N. Dershowitz, ed., Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), Springer-Verlag, NY, 1989.

*[Dershowitz 1989c] N. Dershowitz, Completion and its applications, 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. 31-85.

*[Dershowitz 1990a] N. Dershowitz, E. Pinchover, Inductive synthesis of equational programs, Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990), AAAI Press/MIT Press, 1990, pp. 234-239.

*[Dershowitz 1990b] N. Dershowitz, J. Jouannaud, Rewrite systems, In Handbook of Theoretical Computer Science, Vol. B: Formal Methods and Semantics, chap. 6, ed. J. Van Leeuwen, Elsevier Science Publishers, Amsterdam, and The MIT Press, Cambridge, 1990, pp. 243-320; also available as Rapport 478, LRI, Univ. Paris-Sud, France.

[Dershowitz 1990c] N. Dershowitz, M. Okada, A rationale for conditional equational rewriting, Theoret. Comput. Sci. 75(1/2):111-137, 1990.

[Dershowitz 1991a] N. Dershowitz, S. Kaplan, D.A. Plaisted, Rewrite, rewrite, rewrite, rewrite, rewrite, ... Theor. Comput. Sci. 83(1):71-96, June 1991.

[Dershowitz 1991b] N. Dershowitz, Ordering-based strategies for Horn clauses, 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. 118-124.

[Dershowitz 1991c] N. Dershowitz, J.-P. Jouannaud, Notations for rewriting, In EATACS Bulletin, pp. 162-172, 1991.

*[Dershowitz 1992] N. Dershowitz, S. Mitra, G. Sivakumar, Decidable matching for convergent systems, Proc. 11th Intl. Conf. on Automated Deduction (CADE-11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607, Springer-Verlag, Berlin, 1992, pp. 589-602.

[Desimone 1987] R. Desimone, Explanation-based learning of proof plans, Research paper 304, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1987; also in Machine and Human Learning, ed. Y. Kodratoff, Ellis Horwood, 1987; previous version in Proc. EWSL-86.

[Despeyroux 1988] J. Despeyroux, Theo: An interactive proof development system, No. 887, INRIA, August 1988.

[Detlefs 1985] D. Detlefs, R. Forgaard, A procedure for automatically proving the termination of a set of rewrite rules, Proc. 1st Conf. Rewriting Techniques and Applications (Dijon, France, 20-22 May 1985), ed. J.P. Jouannaud, LNCS 202, Springer-Verlag, Berlin, 1985, pp. 255-270.

[Devienne 1990] P. Devienne, Weighted graphs: a tool for studying the halting problem and time complexity in term rewriting systems and logic programming, J. Theoretical Computer Science 75(1990):157-215.

[Dick 1984] A.J.J. Dick, Automated equational reasoning and the Knuth-Bendix algorithm: an informal introduction, Research Report DoC 84/21, Imperial College, London, March 1984.

*[Dick 1985] A.J.J. Dick, ERIL - Equational reasoning: an interactive laboratory (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. 400-401; also Report No. RAL86010, Rutherford Appleton Laboratory, Chilton, Didcot OX11 0QX, UK, 1986.

[Dick 1986] A.J.J. Dick, R.J. Cunningham, Using narrowing to do isolation in symbolic equation solving - an experiment in automated reasoning, 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. 272-280.

[Dick 1988a] A.J.J. Dick, Order-sorted equational reasoning and rewrite systems, PhD. thesis, Dept. of Computing, Imperial College, London, 1988.

[Dick 1988b] A.J.J. Dick, J.R. Kalmus, ERIL Users Manual, Version R1.6A, Report RAL-88-055, Rutherford Appleton Laboratory, Chilton, September 1988.

[Dick 1990] J. Dick, J. Kalmus, U. Martin, Automating the Knuth Bendix ordering, Acta Inf. 28(2):95-119, December 1990.

*[Dick 1991] A.J.J. Dick, An introduction to Knuth-Bendix Completion, The Computer Journal 34(1):2-15, February 1991.

*[Dick 1991a] A.J.J. Dick, P. Watson, Order-sorted term rewriting, The Computer Journal 34(1):16-19, February 1991.

[Dick 1991b] A.J. Dick, An introduction to Knuth-Bendix completion, Comput. J. 34(1):2-15, February 1991. Special issue on term rewriting.

*[Diekert 1987] V. Diekert, On the Knuth-Bendix completion for concurrent processes, Proc. 14th Intl. Colloquium on Automata, Languages, and Programming (ICALP '87, Karlsruhe, W. Germany, 13-17 July 1987), ed. T. Ottmann, LNCS 267, Springer-Verlag, Berlin, pp. 42-53.

*[Diesen 1989] D. Diesen, Lifting of the ditchmarker refinement for connection method to first order logic, Proc. Scandinavian Conf. on Artificial Intelligence (SCAI '88, Tromso, Norway, 9-11 March 1988), ed. T. Danielsen, IOS, Amsterdam, Netherlands, 1988, pp. 13-21.

[Dietrich 1985] R. Dietrich, Relating resolution and algebraic completion for Horn logic, Arbeitspapiere der GMD Nr. 177, Gesellschaft fur Mathematik und Datenverarbeitung mbH, Bonn, 1985; 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. 62-78.

[Digricoli 1979a] V.J. Digricoli, Resolution by unification and equality, Proc. 4th Workshop on Automated Deduction (CADE-4, Austin, Texas, 1-3 February 1979), ed. W.H. Joyner, 1979; also in Courant Institute, New York Univ., February 1983.

[Digricoli 1979b] V.J. Digricoli, Automatic deduction and equality, Proc. National ACM Conf., Detroit, Michigan, October 1979, pp. 240-250.

[Digricoli 1980] V.J. Digricoli, First experiments with RUE automated deduction, Proc. 1st Natl Conf. on Artificial Intelligence, Stanford Univ., August 1980, pp. 96-98.

[Digricoli 1981] V.J. Digricoli, The efficiency of RUE resolution, experimental results and heuristic theory, Proc. 7th IJCAI, Univ. of British Columbia, Vancouver, August 1981, pp. 539-547.

[Digricoli 1985] V.J. Digricoli, The management of heuristic search in boolean experiments with RUE resolution, Proc. 9th IJCAI, Los Angeles, CA, 1985, pp. 1156-1161.

*[Digricoli 1986] V.J. Digricoli and M.C. Harrison, Equality-based binary resolution, JACM 33(2):253-289, April 1986.

*[Digricoli 1989] V.J. Digricoli, J.J. Lu, V.S. Subrahmanian, And-or graphs applied to RUE resolution, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 354-358.

*[Digricoli 1992] V.J. Digricoli, E. Kochendorfer, LIM+ challenge problems by RUE hyper-resolution, 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. 239-252.

[Dilger 1984a] W. Dilger, and H-A. Schneider, ASSIP-T: A theorem proving machine, Proc. Intl. Conf. on 5th Generation Computer Systems, Tokio, 1984, pp. 497-506; also Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, August 1985, pp. 1194-1200.

[Dilger 1984b] W. Dilger, A. Janson, A unification graph with constraints for intelligent backtracking in deduction systems, Interner Bericht 100/84, Fachbereich Informatik, Universitat Kaiserslautern 1984.

[Dilger 1985] W. Dilger, and H-A. Schneider, A theorem proving associative processor, Interner Bericht 145/85, Fachbereich Informatik, Universitat Kaiserslautern, 1985.

[Dilger 1986] W. Dilger, A. Janson, Intelligent backtracking in deduction systems by means of extended unification graphs, J. of Automated Reasoning 2(1):43-62, D. Reidel Publ. Co., Dordrecht, Holland, 1986.

[Dincbas 1987a] M. Dincbas, P. Van Hentenryck, Extended unification algorithms for the integration of functional programming into logic programming, J. of Logic Programming (to appear), 1987.

*[Dincbas 1987b] M. Dincbas, H. Simonis, P. Van Hentenryck, Extending equation solving and constraint handling in logic programming, In: Resolution of Equations in Algebraic Structures: Vol 2, Rewriting Techniques, ed. H. Ait-Kaci, M. Nivat, Academic Press, Inc., San Diego, 1989, pp. 87-115.

*[Dincbas 1988] M. Dincbas, et al., The CHIP system: Constraint handling in Prolog, 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. 774-775.

[DiPaola 1973] R.A. DiPaola, The solvability of the decision problem for classes of proper formulas and related results, JACM 20(1):112-126, January 1973.

[Dixon 1970] J. Dixon, An improved method for solving deductive problems on a computer by compiled axioms, PhD thesis, Univ. of California, 1970.

[Dixon 1971] J. Dixon, Experiments with a Z-resolution program, Div. of Comput. Res. and Tech., Nat. Inst. of Health, Bethesda, Maryland, 1971.

[Dixon 1973] J.K. Dixon, Z-resolution: Theorem proving with compiled axioms, JACM 20(1):127-147, January 1973.

[Dobry 1987] T.P. Dobry, A high performance architecture for Prolog, DAI V48(09), SecB, Univ. of California, Berkeley, 1987; also available as Univ. Microfilms Order Number ADG87-26188, Computer Science.

[Doggaz 1991] N. Doggaz, C. Kirchner, Completion for unification, Theor. Comput. Sci. 85(2):231-251, August 1991.

[Donat 1987] M.R. Donat, Construction and application of generalisations using higher order unification, Master's thesis, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1987.

*[Donat 1988] M.R. Donat, L.A. Wallen, Learning and applying generalised solutions using higher order resolution, 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. 41-60.

*[Dorre 1990] J. Dorre, W.C. Rounds, On subsumption and semiunification in feature algebras, Proc. 5th Annual IEEE Symp. on Logic Computer Science (Philadelphia, PA, 4-7 June 1990), IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 300-310.

*[Dougherty 1990] D.J. Dougherty, P. Johann, An improved general E-unification method, 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. 261-275.

*[Dougherty 1992] D.J. Dougherty, P. Johann, A combinatory logic approach to higher-order E-unification, 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. 79-93.

[Dowling 1984] W.F. Dowling, J.H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. of Logic Programming 3:267-284, 1984.

[Downey 1978] P.J. Downey, H. Samet, R. Sethi, Off-line and on-line algorithms for deducing equalities, POPL-5, Tucson, Arizona, 1978.

[Downey 1980] P.J. Downey, R. Sethi, R.E. Tarjan, Variations on the common subexpression problem, JACM 27(4):758-771, October 1980.

[Doyle 1979] J. Doyle, A truth maintenance system, Artificial Intelligence 12(1979):231-272.

[Dreben 1957] B. Dreben, Systematic treatment of the decision problem, Talks at Summer Institute of Symbolic Logic, Cornell Univ., pp. 363, 1957.

[Dreben 1964] B. Dreben, H. Wang, A refutation procedure and its model-theoretic justification, Harvard Univ., Cambridge, MA, 1964.

[Dreben 1979] B. Dreben, W.D. Goldfarb, The Decision Problem - Solvable Classes of Quantificational Formulas. Addison-Wesley Publ. Co., 1979.

[Drosten 1983] K. Drosten, Toward executable specifications using conditional axioms, Rept. 83-01, Tech. Univ. Braunschweig, W. Germany, 1983.

[Drosten 1985] K. Drosten, Term rewriting systems with restricted variables, Bericht Nr. 85-11, Institut fur Informatik, Braunschweig, 1985.

*[Duchier 1988] D. Duchier, D. McDermott, LOGICALC: An environment for interactive proof development, 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. 121-130.

[Duda 1978] R.O. Duda, P.E. Hart, N.J. Nilsson, G.L. Sutherland, Semantic network representations in rule-based inference systems, in Pattern-Directed Inference Systems, ed. Waterman and Hayes-Roth, Academic Press, NY, 1978, pp. 203-221.

[Duffy 1989a] D.A. Duffy, A general principle of inductionless induction, Internal report, Univ. of Strathclyde, 1989.

[Duffy 1989b] D.A. Duffy, An alternative to an abstract syntax for proofs, PROSPECTRA report S.3.4-SN-18.0, Univ. of Strathclyde, 1989.

*[Duffy 1991] D.A. Duffy, Principles of Automated Theorem Proving, John Wiley & Sons Ltd., Chichester, England, 1991.

*[Dumant 1992] B. Dumant, Checking the soundness of resolution schemes, Proc. Joint Intl. Conf. and Symp. on Logic Programming, ed. K. Apt, The MIT Press, Cambridge, MA, 1992, pp. 37-51.

[Dunham 1959] B. Dunham, R. Fridshal, G.L. Sward, A nonheuristic program for proving elementary logical theorems, Proc. IFIP Congr. 1959, pp. 282-285; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 93-98.

[Dunham 1962] B. Dunham, R. Fridshal, J.H. North, Exploratory mathematics by machine, Information and Decision Processes, ed. R.E. Machol and P. Grey, Macmillan, NY, 1962; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 276-287.

[Dunham 1963] B. Dunham, J. North, Theorem testing by computer, Proc. Symp. Math. Theory Automata, Polytechnic Press, Brooklyn, NY, 1963, pp. 173-177; also Automation of Reasoning - Classical Papers on Computational Logic, Vol. I, 1957-1966, ed. J. Siekmann and G. Wrightson, Springer-Verlag, Berlin, 1983, pp. 271-275.

[Dunham 1976] B. Dunham, H. Wang, Towards feasible solutions of the tautology problem, Annals of Math. Logic 10(1976):117-154.

*[Dwork 1984] C. Dwork, P. Kanellakis, P. Mitchell, On the sequential nature of unification, J. of Logic Programming 1(1):35-50, June 1984; also Tech. Report CS-83-26, Brown Univ.

[Dwork 1986] C. Dwork, P. Kanellakis, L. Stockmeyer, Parallel algorithms for term matching, 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. 416-430; also SIAM J. of Computing 17(4):711-731, August 1988.

[Echahed 1988] R. Echahed, On completeness of narrowing strategies, Proc. CAAP '88, LNCS 299, Springer-Verlag, 1988, pp. 89-101.

[Eder 1976] A Prolog-like interpreter for non-Horn clauses, Tech. Rep., Dept. Artif. Intell., Univ. Edingburgh, Scotland.

[Eder 1983] E. Eder, Properties of substitutions and unifications, Projekt Beweisverfahren, Inst. fur Inf., Technische Universitat Munchen, Report ATP-17-1-83, 1983; also Proc. GWAI-83, 7th German Workshop on Artificial Intelligence, Dassel/Solling (September 1983), in Informatik-Fachberichte 76, Springer-Verlag, Berlin, 1983, pp. 197-206; also J. of Symbolic Computation 1(1):31-46, March 1985.

*[Eder 1984] E. Eder, An implementation of a theorem prover based on the connection method, Proc. Intl. Conf. on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'84, Varna, Bulgaria, 17-20 September 1984), ed. W. Bibel and B. Petkoff, North-Holland, Amsterdam, 1985, pp. 121-128.

[Eder 1989] E. Eder, A comparison of the resolution calculus and the conncection method, and a new calculus generalizing both methods, Proc. CSL `88, 2nd Workshop on Computer Science Logic (Duisburg, FRG, October 1988), ed. E. Borger, H. Kleine Buning, and M.M. Richter, LNCS 385, Springer-Verlag, Berlin, 1989, pp. 80-98.

*[Eder 1991] E. Eder, Consolution and its relations with resolution, 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. 132-136.

[Edgar 1991] Edgar, A.; and F.J. Pelletier, Natural Language Generation from Natural Deduction Proofs, in Proceedings of the First PACLING Conference (Vancouver, Simon Fraser Univ.), 1991, pp.269-278. (source: F.J. Pelletier)

[Eekelen 1987] M. van Eekelen, R. Plasmeijer, Specifications of reduction strategies in term rewriting systems, Proc. of the Graph Reduction Workshop, ed. J.H. Fasel and R.M. Keller, LNCS 279, Springer-Verlag, 1987, pp. 215-239.

*[Egly 1992] U. Egly, A simple proof for the pigeonhole formulae, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 3-7 August 1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992, pp. 70-71.

[Eichenlaub 1988] C. Eichenlaub, J. Hook, Preliminary manual for theory manager interface, internal report, Odyssey Research Associates, Ithaca, NY, July 1988.

*[Eichenlaub 1990] C. Eichenlaub, B. Esrig, J. Hook, C. Klapper, G. Pottinger, The Romulus proof checker (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. 651-652.

[Eisinger 1981] N. Eisinger, Subsumption and connection graphs, Proc. GWAI-81, Informatik-Fachberichte 47, ed. Siekmann, Springer-Verlag, Berlin, 1981, pp. 188-198; also Proc. 7th IJCAI, Vancouver, Canada, 1981, pp. 480-486.

[Eisinger 1983] N. Eisinger, M. Weigele, A technical note on splitting and clausal form algorithms, Proc. GWAI-83, 7th German Workshop on Artificial Intelligence, Dassel/Solling (September 1983), Informatik-Fachberichte 76, Springer-Verlag, Berlin, 1983, pp. 225-232.

[Eisinger 1986a] N. Eisinger, What you always wanted to know about clause graph 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. 316-336.

[Eisinger 1986b] N. Eisinger, H.J. Ohlbach, The Markgraf Karl Refutation Procedure (MKRP), 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. 681-682.

*[Eisinger 1988] N. Eisinger, Completeness, confluence, and related properties of clause graph resolution, PhD thesis, SEKI Report SR-88-07, Universitat Kaiserslautern, 1988; also published by Pitman, London, and Morgan Kaufmann Publishers, Inc., San Mateo, CA, 1991.

[Eisinger 1989] N. Eisinger, H.J. Ohlbach, A. Pracklein, Elimination of redundancies in clause set and clause graphs, SEKI Report SR-89-10, Universitat Kaiserslautern, 1989.

[Elcock 1982] E.W. Elcock, Goal selection strategies in Horn clause programming, Canadian Society of Computational Studies of Intelligence, Proc. CSCSI/SCEIO Conf. 1982, Univ. of Saskatchewan, Saskatoon, Saskatchewan, May 17-19, 1982, pp. 121-124.

*[Elkan 1989] C. Elkan, Conspiracy numbers and caching for searching and/or trees and theorem-proving, Proc. 11th IJCAI (Detroit, Michigan, USA, 20-25 August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 341-346.

*[Elliot 1989] C. M. Elliott, Higher-order unification with dependent function types, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications (Chapel Hill, North Carolina, 3-5 April 1989), ed. N. Dershowitz, Springer-Verlag, NY, 1989, pp. 121-136.

[Emden 1982] M.H. van Emden, An interpreting algorithm for Prolog programs, 1st Intl. Logic Programming Conf., Univ. of Marseille, 1982, also reprinted in Implementations of Prolog, ed. J.A. Campbell, Ellis Horwood, Chishester, England, 1984, pp. 87-92.

[Emerson 1984] E.A. Emerson, A.P. Sistla, Deciding full branching time logic, Information and Control 61(1984):175-201.

[Emerson 1985a] E.A. Emerson, Automata, tableaux and temporal logics, LNCS 193, 1985, pp. 79-87.

[Emerson 1985b] E.A. Emerson, J.Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, J. Computer and System Sciences 30(1985):1-24.

[Engelhardt 1987] D. Engelhardt, Model elimination - Grundlagen und implementation, Diplomarbeit, Tech. Hochschule Darmstadt, Fachbereich Informatik, 1987.

[Enjalbert 1986] P. Enjalbert, L. Farinas, Modal resolution in clausal form, Report No. RG 14-86, Greco de Programmation, Universite de Bordeaux I, France, 1986; also Theoretical Computer Science 65(1989):1-33. [Erickson 1980] R.W. Erickson, D.R. Musser, The AFFIRM theorem prover: Proof forests and management of large proofs, 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. 220-231.

[Erni 1981] W. Erni, R. Lapsien, On the time and tape complexity of weak unification, Information Processing Letters 12(3):146-150, June 1981.

[Ernst 1967] G.W. Ernst, A. Newell, Some issues of representation in a general problem solver, AFIPS Conf. Proc. 30(1967):583-600.

[Ernst 1970] G.W. Ernst, GPS and decision making: An overview, Theoretical Approaches to Non-Numerical Problem Solving, ed. Banerji, Berlin-Munchen-Heidelberg, 1970.

[Ernst 1971] G.W. Ernst, The utility of independent subgoals in theorem proving, Information and Control 18(April 1971):237-252.

[Ernst 1973] G.W. Ernst, A definition-driven theorem prover, Rep. 1124, Dept. Computer. and Inform. Sci., Case Western Reserve Univ., Cleveland, OH, 1973; also Proc. 3rd IJCAI, Stanford Univ., 1973, pp. 51-55; also IEEE Trans. on Computers C-25(4):317-322, April 1976.

[Ernst 1982] G.W. Ernst, R.J. Hooknay, Mechanical theorem proving in the CASE verifier, Machine Intelligence 10, ed. Hayes, Michie and Pao, Ellis Harwood Ltd., Chichester, 1982.

[Ertel 1989] W. Ertel, J. Schumann, and C.B. Suttner, Learning heuristics for a theorem prover using back propagation, Proc. of the 5. OGAI-Conf., Igls, Austria, Springer, 1989.

*[Escalada-Imaz 1988] G. Escalada-Imaz, M. Ghallab, A practically efficient and almost linear unification algorithm (research note), Artificial Intelligence 36(2):249-263, September 1988.

[Evans 1951] T. Evans, On multiplicative systems defined by generators and relations, I, Proc. of the Cambridge Philosophical Society 47, pp. 637-649, 1951.

[Evans 1968] T.G. Evans, A heuristic program to solve geometry analogy problems, Semantic Inform. Proc., ed. Minsky, MIT Press, 1968.


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