References

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²⁰ 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.