6428 George Andrews: The death of a proof? Semi-rigorous mathematics? You've
got to be kidding! Math. Intell. 16/4 (1994), 16-18.

8765 Wolfgang Bibel: Automated theorem proving. Vieweg 1982.

5822 Alan Bundy: L'automazione del ragionamento matematico. Muzzio 1986.

B. Cipra: Theoretical computer scientists develop transparent proof techniques.
SIAM News 25 (1992), ...

13548 Francesco De Giovanni/Tommaso Landolfi: Le dimostrazioni di teoremi
fondate sull'uso dei calcolatori. Boll. UMI 2-A (1999), 69-81.

M. Fitting: First-order logic and automated theorem proving.
Springer 1990, 240p. "Nowadays, if you wish to learn logic proper, you had
better look at the computer science shelves in the bookstore. What goes by
the name of logic has painted itself into a number of unpleasant corners
(set theory, large cardinals, independence proofs) which make it the branch
of mathematics which is currently farthest removed from what we believe to
be mainstream logic. In this book, the author once more shows himself to be
one of the masters of logic exposition." (Giancarlo Rota).

Georg Gottlob a.o. (ed.): Computational logic and proof theory.
Springer LN CS 1289 (1997).

20817 Thomas Hales: Formal proof. Notices AMS December 2008, 1370-1380.

20819 John Harrison: Formal proof - theory and practice.
Notices AMS December 2008, 1395-1406.

1518 Dieter Hofbauer/Ralf-Detlef Kutsche: Grundlagen des maschinellen
Beweisens. Vieweg 1989.

5728 John Horgan: Der Tod des Beweises. Spektrum 1993/12, 88-101.

824 Robert Kowalski: Logic for problem solving. North-Holland 1979.

5151 Clement Lam: How reliable is a computer-based proof?
Math. Intell. 12/1 (1990), 8-12.

A. Leitsch: The resolution calculus.
Springer 1997, 300p. 3-540-61882-1. DM 58.

D. Loveland: Automated theorem proving. North-Holland 1978.

D. Loveland: Automated theorem proving - a quarter century review.
Duke Univ. ... (1984), ...

5613 Edward Nelson: Taking formalism seriously.
Math. Intell. 15/3 (1993), 8-11. There will be data banks of theorems,
arranged hierarchically to facilitate search by mathematicians attempting
to prove new theorems. Interactive programs will be developed to help us
construct fully formalized proofs, and when these are submitted, they will
be verified and entered into the data bank with the name of the inventor
and date of construction. The author has written a proof-checking program
called qed, written in perl. It is available as pub/qed.tar.Z by anonymous
ftp from math.princeton.edu.

S. Nigiyan: Modification of the Robinson resolution method for built-in
predicates. J. Cont. Math. Anal. Arm. Ac. Sci. 31/5 (1996), 49-58.

10316 Christoph Po''ppe: Der erste ernstzunehmende Computerbeweis.
Spektrum 1997/8, 32-36.

5729 Konrad Polthier: Computerexperimente in der Mathematik.
Spektrum 1993/12, 94-95.

R.M. Robinson: An essentially undecidable axiom system.
Proc. Int. Cong. Math. 1950, Vol. I, 729-730.

22043 Carlos Simpson: Computer theorem proving in math.
Internet ca. 2003, 40p.

W. Snyder: A proof theory for general unification.
Birkha''user 1991, 190p. 3-7643-3593-9. 

Rolf Socher-Ambrosius: Deduktionssysteme. 
Bibl. Inst. 1994, 180p. 3-411-17171-5. DM 38.

Tanel Tammet: Resolution, inverse method and the sequent calculus.
In Gottlob a.o. 1997, 65-83.

20820 Freek Wiedijk: Formal proof - getting started.
Notices AMS December 2008, 1408-1414.

Herbert Wilf: Billions and billions of combinatorial identities.
Talk at Allerton Park in the Conference in Honour of Paul Bateman,
25-27 April 1989.

W. Wu: Mechanical theorem proving in geometries.
Springer 1994, 300p. 3-211-82506-1. DM 98.

Doron Zeilberger: The method of creative telescoping.
J. Symbolic Computing 11 (1991), 195-204.