EMIS ELibM Electronic Journals PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.)
Vol. 33(47), pp. 89--95 (1983)

Previous Article

Next Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home

EMIS Home

 		 

SPOSOB VSTROENIYA PRAVILA INDUKCII V PROCEDURY AVTOMATICHESKOGO DOKAZATEL'STVA TEOREM S REZOLYUCIEI

Petar Z. Hotomski

Pedagoska akademija, 22000 Sremska Mitrovica, Jugoslavija

Abstract: V nastoyashchei rabote osushchstvlyaet\1sya 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.

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
© 2001 ELibM for the EMIS Electronic Edition