| dc.contributor.author | Bailhache, Patrice | |
| dc.date.accessioned | 2015-05-15T13:15:18Z | |
| dc.date.available | 2015-05-15T13:15:18Z | |
| dc.date.issued | 1993 | |
| dc.identifier.issn | 0208-6107 | |
| dc.identifier.uri | http://hdl.handle.net/11089/8844 | |
| dc.description.abstract | 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. | pl_PL |
| dc.description.sponsorship | Zadanie pt. „Digitalizacja i udostępnienie w Cyfrowym Repozytorium Uniwersytetu Łódzkiego kolekcji czasopism naukowych wydawanych przez Uniwersytet Łódzki” nr 885/P-DUN/2014 dofinansowane zostało ze środków MNiSW w ramach działalności upowszechniającej naukę. | pl_PL |
| dc.language.iso | fr | pl_PL |
| dc.publisher | Wydawnictwo Uniwersytetu Łódzkiego | pl_PL |
| dc.relation.ispartofseries | Acta Universitatis Lodziensis. Folia Philosophica;9 | |
| dc.title | A la recherche d'un (impossible) démonstrateur intelligent | pl_PL |
| dc.title.alternative | Poszukiwanie procedury inteligentnego dowodzenia twierdzeń | pl_PL |
| dc.type | Article | pl_PL |
| dc.page.number | 133-144 | pl_PL |
| dc.contributor.authorAffiliation | Université de Nantes, France | pl_PL |
