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

• Authors: Bailhache, Patrice

Title variants

FR

Poszukiwanie procedury inteligentnego dowodzenia twierdzeń

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.

• Publisher: Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
• Journal: Acta Universitatis Lodziensis. Folia Philosophica. Ethica – Aesthetica – Practica
• Year: 1993
• Volume: 09

Dates

published

1993

Contributors

author

Bailhache, Patrice

other

Université de Nantes, France

Identifiers

URI

http://hdl.handle.net/11089/8844