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, SpringerVerlag, Berlin, 1982, pp. 309325.
[Caferra 1984] R. Caferra, E. Eder, B. Frohoefer, W. Bibel,
Extension of PROLOG through matrix reduction, ECAI84, ed. T.
O'Shea, NorthHolland, Amsterdam, 1984, pp. 101104.
*[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 (CADE11, Saratoga
Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes in
Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
385399.
*[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 August3 September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc.,
1993, pp. 7479.
[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,
TR693, 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):549571.
[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):3777.
[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):118, 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):281300.
[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:193230.
*[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, 48
July 1988), ed. P. Gianni, LNCS 358, SpringerVerlag, Berlin,
1989, pp. 407422.
[Cantone 1988c] D. Cantone, S. Ghelfo, E. Omodeo, The automation
of syllogistic. I. Syllogistic normal forms, J. Symbolic
Computation 6(1):8398, 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
settheoretic formulae, Comm. Pure Appl. Math 51(1988):105120.
*[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, 2025 August 1989), ed. N.S.
Sridharan, IJCAI Inc., 1989, pp. 425430.
[Cantone 1989c] D. Cantone, E.G. Omodeo, Topological syllogistic
with continuous and closed functions, Comm. Pure Appl. Math.
42(1989):11751188.
*[Cantone 1990a] D. Cantone, E.G. Omodeo, A. Policriti, The
automation of syllogistic, II. Optimization and complexity issues,
J. of Automated Reasoning 6(2):173187, 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):189201, 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, 2024 August 1990), ACM, NY, NY, 1990, p.
2429.
*[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):193230, 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):231256, 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. 137161.
[Cardelli 1982] L. Cardelli, ML under Unix, Bell Laboratories,
Murray Hill, New Jersey, 1982.
[Cardelli 1986] L. Cardelli, A polymorphic lambdacalculus 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
theoremproving 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, 2025
August 1989), ed. N.S. Sridharan, IJCAI Inc., 1989, pp. 395400.
[Casley 1986] R. Casley, A proof editor for propositional
temporal logic, STANCS861109, 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.
421431.
[Castaing 1985] J. Castaing, How to facilitate the proof of
theorems by using the inductionmatching, and by generalization,
Proc. 9th IJCAI, Vol. 2, Los Angeles, CA, 1823 August 1985, pp.
12081213.
[Catach 1991] L. Catach, TABLEAUX: A general theorem prover for
modal logics, J. Automated Reasoning 7(4):489510, 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 (CADE7, Napa, CA, May 1984), ed. R.E.
Shostak, LNCS 170, SpringerVerlag, NY, 1984, pp. 113127.
[Cavenathi 1987] M. Cavenathi, M. de Zanet, G. Mauri, MCOBJ: 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, CarnegieMellon Univ., 1967; also
JACM 17(2):385396, 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. 8292.
[Champeaux 1979] D. de Champeaux, Subproblem finder and
instance checker  Two cooperating preprocessors for theorem
provers, Proc. 4th Workshop on Automated Deduction (CADE4,
Austin, Texas, 13 February 1979), ed. W.H. Joyner, 1979, pp.
110114; also Proc. 6th IJCAI, Tokyo, 1979, pp. 191196.
[Champeaux 1981a] D. de Champeaux, Challenge problem 1 without
search, ACM SIGART 76, April 1981, pp. 1213.
[Champeaux 1981b] D. Champeaux, B. Domolki, T. Gergely, Other
directions for automatic theorem proving, Mathematical Logic in
Computer Science, NorthHolland, 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. 519527.
[Champeaux 1982] D. de Champeaux, A note on resolution,
connection graphs and subsumption, ACM SIGART Newsletter 81, July
1982, pp. 1517.
[Champeaux 1986a] D. de Champeaux, Subproblem finder and
instance checker, two cooperating modules for theorem provers,
JACM 33(4):633657, October 1986.
[Champeaux 1986b] D. de Champeaux, About the PatersonWegman
linear unification algorithm, J. of Computer and System Sciences
32(1986):7990.
*[Chan 1977] TatHung Chan, An algorithm for checking PL/CV
arithmetic inferences, Tech. Report 77326, Computer Science
Dept., Cornell Univ., October 1977; also In: An Introduction to
the PL/CV2 Programming Logic, ed. Constable, Johnson and
Eichenlaub, LNCS 135, SpringerVerlag, Berlin, 1982, Appendix D,
pp. 227264.
[Chandru 1991] V. Chandru, J.N. Hooker, Extended Horn sets in
propositional logic, JACM 38(1):205221, January 1991.
[Chang 1970a] C. Chang, The unit proof and the input proof in
theorem proving, JACM 17(October 1970):698707; also Automation Of
Reasoning  Classical Papers On Computational Logic, Vol. II,
19671970, ed. J. Siekmann And G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 331341.
[Chang 1970b] C. Chang., Renamable paramodulation for automatic
theorem proving with equality, Artificial Intelligence 1(Winter
1970):47256.
[Chang 1970c] C.L. Chang, R.C.T. Lee, J.R. Slagle, A new
algorithm for generating prime implicants, IEEE Trans. on
Computers C19(4):304310, 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):125136.
[Chang 1971b] C.L. Chang, Theorem proving by generation of
Pseudosemantic trees, Div. of Computer Res. and Tech. Nat. Inst.
of Health, Bethesda, Maryland, 1971.
[Chang 1972a] C.L. Chang, Theorem proving with
variableconstrained resolution, Information Sci. 4(1972):217231.
[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. 2028.
[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):715, March 1973.
[Chang 1979a] C.L. Chang, J.R. Slagle, Using rewriting rules for
connection graphs to prove theorems, Artificial Intelligence
12(2):159180, 1979.
[Chang 1979b] C.L. Chang, Resolution plans in theorem proving,
Proc. 6th IJCAI, Tokyo, August 2023, 1979, pp. 143148.
[Chapman 1985] D. Chapman, Planning for conjunctive goals, Memo
AI802, 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. 101115.
[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):339362,
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 ordersorted calculus: ordersorted unification using compact
representation of clauses, Proc. 8th ECAI, Institut fur Informatik
der Technischen Universitat Munchen, 15 August 1988, pp. 625630.
*[Charniak 1985] E. Charniak, D. McDermott, Introduction to
Artificial Intelligence, AddisonWesley, Reading, MA 1985.
[Chen 1986] T.Y. Chen, J.L. Lassez, G.S. Port, Maximal
unifiable subsets and minimal nonunifiable subsets, New
Generation Computing 4(1986):133152.
*[Chen 1992] W.Z. Chen, Tacticbased theorem proving and
knowledgebased forward chaining: An experiment with Nuprl and
Ontic, 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.
552566.
[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, 1317 July
1987, pp. 1317.
[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
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 4251.
[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. 137160.
[Chester 1976] D. Chester, The translation of formal proofs into
English, Artificial Intelligence 7(3):261278, 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. 108117.
[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. 718.
*[Chi 1988] S. Chi, L.J. Henschen, Recursive query answering
with nonHorn clauses, 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.
294312.
[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 (CADE11,
Saratoga Springs, NY, USA, June 1992), ed. D. Kapur, Lecture Notes
in Artificial Intelligence 607, SpringerVerlag, Berlin, 1992, pp.
711715.
*[Chisholm 1989] G.H. Chisholm, B.T. Smith, A.S. Wojcik, An
automated reasoning problem associated with proving claims about
programs using FloydHoare inductive assertion methods, J.
Automated Reasoning 5(4):533540, December 1989.
*[Cholvy 1993] L. Cholvy, Proving theorems in a multisource
environment, Proc. 13th IJCAI (Chambery, France, 28 August3
September 1993), Vol 1, ed. R. Bajscy, IJCAI, Inc., 1993, pp.
6673.
[Choppy 1985] C. Choppy, C. Johnen, Petrireve: Proving Petri net
properties with rewriting systems, Proc. 1st Conf. Rewriting
Techniques and Applications (Dijon, France, 2022 May 1985), ed.
J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin, 1985, pp.
271286.
[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, 2527 May
1987), ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987,
pp. 256273.
[Choque 1984] G. Choque, How to compute a complete set of
minimal incrementations with the recursive decomposition ordering?
Internal report 84R056, 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):243286.
[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):253273, 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, 1618 June 1986, pp. 187192.
[Chou 1986c] S.C. Chou, GEOProver  A geometry theorem prover
developed at UT, Proc. 8th Intl. Conf. on Automated Deduction
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 679680.
[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):291299, 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):237267, September 1987.
[Chou 1989a] S.C. Chou, S.S. Gao, Mechanical theorem proving
in differential geormetry, TR8908, Dept. of Computer Sciences,
Univ. of Texas at Austin, Texas, March 1989.
*[Chou 1989b] S.C. Chou, X.S. Gao, RittWu's decomposition
algorithm and geometry theorem proving, TR8909, Dept. of
Computer Sciences, Univ. of Texas at Austin, Texas, March 1989;
also 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. 207220.
[Chou 1989c] S.C. Chou, S.S. Gao, Automated reasoning in
mechanics using RittWu's methods, TR8911, 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, TR8937,
Computer Sciences Dept., Univ. of Texas at Austin, November 1989.
[Chou 1989e] S.C. Chou, X.S. Gao,N. McPhee, A combination of
RittWu's method and Collins' method, TR8928, Computer Sciences
Dept., Univ. of Texas at Austin, October 1989.
[Chou 1989f] S.C. Chou, X.S. Gao, Mechanical formula derivation
in elementary geometries, TR8921, 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,
TR8922, 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):237262.
*[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. AitKaci, M. Nivat, Academic Press,
Inc., San Diego, 1989, pp. 3392.
[Chou 1990a] S.C. Chou, X.S. Gao, Techniques for RittWu's
decomposition algorithm, TR902, 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, 2024 August 1990), ACM, NY, NY,
1990, pp. 255260.
*[Chou 1990c] S.C. Chou, Methods for mechanical geometry
formula deriving, Proc. ISSAC '90 (Tokyo, Japan, 2024 August
1990), ACM, NY, NY, 1990, pp. 265270.
*[Chou 1992a] S.C. Chou, X.S. Gao, Proving geometry statements
of constructive type, 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. 2034.
*[Chou 1992b] S.C. Chou, A geometry theorem prover for
Macintoshes, 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. 686690.
*[Chouraqui 1982] E. Chouraqui, Construction of a model for
reasoning by analogy, Proc. ECAI82, Univ. ParisSud, Orsay,
France, 1214 July 1982, pp. 4853.
[Christian 1987] J. Christian, P. Lincoln, Adventures in
associativecommutative unification, MCC Tech. Report
ACAST27587, Microelectronics and Computer Technology Corp.,
Austin, TX, October 1987.
*[Christian 1989a] J. Christian, Fast KnuthBendix commpletion:
summary, Proc. 3rd Intl. Conf. Rewriting Techniques and
Applications (Chapel Hill, North Carolina, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 551555.
[Christian 1989b] J. Christian, High performance permutative
completion, Tech. Report ACTAI30389, MCC, August 1989, PhD
thesis.
*[Christian 1992] J. Christian, Some termination criteria for
narrowing and Enarrowing, 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. 582587.
[Church 1940] A. Church, A formulation of the simple theory of
types, Symbolic Logic 5(1):5668, 1940.
[Church 1951] A. Church, The calculi of lambdaconversion,
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):759768, October 1988.
[Cialdea 1986] M. Cialdea, Some remarks on the possibility of
extending resolution proof procedures to intuitionistic logic,
Information Processing Letters 22(2):8790, 1986.
[Cialdea 1991] M. Cialdea, Resolution for some firstorder modal
systems, Theor. Comput. Sci. 85(2):213229, August 1991.
*[Cichon 1992] A. Cichon, P. Lescanne, Polynomial
interpretations and the complexity of algorithms, 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. 139147.
[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
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 761765.
[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):201216, 1989 (special issue on unification, part 2).
[Cline 1989] M.P. Cline, A fast parallel algorithm for Nary
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, SpringerVerlag, NY, 1981.
[Cochet 1976] Y. Cochet, ChurchRosser congruences on free
semigroups, Coll. Math. Soc. Janos Bolyai: Algebraic Theory of
Semigroups 20(1976): 5160.
[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):329390, 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
2325), ed. S.R. Petrick, ACM, NY, 1971, pp. 268280.
[Cohen 1974] J. Cohen, L. Trilling, P. Wegner, A nucleus of a
theoremprover described in ALGOL68, 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. 75124.
[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 (CADE4, Austin, Texas, 13
February 1979), ed. W.H. Joyner, 1979, pp. 7380.
[Cohn 1981] A. Cohn, The equivalence of two semantic
definitions: A case study in LCF, Report CSR7681, 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,
CSR11382, 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. 8487.
[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 manysorted logic, Proc. 9th IJCAI, Vol. 2, Los Angeles, CA,
1823 August 1985, W. Kaufmann, Inc., pp. 11691174.
[Cohn 1987] A.G. Cohn, A more expressive formulation of many
sorted logic, J. of Automated Reasoning 3(2):113200, June 1987.
*[Cohn 1989a] A. Cohn, The notion of proof in hardware
verification, J. of Automated Reasoning 5(2):127139, 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. 5566.
*[Cohn 1992] A.G. Cohn, A many sorted logic with possibly empty
sorts, 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.
633647.
[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):95104.
[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. 8599.
*[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. 6781.
[Comon 1986] H. Comon, Sufficient completeness, term rewriting
systems and "antiunification", Proc. 8th Intl. Conf. on
Automated Deduction (CADE8, Oxford, England, July 27August 1,
1986), ed. J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986,
pp. 128140.
[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, 35 April 1989), ed. N.
Dershowitz, SpringerVerlag, NY, 1989, pp. 7691.
*[Comon 1990] H. Comon, Solving inequations in term algebras,
Proc. 5th Annual IEEE Symp. on Logic Computer Science
(Philadelphia, PA, 47 June 1990), IEEE Computer Society Press,
Los Alamitos, CA, 1990, pp. 6269.
*[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 (AAAI90, July 29August 3, 1990), AAAI
Press/MIT Press, 1990, pp. 7885.
[Constable 1971] R.L. Constable, Constructive mathematics and
automatic programs writers, Proc. IFIP congress, Ljubljana, 1971,
pp. 229233.
[Constable 1977] R.L. Constable, A constructive programming
logic, Information Processing 77, NY: NorthHolland, 1977, pp.
733738.
[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,
SpringerVerlag, 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):105112, 1983.
[Constable 1983c] R.L. Constable, J.L. Bates, The nearly
ultimate PRL, TR83551, 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):285326, 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):113136, 1985.
[Constable 1985c] R.L. Constable, Constructive mathematics as a
programming logic I: some principles of theory, Annuals of
Discrete Math. 24(1985):2138.
[Constable 1985d] R.L. Constable, N.P. Mendler, Recursive
definitions in type theory, Proc. Logics of Programs Conf., LNCS,
SpringerVerlag, NY, 1985, pp. 6678.
*[Constable 1986] R. Constable, et al., Implementing Mathematics
with the Nuprl Proof Development System, PrenticeHall, 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.
4575.
[Cook 1965] S.A. Cook, Algebraic techniques and the
mechanization of number theory, RM4319PR, 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.
151158.
[Cook 1974] S.A. Cook, R.A. Reckhow, On the lengths of proofs in
the propositional calculus, Proc. 6th ACM STOC, 1974, pp. 135148;
Corrections in: ACM SIGACT News 6(3):1522, 1974.
[Cook 1975] S.A. Cook. Feasibility constructive proofs in the
propositional calculus, Proc. 7th Annual ACM Symp. on Th. of
Computing, pp. 8397, 1975. [Cook 1976] S.A. Cook, A short proof
on the Pigeonhole principle using extended resolution, ACM SIGACT
News 8(October  December 1976):2832.
[Cook 1979] S.A. Cook, R.A. Reckhow, The relative efficiency of
propositional proof systems, J. of Symbolic Logic 44(1979):3650.
[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. 2031, 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 nonnumerical computation, ed. Fox,
Pergamon Press, Oxford, 1966, pp. 155182.
[Cooper 1967] D.C. Cooper, Mathematical proofs about computer
programs, Machine Intelligence 1, ed. Collins and Michie, American
Elsevier, NY, 1967, pp. 1730.
[Cooper 1971] D.C. Cooper, Programs for mechanical program
verification, Machine Intelligence 6, ed. B. Meltzer and D.
Michie, American Elsevier, NY, 1971, pp. 4359.
[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. 9199.
*[Cooperman 1986] G. Cooperman, A semantic matcher for computer
algebra, 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.
132134.
[Copi 1959] K. Copi, M. Beard, Programming an idealized general
purpose computer to decide questions of truth and falsehood, Rep.
2144402T, 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, SophiaAntipolis, 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, 13 April
1985), Vol. 1: Invited Lectures, ed. B. Buchberger, LNCS 203,
SpringerVerlag, Berlin, 1985, pp. 151184.
[Coquand 1988] T. Coquand, G. Huet, The calculus of
constructions, Information and Computation 76(1988):95120.
[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. 909914; 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, Metalevel 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. 359373.
[Cosmadakis 1985] S. Cosmadakis, P. Kanellakis, Two applications
of equational theories to data base theory, Proc. 1st Conf.
Rewriting Techniques and Applications (Dijon, France, 2022 May
1985), ed. J.P. Jouannaud, LNCS 202, SpringerVerlag, Berlin,
1985, pp. 107123.
*[Costa 1982] E.J.F. Costa, Weakly commuting term rewriting
systems: application to automatic recursion removal, Proc.
ECAI82, ParisSud, Orsay, France, 1214 July 1982, pp. 8790.
*[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 (CADE10, Kaiserslautern, FRG, July 1990), Lecture Notes
in Artificial Intelligence 449, ed. M.E. Stickel, SpringerVerlag,
Berlin, 1990, pp. 7286.
*[Courcelle 1989] B. Courcelle, On recognizable sets and tree
automata, In: Resolution of Equations in Algebraic Structures: Vol
1, Algebraic Techniques, ed. H. AitKaci, M. Nivat, Academic
Press, Inc., San Diego, 1989, pp. 93126.
[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. 266278.
[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. 2029.
[Cox 1979] P.T. Cox, Representational economy in a mechanical
theorem prover, Proc. 4th Workshop on Automated Deduction (CADE4,
Austin, Texas, 13 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, 811 July 1980), ed. W. Bibel and R.
Kowalski, LNCS 87, SpringerVerlag, Berlin, 1980, pp. 374385.
[Cox 1981a] P.T. Cox, T. Pietrzykowski, Deduction plans: A basis
for intelligent backtracking, IEEE Trans. on Pattern Analysis and
Machine Intelligence PAMI3(1):5265, January 1981.
[Cox 1981b] P.T. Cox, On determining the causes of
nonunifiability, Auckland Computer Science Report No. 23, Univ.
of Auckland, 1981; also J. Logic Programming 4(1987):3358.
[Cox 1984] P.T. Cox, T. Pietrzykowski, A complete, nonredundant
algorithm for reversed skolemization, Theoretical Computer Science
28(1984):239261.
[Cox 1985] P.T. Cox, T. Pietrzykowski, Surface deduction: a
uniform mechanism for logic programming, Proc. 1985 Logic Prog.
Symp., Boston, 1985, pp. 220227.
[Cox 1986a] P.T. Cox, T. Pietrzykowski, Causes for events: their
computation and applications, Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp.
608621.
[Cox 1986b] P.T. Cox, T. Pietrzykowski, Incorporating equality
in logic programming via surface deduction, Annals of Pure and
Applied Logic 31(1986):177189.
[Craig 1957a] W. Craig, Linear reasoning: A new form of the
HerbrandGentzen theorem, J. Symbolic Logic 22(1957):250268.
[Craig 1957b] W. Craig, Three uses of the HerbrandGentzen
theorem relating model theorem to proof theorem, J. Symbolic Logic
22(1957):269286.
[Craigen 1987] D. Craigen, et al., mEVES: A tool for verifying
software, TR87540226, I.P. Sharp Associates Limited, August
1987; also in Proc. 10th Intl. Conf. on Software Engineering,
Singapore, 1115 April 1987.
*[Craigen 1992] D. Craigen, S. Kromodimoeljo, I. Meisels, B.
Pase, M. Saaltink, EVES system description, 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. 771775.
[CroneRawe 1989] B. CroneRawe, Unification algorithms for
Boolean rings, SEKI Working Paper SWP8901, Universitat
Kaiserslautern, 1989.
[Cunningham 1983a] R.J. Cunningham, S. ZappacostaAmboldi,
Software tools for firstorder logic, Software Practice and
Experience 13(1983):10191025.
[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. 149169.
[Curry 1958] H.B. Curry, R. Feys, W. Craig, Combinatory Logic,
Vol. 1, NorthHolland, Amsterdam, 1958.
[Curry 1972] H.B. Curry, J.R. Hindley, J.P. Seldin, Combinatory
Logic, Vol. 2, NorthHolland, Amsterdam, 1972.
*[Cvetkovic 1988] D. Cvetkovic, I. Pevac, Manmachine theorem
proving in graph theory, Artificial Intelligence 35(1):124, 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
(WendischRietz, GDR, April 1985), ed. W. Bibel and K.P. Jantke,
LNCS 215 SpringerVerlag, Berlin, 1985, pp. 149155.
[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. 798809.
*[Cyrluk 1988] D.A. Cyrluk, R.M. Harris, D. Kapur, GEOMETER: A
theorem prover for algebraic geometry, 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. 770771.
*[Czapor 1986] S.R. Czapor, K.O. Geddes, On implementing
Buchberger's algorithm for Grobner bases, 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. 233238.
*[Czapor 1987] S.R. Czapor, Solving algebraic equations via
Buchberger's algorithm, Proc. European Conf. on Computer Algebra
(EUROCAL '87, Leipzig, GDR, 25 June 1987), ed. J.H. Davenport,
LNCS 378, SpringerVerlag, Berlin, 1989, pp. 260269.
[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 ifthenelse technique for
automated theorem proving in propositional calculus, Bul. Inst.
Politeh. 'Gheorghe GheorghiuDej' Bucuresti 43(2):95100, Rumania,
June 1981.
*[Dafa 1992] L. Dafa, A natural deduction automated theorem
proving system, Proc. 11th Intl. Conf. on Automated Deduction
(CADE11, Saratoga Springs, NY, USA, June 1992), ed. D. Kapur,
Lecture Notes in Artificial Intelligence 607, SpringerVerlag,
Berlin, 1992, pp. 668672.
[Darlington 1962] J.L. Darlington, A Comit program for
DavisPutnam algorithm, Research Lab. Electron. Mech. Translation
Group, MIT, 1962.
[Darlington 1964] J.L. Darlington, Translating ordinary language
into symbolic logic, MACM149, MIT, Cambridge, MA, March 1964.
[Darlington 1965] J.L. Darlington, Machine methods for proving
logical arguments expressed in English, Mech. Transl.
8(1965):4167.
[Darlington 1968a] J.L. Darlington, Some theoremproving
strategies based on the resolution principal, Machine Intelligence
2. ed. Dale and Michie, American Elsevier, NY, 1968, pp. 5771.
[Darlington 1968b] J. Darlington, Automatic theoremproving with
equality substitutions and mathematical induction, Machine
Intelligence 3, ed. Dale and Michie, Oliver and Boyd, Edinburgh,
1968, pp. 113127.
[Darlington 1969a] J.L. Darlington, Theorem proving and
information retrieval, Machine Intelligence 4, ed. B. Meltzer and
D. Michie, American Elsevier, NY, 1969, pp. 173181.
[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
secondorder logic, Machine Intelligence 6, ed. B. Meltzer and D.
Michie, American Elsevier, NY, 1971, pp. 91100.
[Darlington 1972] J.L. Darlington, Deductive plan formation in
higherorder logic, Machine Intelligence 7, ed. B. Meltzer and D.
Michie, Univ. of Edinburgh Press, 1972, pp. 129137.
[Darlington 1977] J.L. Darlington, Improving the efficiency of
higher order unification, Proc. 5th IJCAI, MIT, Cambridge, MA,
1977, pp. 520525.
[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 programmingan evaluation mechanism
for absolute set abstraction, Proc. 3rd Intl. Conf. Rewriting
Techniques and Applications (Chapel Hill, North Carolina, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
92108.
[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, NorthHolland, AmsterdamNew York, 1986,
pp. 301313.
[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, SpringerVerlag, Berlin, pp. 8089.
[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,
2225 June 1987, pp. 353359.
[Dauchet 1987c] M. Dauchet, F. De Comite, A gap between linear
and nonlinear termrewriting systems, Proc. 2nd Intl. Conf. on
Rewriting Techniques and Applications (Bordeaux, France, 2527 May
1987), ed. P. Lescanne, LNCS 256, SpringerVerlag, Berlin, 1987,
pp. 95104.
[Dauchet 1988] M. Dauchet, Termination of rewriting is
undecidable in the onerule case, Proc. 13th Mathematical
Foundations of Computer Science, Carlsbad, CSSR, LNCS 324,
SpringerVerlag, September 1988, pp. 262270.
*[Dauchet 1989a] M. Dauchet, Simulation of Turing machines by a
leftlinear rewrite rule, Proc. 3rd Intl. Conf. Rewriting
Techniques and Applications (Chapel Hill, North Carolina, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
109120.
*[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, 35 April 1989), ed. N. Dershowitz, SpringerVerlag, NY,
1989, pp. 556558.
*[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, 47 June 1990), IEEE Computer
Society Press, Los Alamitos, CA, 1990, pp. 242248.
[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. 215233; also Automation of Reasoning  Classical Papers on
Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 4148.
[Davis 1958] M. Davis, Computability and Unsolvability, McGraw
Hill, 1958.
[Davis 1959] M. Davis, H. Putnam, A computational proof
procedure, AFOSR TR 59124, Rensselaer PolyTech. Institution,
Troy, NY, 1959.
[Davis 1960a] M. Davis, H. Putnam, A computing procedure for
quantification theory, JACM 7(3):201215, 1960; also Automation of
Reasoning  Classical Papers on Computational Logic, Vol. I,
19571966, ed. J. Siekmann and G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 125139.
[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):394397; also
Automation of Reasoning  Classical Papers on Computational Logic,
Vol. I, 19571966, ed. J. Siekmann and G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 267270.
[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. 1530; also Automation of Reasoning
 Classical Papers on Computational Logic, Vol. I, 19571966, ed.
J. Siekmann and G. Wrightson, SpringerVerlag, Berlin, 1983, pp.
315330.
[Davis 1968] M. Davis, Invited commentary on new directions in
mechanical theoremproving, Proc. IFIP Congress 1968, Vol. 1,
NorthHolland, Amsterdam, 1968, pp. 6768.
[Davis 1973] M. Davis, Hilbert's tenth problem is unsolvable,
Amer. Math. Monthly 80(3):233269, 1973.
[Davis 1979a] M. Davis, J.T. Schwartz, Metamathematical
extensibility for theorem verifiers and proofcheckers, Computers
and Mathematics with Applications 5(3):217230, 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
(CADE4, Austin, Texas, 13 February 1979), ed. W.H. Joyner, 1979;
also Automation of Reasoning  Classical Papers on Computational
Logic, Vol. I, 19571966, ed. J. Siekmann and G. Wrightson,
SpringerVerlag, Berlin, 1983, pp. 128.
[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. 530531.
[Davis 1980b] R. Davis, Metarules: reasoning about control,
Artificial Intelligence 15(1980):179222.
[Davis 1982] R. Davis, D. Lenat, KnowledgeBased Systems in
Artificial Intelligence, McGrawHill, 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, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983.
[Davydov 1973] G.V. Davydov, Synthesis of the resolution method
with the inverse method, J. Soviet Mathematics 1:1218, 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,
19671970, ed. J. Siekmann And G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 531541.
[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):114116.
[Degano 1985] P. Degano, F. Sirovich, An evaluation based
theorem prover, IEEE Transactions of Pattern Analysis and Machine
Intelligence PAMI7(1):7079, January 1985.
[deGroote 1987] P. deGroote, How I spent my time in Cambridge
with Isabelle, Tech. Report RR 871, Universite Catholique de
Louvain, January 1987.
[Degtyarev 1986] A.I. Degtyarev, A.A. Voronkov, Equality control
methods in machine theorem proving, Cybernetics 3(22):298307,
MayJune 1986.
[Degtyarev 1986a] A.I. Degtyarev, A.A. Voronkov, Methods of
control of equality in mechanical proofs of theorems, Kibernetika
(Kiev) 3:3441, 1986.
[Degtyarev 1986b] A.I. Degtyarev, A.A. Voronkov, Control
equality methods in mechanical proofs of theorems, Cybernetics
22(3):298307, MayJune 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 antiunification, Logic Programming: Proc. of the 7th
Intl. Conf. (ed. D.H.D. Warren and P. Szeredi, MIT Press, 1990,
pp. 355369. [Deliyanni 1979] A. Deliyanni, R.A. Kowalski, Logic
and semantic networks, CACM 22(3):184192, 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. 10011012.
*[Demolombe 1991] R. Demolombe, L. Farinas del Cerro, An
inference rule for hypothesis generation, Proc. 12th Intl. Conf.
on Artificial Intelligence, Vol 1 (IJCAI91, Darling Harbour,
Sydney, Australia, 2430 August 1991), Morgan Kaufmann Publ.,
Inc., 1991, pp. 152157.
[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 (GWAI89, Eringerfeld, 1822 September
1989), ed. D. Metzing, SpringerVerlag, Berlin, 1989, pp. 92101.
[Dershowitz 1979a] N. Dershowitz, Z. Manna, Proving termination
with multiset orderings, Proc. Intl Colloquium on Automata,
Languages and Programming, Graz, July 1979, pp. 188202; CACM
22(8):465476, August 1979.
[Dershowitz 1979b] N. Dershowitz, A note on simplification
orderings, Information Processing Letters 9(5):212215, 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. 123131; also Theoretical
Computer Science 17(3):279301, NorthHolland, 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 ATR82(8478)3,
Information Sciences Research Office, The Aerospace Corporation,
El Segundo, CA, 1982.
[Dershowitz 1983a] N. Dershowitz, Computing with rewrite
systems, Report no. ATR83 (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. 269298; also Information and Control
64(2/3):122157, May/June 1985.
[Dershowitz 1983b] N. Dershowitz, Applications of the
KnuthBendix completion procedure, Technical Report
ATR83(8478)2, Aerospace Corp., El Segundo, CA, May 1983.
[Dershowitz 1983c] N. Dershowitz, J. Hsiang, N.A. Josephson,
D.A. Plaisted, Associativecommutative rewriting, Proc. 8th IJCAI,
Karlsruhe, W. Germany, August 1983, pp. 940944.
[Dershowitz 1983d] N. Dershowitz, Wellfounded orderings,
ATR83(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 nonclausal 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. 114123,
[Dershowitz 1985a] N. Dershowitz, Termination of rewriting,
Report No. UIUCDSR851220, UILUENG851728, Dept. of Computer
Science, Univ. of Illinois at UrbanaChampaign, 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):69116, February/April 1987; Corrigendum in
4(3):409410, December 1987.
[Dershowitz 1985b] N. Dershowitz, L. Marcus, A. Tarlecki,
Existence, uniqueness, and construction of rewrite systems, Report
ATR85(8354)7, Lab. Operations, The Aerospace Corp., El Segundo,
CA, 1985; also in SIAM J. Computing 17(4):629639, 1988.
[Dershowitz 1985c] N. Dershowitz, Termination, rewriting
techniques and applications, Proc. Conf. Rewriting Techniques and
Applications, LNCS 202, SpringerVerlag, 1985, pp. 180224.
*[Dershowitz 1988a] N. Dershowitz, M. Okada, Prooftheoretic
techniques for term rewriting theory, Proc. 3rd Annual Symp. on
Logic in Computer Science (Edinburgh, Scotland, 58 July 1988),
IEEE, 1988, pp. 104111.
*[Dershowitz 1988b] N. Dershowitz, M. Okada, G. Sivakumar,
Canonical conditional rewrite systems, 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. 538549.
*[Dershowitz 1988c] N. Dershowitz, G. Sivakumar, Goaldirected
equation solving, Proc. AAAI88, 7th National Conf. on Artificial
Intelligence, Vol. 1, St. Paul, Minnesota, 2126 August 1988, pp.
166170.
*[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. 2156.
*[Dershowitz 1988e] N. Dershowitz, M. Okada, G. Sivakumar,
Confluence of conditional rewrite systems, 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. 3144.
*[Dershowitz 1988f] N. Dershowitz, G. Sivakumar, Solving goals
in equational language, 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. 4555.
*[Dershowitz 1989a] N. Dershowitz, S. Kaplan, Rewrite, rewrite,
rewrite,..., Proc. 16th Annual ACM Symp. on Principles of
Programming (POPL89, Austin, Texas, 1113 January 1989), ACM, NY,
1989.
*[Dershowitz 1989b] N. Dershowitz, ed., Proc. 3rd Intl. Conf.
Rewriting Techniques and Applications (Chapel Hill, North
Carolina, 35 April 1989), SpringerVerlag, NY, 1989.
*[Dershowitz 1989c] N. Dershowitz, Completion and its
applications, In: Resolution of Equations in Algebraic Structures,
Vol. 2: Rewriting Techniques, ed. H. AitKaci and M. Nivat,
Academic Press, Inc., San Diego, 1989, pp. 3185.
*[Dershowitz 1990a] N. Dershowitz, E. Pinchover, Inductive
synthesis of equational programs, Proc. 8th National Conf. on
Artificial Intelligence (AAAI90, July 29August 3, 1990), AAAI
Press/MIT Press, 1990, pp. 234239.
*[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. 243320; also available as Rapport 478, LRI,
Univ. ParisSud, France.
[Dershowitz 1990c] N. Dershowitz, M. Okada, A rationale for
conditional equational rewriting, Theoret. Comput. Sci.
75(1/2):111137, 1990.
[Dershowitz 1991a] N. Dershowitz, S. Kaplan, D.A. Plaisted,
Rewrite, rewrite, rewrite, rewrite, rewrite, ... Theor. Comput.
Sci. 83(1):7196, June 1991.
[Dershowitz 1991b] N. Dershowitz, Orderingbased strategies for
Horn clauses, Proc. 12th Intl. Conf. on Artificial Intelligence,
Vol 1 (IJCAI91, Darling Harbour, Sydney, Australia, 2430 August
1991), Morgan Kaufmann Publ., Inc., 1991, pp. 118124.
[Dershowitz 1991c] N. Dershowitz, J.P. Jouannaud, Notations for
rewriting, In EATACS Bulletin, pp. 162172, 1991.
*[Dershowitz 1992] N. Dershowitz, S. Mitra, G. Sivakumar,
Decidable matching for convergent systems, Proc. 11th Intl. Conf.
on Automated Deduction (CADE11, Saratoga Springs, NY, USA, June
1992), ed. D. Kapur, Lecture Notes in Artificial Intelligence 607,
SpringerVerlag, Berlin, 1992, pp. 589602.
[Desimone 1987] R. Desimone, Explanationbased 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. EWSL86.
[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, 2022 May 1985), ed. J.P. Jouannaud, LNCS 202,
SpringerVerlag, Berlin, 1985, pp. 255270.
[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):157215.
[Dick 1984] A.J.J. Dick, Automated equational reasoning and the
KnuthBendix 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, 13 April 1985),
Vol. 2: Research Contributions, ed. B.F. Caviness, LNCS 204,
SpringerVerlag, Berlin, pp. 400401; 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
(CADE8, Oxford, England, July 27August 1, 1986), ed. J.H.
Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp. 272280.
[Dick 1988a] A.J.J. Dick, Ordersorted 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 RAL88055, Rutherford Appleton Laboratory,
Chilton, September 1988.
[Dick 1990] J. Dick, J. Kalmus, U. Martin, Automating the Knuth
Bendix ordering, Acta Inf. 28(2):95119, December 1990.
*[Dick 1991] A.J.J. Dick, An introduction to KnuthBendix
Completion, The Computer Journal 34(1):215, February 1991.
*[Dick 1991a] A.J.J. Dick, P. Watson, Ordersorted term
rewriting, The Computer Journal 34(1):1619, February 1991.
[Dick 1991b] A.J. Dick, An introduction to KnuthBendix
completion, Comput. J. 34(1):215, February 1991. Special issue on
term rewriting.
*[Diekert 1987] V. Diekert, On the KnuthBendix completion for
concurrent processes, Proc. 14th Intl. Colloquium on Automata,
Languages, and Programming (ICALP '87, Karlsruhe, W. Germany,
1317 July 1987), ed. T. Ottmann, LNCS 267, SpringerVerlag,
Berlin, pp. 4253.
*[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, 911
March 1988), ed. T. Danielsen, IOS, Amsterdam, Netherlands, 1988,
pp. 1321.
[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 (CADE8, Oxford,
England, July 27August 1, 1986), ed. J.H. Siekmann, LNCS 230,
SpringerVerlag, Berlin, 1986, pp. 6278.
[Digricoli 1979a] V.J. Digricoli, Resolution by unification and
equality, Proc. 4th Workshop on Automated Deduction (CADE4,
Austin, Texas, 13 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. 240250.
[Digricoli 1980] V.J. Digricoli, First experiments with RUE
automated deduction, Proc. 1st Natl Conf. on Artificial
Intelligence, Stanford Univ., August 1980, pp. 9698.
[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.
539547.
[Digricoli 1985] V.J. Digricoli, The management of heuristic
search in boolean experiments with RUE resolution, Proc. 9th
IJCAI, Los Angeles, CA, 1985, pp. 11561161.
*[Digricoli 1986] V.J. Digricoli and M.C. Harrison,
Equalitybased binary resolution, JACM 33(2):253289, April 1986.
*[Digricoli 1989] V.J. Digricoli, J.J. Lu, V.S. Subrahmanian,
Andor graphs applied to RUE resolution, Proc. 11th IJCAI
(Detroit, Michigan, USA, 2025 August 1989), ed. N.S. Sridharan,
IJCAI Inc., 1989, pp. 354358.
*[Digricoli 1992] V.J. Digricoli, E. Kochendorfer, LIM+
challenge problems by RUE hyperresolution, 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. 239252.
[Dilger 1984a] W. Dilger, and HA. Schneider, ASSIPT: A theorem
proving machine, Proc. Intl. Conf. on 5th Generation Computer
Systems, Tokio, 1984, pp. 497506; also Proc. 9th IJCAI, Vol. 2,
Los Angeles, CA, August 1985, pp. 11941200.
[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 HA. 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):4362, 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. AitKaci, M. Nivat, Academic
Press, Inc., San Diego, 1989, pp. 87115.
*[Dincbas 1988] M. Dincbas, et al., The CHIP system: Constraint
handling in Prolog, 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. 774775.
[DiPaola 1973] R.A. DiPaola, The solvability of the decision
problem for classes of proper formulas and related results, JACM
20(1):112126, 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 Zresolution program,
Div. of Comput. Res. and Tech., Nat. Inst. of Health, Bethesda,
Maryland, 1971.
[Dixon 1973] J.K. Dixon, Zresolution: Theorem proving with
compiled axioms, JACM 20(1):127147, 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 ADG8726188,
Computer Science.
[Doggaz 1991] N. Doggaz, C. Kirchner, Completion for
unification, Theor. Comput. Sci. 85(2):231251, 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 (CADE9, Argonne, Illinois,
2326 May 1988), ed. E. Lusk and R. Overbeek, LNCS 310,
SpringerVerlag, Berlin, 1988, pp. 4160.
*[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, 47 June 1990), IEEE
Computer Society Press, Los Alamitos, CA, 1990, pp. 300310.
*[Dougherty 1990] D.J. Dougherty, P. Johann, An improved general
Eunification method, 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. 261275.
*[Dougherty 1992] D.J. Dougherty, P. Johann, A combinatory logic
approach to higherorder Eunification, 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. 7993.
[Dowling 1984] W.F. Dowling, J.H. Gallier, Lineartime
algorithms for testing the satisfiability of propositional Horn
formulae, J. of Logic Programming 3:267284, 1984.
[Downey 1978] P.J. Downey, H. Samet, R. Sethi, Offline and
online algorithms for deducing equalities, POPL5, Tucson,
Arizona, 1978.
[Downey 1980] P.J. Downey, R. Sethi, R.E. Tarjan, Variations on
the common subexpression problem, JACM 27(4):758771, October
1980.
[Doyle 1979] J. Doyle, A truth maintenance system, Artificial
Intelligence 12(1979):231272.
[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
modeltheoretic justification, Harvard Univ., Cambridge, MA, 1964.
[Dreben 1979] B. Dreben, W.D. Goldfarb, The Decision Problem 
Solvable Classes of Quantificational Formulas. AddisonWesley
Publ. Co., 1979.
[Drosten 1983] K. Drosten, Toward executable specifications
using conditional axioms, Rept. 8301, Tech. Univ. Braunschweig,
W. Germany, 1983.
[Drosten 1985] K. Drosten, Term rewriting systems with
restricted variables, Bericht Nr. 8511, 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 (CADE9, Argonne, Illinois, 2326 May
1988), ed. E. Lusk and R. Overbeek, LNCS 310, SpringerVerlag,
Berlin, 1988, pp. 121130.
[Duda 1978] R.O. Duda, P.E. Hart, N.J. Nilsson, G.L. Sutherland,
Semantic network representations in rulebased inference systems,
in PatternDirected Inference Systems, ed. Waterman and
HayesRoth, Academic Press, NY, 1978, pp. 203221.
[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.4SN18.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. 3751.
[Dunham 1959] B. Dunham, R. Fridshal, G.L. Sward, A nonheuristic
program for proving elementary logical theorems, Proc. IFIP Congr.
1959, pp. 282285; also Automation of Reasoning  Classical Papers
on Computational Logic, Vol. I, 19571966, ed. J. Siekmann and G.
Wrightson, SpringerVerlag, Berlin, 1983, pp. 9398.
[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,
19571966, ed. J. Siekmann and G. Wrightson, SpringerVerlag,
Berlin, 1983, pp. 276287.
[Dunham 1963] B. Dunham, J. North, Theorem testing by computer,
Proc. Symp. Math. Theory Automata, Polytechnic Press, Brooklyn,
NY, 1963, pp. 173177; also Automation of Reasoning  Classical
Papers on Computational Logic, Vol. I, 19571966, ed. J. Siekmann
and G. Wrightson, SpringerVerlag, Berlin, 1983, pp. 271275.
[Dunham 1976] B. Dunham, H. Wang, Towards feasible solutions of
the tautology problem, Annals of Math. Logic 10(1976):117154.
*[Dwork 1984] C. Dwork, P. Kanellakis, P. Mitchell, On the
sequential nature of unification, J. of Logic Programming
1(1):3550, June 1984; also Tech. Report CS8326, Brown Univ.
[Dwork 1986] C. Dwork, P. Kanellakis, L. Stockmeyer, Parallel
algorithms for term matching, Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp.
416430; also SIAM J. of Computing 17(4):711731, August 1988.
[Echahed 1988] R. Echahed, On completeness of narrowing
strategies, Proc. CAAP '88, LNCS 299, SpringerVerlag, 1988, pp.
89101.
[Eder 1976] A Prologlike interpreter for nonHorn 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 ATP17183, 1983; also Proc. GWAI83,
7th German Workshop on Artificial Intelligence, Dassel/Solling
(September 1983), in InformatikFachberichte 76, SpringerVerlag,
Berlin, 1983, pp. 197206; also J. of Symbolic Computation
1(1):3146, 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, 1720 September 1984), ed. W. Bibel and B. Petkoff,
NorthHolland, Amsterdam, 1985, pp. 121128.
[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, SpringerVerlag, Berlin, 1989, pp.
8098.
*[Eder 1991] E. Eder, Consolution and its relations with
resolution, Proc. 12th Intl. Conf. on Artificial Intelligence, Vol
1 (IJCAI91, Darling Harbour, Sydney, Australia, 2430 August
1991), Morgan Kaufmann Publ., Inc., 1991, pp. 132136.
[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.269278. (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,
SpringerVerlag, 1987, pp. 215239.
*[Egly 1992] U. Egly, A simple proof for the pigeonhole
formulae, Proc. 10th ECAI (ECAI 92, Vienna, Austria, 37 August
1992), ed. B. Neumann, John Wiley & Sons, Chichester, 1992,
pp. 7071.
[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 (CADE10, Kaiserslautern, FRG,
July 1990), Lecture Notes in Artificial Intelligence 449, ed. M.E.
Stickel, SpringerVerlag, Berlin, 1990, pp. 651652.
[Eisinger 1981] N. Eisinger, Subsumption and connection graphs,
Proc. GWAI81, InformatikFachberichte 47, ed. Siekmann,
SpringerVerlag, Berlin, 1981, pp. 188198; also Proc. 7th IJCAI,
Vancouver, Canada, 1981, pp. 480486.
[Eisinger 1983] N. Eisinger, M. Weigele, A technical note on
splitting and clausal form algorithms, Proc. GWAI83, 7th German
Workshop on Artificial Intelligence, Dassel/Solling (September
1983), InformatikFachberichte 76, SpringerVerlag, Berlin, 1983,
pp. 225232.
[Eisinger 1986a] N. Eisinger, What you always wanted to know
about clause graph resolution, Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp.
316336.
[Eisinger 1986b] N. Eisinger, H.J. Ohlbach, The Markgraf Karl
Refutation Procedure (MKRP), Proc. 8th Intl. Conf. on Automated
Deduction (CADE8, Oxford, England, July 27August 1, 1986), ed.
J.H. Siekmann, LNCS 230, SpringerVerlag, Berlin, 1986, pp.
681682.
*[Eisinger 1988] N. Eisinger, Completeness, confluence, and
related properties of clause graph resolution, PhD thesis, SEKI
Report SR8807, 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 SR8910, 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 1719, 1982, pp. 121124.
*[Elkan 1989] C. Elkan, Conspiracy numbers and caching for
searching and/or trees and theoremproving, Proc. 11th IJCAI
(Detroit, Michigan, USA, 2025 August 1989), ed. N.S. Sridharan,
IJCAI Inc., 1989, pp. 341346.
*[Elliot 1989] C. M. Elliott, Higherorder unification with
dependent function types, Proc. 3rd Intl. Conf. Rewriting
Techniques and Applications (Chapel Hill, North Carolina, 35
April 1989), ed. N. Dershowitz, SpringerVerlag, NY, 1989, pp.
121136.
[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.
8792.
[Emerson 1984] E.A. Emerson, A.P. Sistla, Deciding full
branching time logic, Information and Control 61(1984):175201.
[Emerson 1985a] E.A. Emerson, Automata, tableaux and temporal
logics, LNCS 193, 1985, pp. 7987.
[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):124.
[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 1486, Greco de Programmation,
Universite de Bordeaux I, France, 1986; also Theoretical Computer
Science 65(1989):133. [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,
811 July 1980), ed. W. Bibel and R. Kowalski, LNCS 87,
SpringerVerlag, Berlin, 1980, pp. 220231.
[Erni 1981] W. Erni, R. Lapsien, On the time and tape complexity
of weak unification, Information Processing Letters 12(3):146150,
June 1981.
[Ernst 1967] G.W. Ernst, A. Newell, Some issues of
representation in a general problem solver, AFIPS Conf. Proc.
30(1967):583600.
[Ernst 1970] G.W. Ernst, GPS and decision making: An overview,
Theoretical Approaches to NonNumerical Problem Solving, ed.
Banerji, BerlinMunchenHeidelberg, 1970.
[Ernst 1971] G.W. Ernst, The utility of independent subgoals in
theorem proving, Information and Control 18(April 1971):237252.
[Ernst 1973] G.W. Ernst, A definitiondriven theorem prover,
Rep. 1124, Dept. Computer. and Inform. Sci., Case Western Reserve
Univ., Cleveland, OH, 1973; also Proc. 3rd IJCAI, Stanford Univ.,
1973, pp. 5155; also IEEE Trans. on Computers C25(4):317322,
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. OGAIConf., Igls, Austria, Springer, 1989.
*[EscaladaImaz 1988] G. EscaladaImaz, M. Ghallab, A
practically efficient and almost linear unification algorithm
(research note), Artificial Intelligence 36(2):249263, September
1988.
[Evans 1951] T. Evans, On multiplicative systems defined by
generators and relations, I, Proc. of the Cambridge Philosophical
Society 47, pp. 637649, 1951.
[Evans 1968] T.G. Evans, A heuristic program to solve geometry
analogy problems, Semantic Inform. Proc., ed. Minsky, MIT Press,
1968.
