**1**- Held at the International Conference & Research Center for Computer Science, Schloss Dagstuhl, Wadern, Saarland, Germany, April 7 - 10, 1997. These workshops traditionally have no published Proceedings.
**2**-
P. B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi.

TPS: A theorem proving system for classical type theory.*Journal of Automated Reasoning*, 16:321-353, 1996. **3**-
P.B. Andrews.

Transforming matings into natural deduction proofs.

In Bibel and Kowalski, editors,*Proceedings of the Fifth Conference on Automated Deduction*, Lecture Notes in Computer Science 87, pages 281-292. Springer-Verlag, Berlin, July 1981. **4**-
O.L. Astrachan.

METEOR: Exploring Model Elimination theorem proving.*Journal of Automated Reasoning*, 13:283-296, 1994. **5**-
L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder.

Basic paramodulation and superposition.

In D. Kapur, editor,*Proceedings of the Eleventh Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 607, pages 462-476. Springer-Verlag, Berlin, June 1992. **6**-
D. Barker-Plummer and S. C. Bailin.

Graphical theorem proving: An approach to reasoning with the help of diagrams.

In*Proceedings of the European Conference on Artificial Intelligence*, pages 55-59. John Wiley and Sons, Vienna, August 1992. **7**-
D. Barker-Plummer, S. C. Bailin, and S. M. T. Ehrlichman.

Diagrams and mathematics.

In B. Selman and H. Kautz, editors,*Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics*, pages 14-17. Fort Lauderdale, Florida, January 1996. **8**-
J. Barwise and J. Etchmendy.
*The Language of First-Order Logic*.

CSLI Publications, Center for the Study of Language and Information, Stanford, third edition, 1992. **9**-
J. Barwise and J. Etchmendy.
*Hyperproof*.

CSLI Publications, Center for the Study of Language and Information, Stanford, 1994. **10**-
D. L. Beatty and R. E. Bryant.

Formally verifying a microprocessor using a simulation methodology.

In*Proceedings of the Thirty-first Design Automation Conference*, pages 596-602, 1994. **11**-
W. W. Bledsoe and G. Feng.

SET-VAR.*Journal of Automated Reasoning*, 11:293-314, 1993. **12**-
W. W. Bledsoe and L. M. Hines.

Variable elimination and chaining in a resolution-based prover for inequalties.

In Bibel and Kowalski, editors,*Proceedings of the Fifth Conference on Automated Deduction*, pages 70-87. Springer Verlag, 1980. **13**-
N. Bourbaki.
*Elements of Mathematics*.

Addison Wesley, Reading, Massachusetts, 1968. **14**-
R.S. Boyer and J.S. Moore.
*A Computational Logic Handbook*.

Academic Press, New York, 1988. **15**-
D. Brand.

Proving theorems with the Modification Method.*SIAM Journal on Computing*, 4:412-430, 1975. **16**-
I. Bratko.
*Prolog Programming for Artificial Intelligence*.

Addison-Wesley, Reading, Massachusetts, 1990. **17**-
I. Bratko and S. Muggleton.

Applications of inductive logic programming.*Communications of the Association for Computing Machines*, pages 65-70, 1995. **18**-
A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill.

Rippling: A heuristic for guiding induction proofs.*Artificial Intelligence*, 62:185-253, 1993. **19**-
A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill.

Experiments with proof plans for induction.*Journal of Automated Reasoning*, 7:303-324, 1991. **20**-
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang.

Symbolic model checking: 10^{20}states and beyond.*Information and Computation*, pages 142-170, June 1992. **21**-
S.C. Chou.
*Mechanical Geometry Theorem Proving*.

D. Reidel, Dordrecht, Netherlands, 1988. **22**-
S.C. Chou, X.S. Gao, and J.Z. Zhang.
*Machine Proofs in Geometry*.

World Scientific, Singapore, 1994. **23**-
E. M. Clarke, E. A. Emerson, and A. P. Sistla.

Automatic verification of finite-state concurrent systems using temporal logic specifications.*ACM Transactions on Programming Languages and Systems*, pages 244-263, April 1986. **24**-
E. M. Clarke and X. Zhao.

Analytica: A theorem prover for Mathematica.*The Mathematica Journal*, pages 56-71, 1993. **25**-
E. M. Clarke and X. Zhao.

Combining symbolic computation and theorem proving: Some problems of Ramanujan.

In M. A. McRobbie and J. K. Slaney, editors,*Proceedings of the Thirteenth Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 1104, pages 758-763. Springer-Verlag, Berlin, July 1996. **26**-
R.L. Constable et al.
*Implementing Mathematics with the Nuprl Proof Development System*.

Prentice Hall, 1986. **27**-
R. Constable and C. Murthy.

Finding computational content from classical proofs.

In Huet and Plotkin, editors,*Logical Frameworks*, pages 341-362. Cambridge University Press, 1991. **28**-
T. Coquand and G. Huet.

The calculus of constructions.*Information and Computation*, 76:95-120, 1988. **29**-
D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink.

EVES: An overview.

In*Proceedings of VDM'91*, Noordwijkerhout, The Netherlands, October 1991. **30**-
D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink.

Eves system description.

In D. Kapur, editor,*Proceedings of the Eleventh Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 607, pages 771-775. Springer-Verlag, Berlin, June 1992. **31**-
B. I. Dahn, J. Gehne, Th. Honigmann, and A. Wolf.

Integration of automated and interactive theorem proving in ILF.

In W. W. McCune, editor,*Proceedings of the Fourteenth Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 1249, pages 57 -60. Springer-Verlag, Berlin, July 1997. **32**-
B. I. Dahn and A. Wolf.

Natural language presentation and combination of automatically generated proofs.

In*Proceedings of the First Conference on Frontiers of Combining Systems*, pages 175-192. Kluwer Academic Publishers, 1996. **33**-
M. Davis, G. Logemann, and D. Loveland.

A machine program for theorem proving.*Communications of the Association for Computing Machines*, pages 394-397, 1962. **34**-
M. Davis and H. Putnam.

A computing procedure for quantification theory.*Journal of the Association for Computing Machines*, pages 201-215, 1960. **35**-
R. Dechter and J. Pearl.

Network-based heuristics for constraint-satisfaction problems.*Artificial Intelligence*, pages 1-38, 1988. **36**-
R. Dechter and I. Rish.

Directional Resolution: The Davis-Putnam procedure revisited.

In*Proceedings of the Third International Conference on Knowledge Representation and Reasoning (KR'94)*, Bonn, Germany, 1994. **37**-
J. Denzinger and S. Schulz.

Learning domain knowledge to improve theorem proving.

In M. A. McRobbie and J. K. Slaney, editors,*Proceedings of the Thirteenth Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 1104, pages 62-76. Springer-Verlag, Berlin, July 1996. **38**-
D. Detlefs.

An overview of the Extended Static Checking system.

In*First Workshop on Formal Methods in Software Practice (FMSP '96)*, pages 1-9, San Diego, CA, January 1996. Association for Computing Machines. **39**-
Y. Deville.
*Logic Programming: Systematic Program Development*.

Addison-Wesley, Reading, Massachusetts, 1990. **40**-
M. Fujita, J. Slaney, and F. Bennett.

Automatic generation of some results in finite algebra.

In*Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence*, pages 52-57, Chambéry, France, 1993. **41**-
H. Ganzinger, editor.
*Proceedings of the Seventh International Conference on Rewriting Techniques and Applications, RTA-96*, Lecture Notes in Computer Science 1103.

Springer-Verlag, Berlin, 1996. **42**-
H. Gelernter.

Realization of a geometry theorem-proving machine.

In*Proceedings of the International Conference on Information Processing*, pages 273-282. Paris: UNESCO House, 1959.

Also in*Computers and Thought*(Feigenbaum and Feldman, Eds.), McGraw-Hill 1963, pages 134-152. **43**-
H. Gelernter, J.R. Hanson, and D.W. Loveland.

Empirical explorations of the geometry-theorem proving machine.

In*Proceedings of the Western Joint Computer Conference*, pages 143-147, 1960.

Also in*Computing and Thought*(Feigenbaum and Feldman, Eds.), McGraw-Hill, 1963, pages 153-163. **44**-
D. Goldson, S. Reeves, and R. Bornet.

A review of several programs for the teaching of logic.*The Computer Journal*, 36:373-386, 1993. **45**-
M.J. Gordon and T.F. Melham, editors.
*Introduction to HOL: A theorem-proving environment for higher-order logic*.

Cambridge University Press, 1993. **46**-
T. A. Henzinger and Pei-Hsin Ho.

HyTech: The Cornell hybrid technology tool.

In*Hybrid Systems II*, Lecture Notes in Computer Science 999, pages 265-294. Springer-Verlag, Berlin, 1995. **47**-
L. Hines.

STR+VE and integers.

In Bundy, editor,*Proceedings of the Twelfth Conference on Automated Deduction*, pages 416-430. Springer Verlag, 1994. **48**-
P. H. Ho.
*The Algorithmic Analysis of Hybrid Systems*.

PhD thesis, Cornell University, 1995. **49**-
D. J. Howe.

The computational behavior of Girard's paradox.

In*Proceedings of the IEEE Symposium on Logic in Computer Science*, pages 205-214, Washington, D. C., 1987. **50**-
D. J. Howe.

Importing mathematics from HOL into Nuprl.

In J. von Wright, J. Grundy, and J. Harrison, editors,*Theorem Proving in Higher Order Logics*, Lecture Notes in Computer Science 1125, pages 267-282. Springer-Verlag, Berlin, 1996. **51**-
X. Huang and A. Fiedler.

Presenting machine-found proofs.

In M. A. McRobbie and J. K. Slaney, editors,*Proceedings of the Thirteenth Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 1104, pages 221-225. Springer-Verlag, Berlin, July 1996. **52**- Private communication from D. Kapur, March 1997.
**53**-
D. Kapur and M. Subramaniam.

Mechanically verifying a family of multiplier circuits.

In Alur and Henzinger, editors,*Proceedings of the Conference on Computer Aided Verification*, Lecture Notes in Computer Science 1102, pages 135-146, Berlin, August 1996. Springer-Verlag. **54**-
D. Kapur and H. Zhang.

An overview of Rewrite Rule Laboratory.*Computers and Mathematics with Applications*, pages 91-114, 1995. **55**-
M. Kaufmann and J. S. Moore.

ACL2: An industrial strength version of Nqthm.

In*Proceedings of the Eleventh Annual Conference on Computer Assurance*, pages 23-34. IEEE Computer Society Press, 1996. **56**-
H. Kautz, D. McAllester, and B. Selman.

Encoding plans in propositional logic.

In*Proceedings of the Fourth International Conference on Principles of Knowledge Representation and Reasoning*, pages 374-384. Morgan Kaufmann, November 1996. **57**-
H. Kautz and B. Selman.

Pushing the envelope: Planning, propositional logic, and stochastic search.

In*Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96)*, pages 1194-1201, Portland, Oregon, 1996. AAAI Press/MIT Press. **58**-
D. King and R. Arthan.

Development of practical verification tools.*The ICL Systems Journal*, May 1996. **59**-
D. E. Knuth and P. B. Bendix.

Simple word problems in universal algebra.

In Leech, editor,*Combinatorial Problems in Abstract Algebras*, pages 263-270. Pergamon, New York, 1970. **60**-
R. Kowalski.

Robert Kowalski on logic programming: an interview.*Future Generations Computer Systems*, pages 79-83, 1984. **61**-
K. Kunen.

Moufang quasigroups.*Journal of Algebra*, 183:231-234, 1996. **62**-
K. Kunen.

Quasigroups, loops, and associative laws.*Journal of Algebra*, 185:194-204, 1996. **63**-
H. J. Levesque, R. Reiter, Y. Lespérance, F. Lin, and R. B. Scherl.

GOLOG: A logic programming language for dynamic domains.*Journal of Logic Programming*, 1996.

To appear. **64**-
D.W. Loveland.

A simplified format for the Model Elimination procedure.*Journal of the Association for Computing Machines*, pages 349-363, 1969. **65**-
D.W. Loveland.

Automated theorem proving: a quarter-century review.

In Bledsoe and Loveland, editors,*Automated Theorem Proving: after 25 Years*, volume 29 of*Contemporary Mathematics*, pages 1-45. American Mathemtical Society, Providence, 1984. **66**-
Z. Manna and R. Waldinger.

A deductive approach to program synthesis.*ACM Transactions on Programming Languages*, pages 90-121, 1980. **67**-
J. McCarthy.

Programs with common sense.

In Minsky, editor,*Semantic Information Procession*, pages 403-418. The MIT Press, 1968. **68**-
J. McCarthy and P. Hayes.

Some philosophical problems from the standpoint of artificial intelligence.

In Meltzer and Michie, editors,*Machine Intelligence 4*, pages 463-502. Edinburgh University Press, Edinburgh, 1969. **69**-
W. McCune.

Single axioms for groups and abelian groups with various operations.*Journal of Automated Reasoning*, 10:1-13, 1993. **70**-
W. McCune.

OTTER 3.0 Reference Manual and Guide.

Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994. **71**-
W. McCune.

33 basic test problems: A practical evaluation of some paramodulation strategies.

Preprint ANL/MCS-P618-1096, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1996. **72**-
D. MacKenzie.

The automation of proof, a historical and sociological exploration.*IEEE Annals of the History of Computing*, 17:7-29, 1995. **73**-
W. McCune and L. Wos.

Otter. The CADE-13 Competition incarnations.*Journal of Automated Reasoning*, 18:211-220, 1997. **74**-
E. Melis and J. Whittle.

Internal analogy in theorem proving.

In M. A. McRobbie and J. K. Slaney, editors,*Proceedings of the Thirteenth Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 1104, pages 92-105. Springer-Verlag, Berlin, July 1996. **75**-
D. A. Miller.

Expansion tree proofs and their conversion to natural deduction proofs.

In Shostak, editor,*Proceedings of the Seventh Conference on Automated Deduction*, Lecture Notes in Computer Science 170, pages 347-370. Springer-Verlag, Berlin, May 1984. **76**-
R. Milner, M. Tofte, and R. Harper.
*The Definition of Standard ML*.

MIT Press, 1990. **77**-
J.S. Moore.

Introduction to the OBDD algorithm for the ATP community.*Journal of Automated Reasoning*, pages 33-45, 1994. **78**-
M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr.

SETHEO and E-SETHEO: The CADE-13 Systems.*Journal of Automated Reasoning*, 18:237-246, 1997. **79**-
C. Murthy.

An evaluation semantics for classical proofs.

In*Proceedings of the IEEE Symposium on Logic in Computer Scienc e*, pages 96-109, Washington, D. C., 1991. **80**-
G. Nadathur and D. Miller.

An overview of Lambda-Prolog.

In*Proceedings of the Fifth International Conference and Symposium on Logic Programming*. MIT Press, 1988. **81**-
A. Newell, J.C. Shaw, and H.A. Simon.

Empirical explorations of the logic theory machine: a case study in heuristics.

In*Proceedings of the Western Joint Computer Conference*, pages 218-239, 1956.

Also in*Computers and Thought*(Feigenbaum and Feldman, Eds.), McGraw-Hill, 1963, pages 134-152. **82**-
With Major Math Proof Brute Computers Show Flash of Reasoning
Power.

New York Times, Sunday, December 10, 1996. **83**-
S. Owen.
*Analogy for Automated Reasoning*.

Academic Press, London, 1990. **84**-
S. Owre, J.M. Rushby, and N. Shankar.

PVS: A Prototype Verification System.

In D. Kapur, editor,*Proceedings of the Eleventh Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 607, pages 748-752. Springer-Verlag, Berlin, June 1992. **85**-
L. C. Paulson.

Set theory for verification: I. from foundations to functions.*Journal of Automated Reasoning*, 11:353-389, 1993. **86**-
L. C. Paulson.
*Isabelle: a Generic Theorem Prover*.

Lectures Notes in Computer Science 828. Springer-Verlag, Berlin, 1994. **87**-
L. C. Paulson and K. Grabczewski.

Mechanizing set theory.*Journal of Automated Reasoning*, 17:291-323, 1996. **88**-
G. Péli, J. Bruggeman, M. Masuch, and B. Ó Nualláin.

A logical approach to formalizing organizational ecology.*American Sociological Review*, 59(4):571-593, 1994. **89**-
G. Péli and M. Masuch.

The logic of propagation strategies: Axiomatizing a fragment of organizational ecology in first-order logic.*Organization Science*, 8(3):310-331, 1997. **90**-
D. A. Plaisted and Y. Zhu.

Ordered semantic hyper linking.

In*Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI97)*, July 1997. **91**-
QED Group.

The QED Manifesto.

In Alan Bundy, editor,*Proceedings of the Twelfth International Conference on Automated Deduction*, pages 238-251. Springer-Verlag, 1994.

A comprehensive view of QED is obtained at the Web site`http://www.mcs.anl.gov/qed`. **92**-
J.A. Robinson.

A machine-oriented logic based on the resolution principle.*Journal of the Association for Computing Machines*, pages 23-41, 1965. **93**-
J.A. Robinson.

Logic and logic programming.*Communications of the Association for Computing Machines*, pages 40-65, 1992. **94**-
J. Slanet, M. Fujita, and M. Stickel.

Automated reasoning and exhaustive search: Quasigroup existence problems.*Computers and Mathematics with Applications*, 29:115-132, 1995. **95**-
J. H. Siekmann and G. Wrightson (Eds.).
*The Automation of Reasoning*, volumes I and II.

Springer-Verlag, Berlin, 1983. **96**-
D. R. Smith.

KIDS: A semi-automated program development system.*IEEE Transactions on Software Engineering*, pages 1024-1043, September 1990.

Special Issue on Formal Methods. **97**-
M. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood.

Deductive composition of astronomical software from subroutine libraries.

In Bundy, editor,*Proceedings of the Twelfth Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 814, pages 341-355. Springer-Verlag, Berlin, 1994. **98**-
M.E. Stickel.

A complete unification algorithm for associative-commutative functions.

In*Proceedings of the Fourth International Joint Conference on Artificial Intelligence*, pages 423-434, Tbilisi, USSR, 1975.

Also see*Journal of the Association for Computing Machines*, 1981, pages 423-434. **99**-
P. Suppes and J. McDonald.

Student use of an interactive theorem prover.

In Bledsoe and Loveland, editors,*Automated Theorem Proving: After 25 Years*, volume 29 of*Contemporary Mathematics*, pages 315-360. American Mathemtical Society, Providence, 1984. **100**-
G. Sutcliffe and C. B. Suttner.

The Results of the CADE-13 ATP System Competition.*Journal of Automated Reasoning*, 18:271-286, 1997. **101**-
C. B. Suttner and G. Sutcliffe.

The Design of the CADE-13 ATP System Competition.*Journal of Automated Reasoning*, 18:139-162, 1997. **102**-
F.J. Thayer, W.M. Farmer, and J.D. Guttman.

IMPS: An interactive mathematical proof system.*Journal of Automated Reasoning*, pages 213-248, 1993. **103**-
T. Walsh, A. Nunes, and A. Bundy.

The use of proof plans to sum series.

In D. Kapur, editor,*Proceedings of the Eleventh Conference on Automated Deduction*, Lecture Notes in Artificial Intelligence 607, pages 325-339. Springer-Verlag, Berlin, June 1992. **104**-
C. Weidenbach.

SPASS: Version 0.49.*Journal of Automated Reasoning*, Special Issue on the CADE-13 ATP System Competition, 1997. **105**-
S. Winker and L. Wos.

Automated generation of models and counter examples and its application to open questions in ternary boolean algebra.

In*Proceedings of the Eighth International Symposium on Multiple-valued Logic*, pages 251-256. IEEE and ACM Publ., Rosemont, Illinois, 1978. **106**-
L. Wos.

Otter and the Moufang identity problem.*Journal of Automated Reasoning*, pages 215-257, 1996. **107**-
L. Wos, G. Robinson, and D. Carson.

Efficiency and completeness of the set of support strategy in theorem proving.*Journal of the Association for Computing Machines*, pages 536-541, 1965. **108**-
L. Wos, G. Robinson, D. Carson, and L. Shalla.

The concept of demodulation in theorem proving.*Journal of the Association for Computing Machines*, pages 698-709, 1967.