A la recherche d'un (impossible) démonstrateur intelligent

Abstrakt

W ostatnich latach wraz z rozwojem nauk komputerowych, pojawiło się wiele programów mających wspomagać nauczanie logiki. Większość z tych programowań służy do sprawdzania rachunków, a nic do dowodzenia twierdzeń, ponieważ zgodnie ze znanym twierdzeniem Godła, nie istnieje procedura rozstrzygalności twierdzeń rachunku pierwszego rzędu. Kilka metatwierdzeń, w których jednym jest twierdzenie Godła, tłumaczy dlaczego dysponujemy dobrymi systemami dedukcji naturalnej, mimo że tak trudno jest (a faktycznie nie można) znaleźć „inteligentną" procedurę dowodzenia formuł. W artykule przedstawiono drogę uzyskania częściowego systemu dowodzenia twierdzeń za pomocą procedury unifikacji, dla której załączono program komputerowy w języku pascal.