System wspomagający dowodzenie twierdzeń

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:

• Coq
• Isabelle
• LEGO
• Mizar
• Prototype Verification System (PVS)

Przykładowe dowody używające proverów:

• twierdzenie o czterech barwach
• Postulat Keplera