Title variants
Poszukiwanie procedury inteligentnego dowodzenia twierdzeń
Languages of publication
Abstracts
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
Publisher
Year
Volume
Physical description
Dates
published
1993
Contributors
author
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.