A la recherche d'un (impossible) démonstrateur intelligent
Streszczenie
W ostatnich latach wraz z rozwojem nauk komputerowych, pojawiło się wiele programów
mających wspomagać nauczanie logiki. Większość z tych programowań sluż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.