Geodesic
Some Heuristics in Automatic Theorem Proving
Publications de l'Institut Mathématique, _N_S_35 (1984) no. 49, p. 167 .

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

We propose two heuristics in automatic theorem proving: an analogy heuristic and a heurietic for detecting the logical equivalence of formulas. The first heuristic tries to establish an analogy between some subtheories of two non-analogous theories and to prove in this way a formula in one theory using a theorem in the second one. The second heuristic is related to the case when one should establish the logical equivalence of two formulas by instantiation of definitions. The structure of the definition set is represented by a digraph and a digraph coloring language is used.
Classification : 68G15 
@article{PIM_1984_N_S_35_49_a22,
     author = {Drago\v{s} Cvetkovi\'c and Irena Pevac},
     title = {Some {Heuristics} in {Automatic} {Theorem} {Proving}},
     journal = {Publications de l'Institut Math\'ematique},
     pages = {167 },
     publisher = {mathdoc},
     volume = {_N_S_35},
     number = {49},
     year = {1984},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/PIM_1984_N_S_35_49_a22/}
}
TY  - JOUR
AU  - Dragoš Cvetković
AU  - Irena Pevac
TI  - Some Heuristics in Automatic Theorem Proving
JO  - Publications de l'Institut Mathématique
PY  - 1984
SP  - 167 
VL  - _N_S_35
IS  - 49
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PIM_1984_N_S_35_49_a22/
LA  - en
ID  - PIM_1984_N_S_35_49_a22
ER  - 
%0 Journal Article
%A Dragoš Cvetković
%A Irena Pevac
%T Some Heuristics in Automatic Theorem Proving
%J Publications de l'Institut Mathématique
%D 1984
%P 167 
%V _N_S_35
%N 49
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PIM_1984_N_S_35_49_a22/
%G en
%F PIM_1984_N_S_35_49_a22
Dragoš Cvetković; Irena Pevac. Some Heuristics in Automatic Theorem Proving. Publications de l'Institut Mathématique, _N_S_35 (1984) no. 49, p. 167 . http://geodesic.mathdoc.fr/item/PIM_1984_N_S_35_49_a22/