System wspomagający dowodzenie twierdzeń

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

System wspomagający dowodzenie twierdzeń (ang. 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 mocno ograniczona.

Przykładowe provery:

Zobacz też[edytuj | edytuj kod]