Automatyczne dowodzenie twierdzeń
Z Wikipedii, wolnej encyclopedia
Automatyczne dowodzenie twierdzeń (ang. automated theorem proving) – proces, w którym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiejś teorii, często przy okazji generując jego dowód. Twierdzenia te należą zwykle do rachunku zdań lub rachunku predykatów pierwszego rzędu.
Dla komputera wygodniejsze jest zwykle wnioskowanie w tył, choć czasem stosuje się też wnioskowanie w przód.
Przykładem twierdzenia, które zostało dowiedzione dopiero przez ATP jest "Algebry Robbinsa są boolowskie"[1].