Automatsko dokazivanje teorema
From Wikipedia, the free encyclopedia
Automatsko dokazivanje teorema (takođe poznato kao automatizovana dedukcija) je podoblast automatskog zaključivanja i matematičke logike koja se bavi dokazivanjem matematičkih teorema pomoću kompjuterskih programa. Automatsko rezonovanje o matematičkom dokazu bilo je glavni podsticaj za razvoj računarske nauke.