Geodesic
Sposob Vstroeniya Pravila Indukcii v Procedury Avtomaticheskogo Dokazatel'stva Teorem s Rezolyuciei
Publications de l'Institut Mathématique, _N_S_33 (1983) no. 47, p. 89 
Petar Z. Hotomski. Sposob Vstroeniya Pravila Indukcii v Procedury Avtomaticheskogo Dokazatel'stva Teorem s Rezolyuciei. Publications de l'Institut Mathématique, _N_S_33 (1983) no. 47, p. 89 . http://geodesic.mathdoc.fr/item/PIM_1983_N_S_33_47_a12/
@article{PIM_1983_N_S_33_47_a12,
     author = {Petar Z. Hotomski},
     title = {Sposob {Vstroeniya} {Pravila} {Indukcii} v {Procedury} {Avtomaticheskogo} {Dokazatel'stva} {Teorem} s {Rezolyuciei}},
     journal = {Publications de l'Institut Math\'ematique},
     pages = {89 },
     year = {1983},
     volume = {_N_S_33},
     number = {47},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/PIM_1983_N_S_33_47_a12/}
}
TY  - JOUR
AU  - Petar Z. Hotomski
TI  - Sposob Vstroeniya Pravila Indukcii v Procedury Avtomaticheskogo Dokazatel'stva Teorem s Rezolyuciei
JO  - Publications de l'Institut Mathématique
PY  - 1983
SP  - 89 
VL  - _N_S_33
IS  - 47
UR  - http://geodesic.mathdoc.fr/item/PIM_1983_N_S_33_47_a12/
LA  - en
ID  - PIM_1983_N_S_33_47_a12
ER  - 
%0 Journal Article
%A Petar Z. Hotomski
%T Sposob Vstroeniya Pravila Indukcii v Procedury Avtomaticheskogo Dokazatel'stva Teorem s Rezolyuciei
%J Publications de l'Institut Mathématique
%D 1983
%P 89 
%V _N_S_33
%N 47
%U http://geodesic.mathdoc.fr/item/PIM_1983_N_S_33_47_a12/
%G en
%F PIM_1983_N_S_33_47_a12

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

V nastoyashchei rabote osushchstvlyaetsya vklyuchenie pravila binarnoi indukcii, opisannogo v [1], v avtomaticheskie procedury oproverzheniya v teoriyah pervogo poryadka. Privodit\-sya modificirovannyi algoritm unifikacii dlya otyskaniya podstanovki kotoraya potrebuet\-sya dlya primenjeniya pravila binarnoi indukcii. Rassmatrivaet\-sya algoritm poiska oproverzheniya s rezolyuciei i pravilom binarnoi indukcii v teoriyah pervogo poryadka s matematicheskoi indukciei. Privodit\-sya svedeniya o programmnoi sisteme i rezul'tatah otladki na evm.