System wspomagający dowodzenie twierdzeń

Ten artykuł od 2011-06 wymaga zweryfikowania podanych informacji.

Należy podać wiarygodne źródła w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

System wspomagający dowodzenie twierdzeń (ang. proof assistant, interactive theorem prover) – program komputerowy pozwalający użytkownikowi na zapis wyrażeń i formuł matematycznych oraz pomagający przy przeprowadzaniu ich dowodu. W ogólności automatyczne dowodzenie twierdzeń jest niemożliwe, gdyż dla wielu logik pytanie, czy dana formuła ma dowód jest nierozstrzygalne, dlatego provery zazwyczaj tylko asystują użytkownikowi przy przeprowadzaniu dowodu i weryfikują, czy użytkownik nie wykonuje niedozwolonych operacji. Zwykle potrafią również znaleźć dowody dla prostych faktów lub udzielić użytkownikowi wskazówek, które drogi rozumowania mogą doprowadzić do wyniku, niemniej ich moc jest ograniczona.

Przykładowe provery: