PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 34(48), pp. 37--47 (1983)
DISCUSSING GRAPH THEORY WITH A COMPUTER III, MAN--MACHINE THEOREM PROVING
Drago\v s M. Cvetkovi\'c and Irena PevacElektrotehnicki fakultet, Beograd, Yugoslavia and Matematicki institut SANU, Beograd, Yugoslavia
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:
Electronic fulltext finalized on: 3 Nov 2001. This page was last modified: 16 Nov 2001.
© 2001 Mathematical Institute of the Serbian Academy of Science and Arts