Bibliography

1

R. Butler and R. Overbeek.
A tutorial on the construction of high-performance resolution/paramodulation systems.
Tech. Report ANL-90/30, Argonne National Laboratory, Argonne, IL, 1990.

2

T. Henry and W. McCune.
FORMED: An X Window System application for managing first-order formulas.
Tech. Memo ANL/MCS-TM-141, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, October 1990.

3

A. Jindal, R. Overbeek, and W. Cabot.
Exploitation of parallel processing for implementing high-performance deduction systems.
Journal of Automated Reasoning, 8(1):23-38, 1992.

4

John Kalman.
An itp workbook.
Technical Report ANL-86-56, Argonne National Laboratory, December 1986.

5

D. Knuth and P. Bendix.
Simple word problems in universal algebras.
In J. Leech, editor, Computational Problems in Abstract Algebras. Pergamon Press, 1970.

6

E. Lusk and W. McCune.
Experiments with ROO, a parallel automated deduction system.
Preprint MCS-P254-0791, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.
To appear in Springer-Verlag Lecture Notes in Artificial Intelligence.

7

E. Lusk, W. McCune, and R. Overbeek.
Logic Machine Architecture: Inference mechanisms.
In D. Loveland, editor, Proceedings of the 6th Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 138, pages 85-108, New York, 1982. Springer-Verlag.

8

E. Lusk, W. McCune, and R. Overbeek.
Logic Machine Architecture: Kernel functions.
In D. Loveland, editor, Proceedings of the 6th Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 138, pages 70-84, New York, 1982. Springer-Verlag.

9

E. Lusk, W. McCune, and J. Slaney.
ROO--a parallel theorem prover.
Tech. Memo MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.

10

E. Lusk and R. Overbeek.
Experiments with resolution-based theorem-proving algorithms.
Computers and Mathematics with Application, 8(3):141-152, 1982.

11

E. Lusk and R. Overbeek.
The automated reasoning system ITP.
Tech. Report ANL-84/27, Argonne National Laboratory, Argonne, IL, April 1984.

12

E. Lusk and R. McFadden.
Using automated reasoning tools: A study of the semigroup f2b2.
Semigroup Forum, 36(1):75-88, 1987.

13

J. McCharen, R. Overbeek, and L. Wos.
Problems and experiments for and with automated theorem-proving programs.
IEEE Transactions on Computers, C-25(8):773-782, August 1976.

14

W. McCune.
OTTER 2.0 Users Guide.
Tech. Report ANL-90/9, Argonne National Laboratory, Argonne, IL, March 1990.

15

W. McCune.
Automated discovery of new axiomatizations of the left group and right group calculi.
Preprint MCS-P220-0391, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.
To appear in J. Automated Reasoning.

16

W. McCune.
Experiments with discrimination tree indexing and path indexing for term retrieval.
Preprint MCS-P191-1190, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.
Invited paper, to appear in J. of Automated Reasoning.

17

W. McCune.
Single axioms for the left group and right group calculi.
Preprint MCS-P219-0391, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.

18

W. McCune.
What's New in OTTER 2.2.
Tech. Memo ANL/MCS-TM-153, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, July 1991.

19

W. McCune and L. Wos.
The absence and the presence of fixed point combinators.
Theoretical Computer Science, 87:221-228, 1991.

20

R. Overbeek.
A new class of automated theorem-proving algorithms.
Journal of the ACM, 21:191-200, 1974.

21

R. Overbeek.
An implementation of hyper-resolution.
Computers and Mathematics with Applications, 1:201-214, 1975.

22

G. Robinson and L. Wos.
Paramodulation and theorem-proving in first-order theories with equality.
In D. Michie and R. Meltzer, editors, Machine Intelligence, Vol. IV, pages 135-150. Edinburg U. Press, 1969.

23

J. Slaney.
FINDER, finite domain enumerator: Version 1.0 notes and guide.
Tech. Report TR-ARP-10/91, Automated Reasoning Project, Australian National University, Canberra, Australia, 1991.

24

J. Slaney and E. Lusk.
Parallelizing the closure computation in automated deduction.
In M. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 449, pages 28-39, New York, July 1990. Springer-Verlag.

25

S. Winker.
Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions.
J. ACM, 29:273-284, 1982.

26

S. Winker, L. Wos, and E. Lusk.
Semigroups, antiautomorphisms, and involutions: A computer solution to an open problem, I.
Math. of Comp., 37:533-545, 1981.

27

L. Wos, D. Carson, and G. Robinson.
The unit preference strategy in theorem proving.
In Proceedings of the Fall Joint Computer Conferenc, pages 615-62, New York, 1964. Thompson Book Compan.

28

L. Wos, R. Overbeek, E. Lusk, and J. Boyle.
Automated Reasoning: Introduction and Applications.
McGraw-Hill, second edition, 1992.

29

L. Wos, G. Robinson, and D. Carson.
Efficiency and completeness of the set of support strategy in theorem proving.
J. ACM, 12(4):536-541, 1965.

30

L. Wos, S. Winker, and E. Lusk.
An automated reasoning system.
In Proceedings of the AFIPS National Computer Conference, pages 697-702, 1981.

31

L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler.
Automated reasoning contributes to mathematics and logic.
In M. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 449, pages 485-499, New York, July 1990. Springer-Verlag.

32

L. Wos, S. Winker, B. Smith, R. Veroff, and L. Henschen.
A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains.
Artificial Intelligence, 22:303-356, 1984.