DISCUSSING GRAPH THEORY WITH A COMPUTER III, MAN--MACHINE THEOREM PROVING

Drago\v s M. Cvetkovi\'c and Irena Pevac

Abstract: 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.

Classification (MSC2000): 68G15; 03B35; 05C99

Full text of the article:

• Compressed PostScript file (180 kilobytes)
• PDF file (544 kilobytes)