PL EN


1993 | 09 |
Article title

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

Content
Title variants
FR
Poszukiwanie procedury inteligentnego dowodzenia twierdzeń
Languages of publication
Abstracts
PL
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.
Keywords
References
Document Type
Publication order reference
Identifiers
URI
http://hdl.handle.net/11089/8844
YADDA identifier
bwmeta1.element.hdl_11089_8844
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.