The interactive programming system ``Graph'' for the classification and extension of knowledge in the field of graph theory has recently been implemented at the University of Belgrade, Faculty of Electrical Engineereing. System ``Graph'' consists of a computerized graph theory bibliography, a system for graph theoretic alorithms and a mechanical theorem prover. This paper describes the theorem prover of the system ``Graph''. The main features of the prover are: formalization of graph theory by a first order calculus, well organized files of definitions and lemmas, both interactive (natural deduction) and non-interactive (resolution) work, usage of analogies, man-machine communication by natural language (including sentences to be proved), possibility to use graph theoretic alogithms to prove statements about concrete graphs or to check conjectures on particular graphs including random graphs.