Geodesic
Discussing Graph Theory with a Computer III, Man-machine Theorem Proving
Publications de l'Institut Mathématique, _N_S_34 (1983) no. 48, p. 37 .

Voir la notice de l'article provenant de la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts

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 : 68G15 03B35 05C99 
@article{PIM_1983_N_S_34_48_a6,
     author = {Drago\v{s} M. Cvetkovi\'c and Irena Pevac},
     title = {Discussing {Graph} {Theory} with a {Computer} {III,} {Man-machine} {Theorem} {Proving}},
     journal = {Publications de l'Institut Math\'ematique},
     pages = {37 },
     publisher = {mathdoc},
     volume = {_N_S_34},
     number = {48},
     year = {1983},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/PIM_1983_N_S_34_48_a6/}
}
TY  - JOUR
AU  - Dragoš M. Cvetković
AU  - Irena Pevac
TI  - Discussing Graph Theory with a Computer III, Man-machine Theorem Proving
JO  - Publications de l'Institut Mathématique
PY  - 1983
SP  - 37 
VL  - _N_S_34
IS  - 48
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PIM_1983_N_S_34_48_a6/
LA  - en
ID  - PIM_1983_N_S_34_48_a6
ER  - 
%0 Journal Article
%A Dragoš M. Cvetković
%A Irena Pevac
%T Discussing Graph Theory with a Computer III, Man-machine Theorem Proving
%J Publications de l'Institut Mathématique
%D 1983
%P 37 
%V _N_S_34
%N 48
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PIM_1983_N_S_34_48_a6/
%G en
%F PIM_1983_N_S_34_48_a6
Dragoš M. Cvetković; Irena Pevac. Discussing Graph Theory with a Computer III, Man-machine Theorem Proving. Publications de l'Institut Mathématique, _N_S_34 (1983) no. 48, p. 37 . http://geodesic.mathdoc.fr/item/PIM_1983_N_S_34_48_a6/