Witold Marciszewski (UwB)
Rozumowania oglądowe a rozumowania sformalizowane

Abstrakt

Odczyt jest próbą odpowiedzi, w jakim zakresie rozumowania oglądowe poddają się formalizacji i automatyzacji. Argumentuje się (wbrew behawiorystom, nominalistom etc.), że istnieją r.oglądowe czyli takie, które polegają na uzyskiwaniu wniosków w wyniku myślowego przetwarzaniu obrazów, nie dając się w pełni wyrazić jako tekstowe, tj. teksty w którymś z języków potocznych lub symbolicznych; te drugie to języki sformalizowane za pomocą symboliki logicznej. R.oglądowe całkowicie pozbawione możliwości utekstowienia (tj. wyrażenia w tekście) są charakterystyczne dla zwierząt, a r.tekstowe nie mające oparcia w oglądowych są charakterystyczne dla komputerów.

Jak przekształcić rozumowanie oglądowe R0 w r.zautomatyzowane w procedurze automatycznej weryfikacji (por. anons J.Golińskiej-Pilarek)? Oto kolejne kroki. (1) Stworzyć środki wyrazu w określonym języku potocznym przekształcające R0 w r.tekstowe R1 w tym języku (tak Euklides wyraził oglądowe r.geometryczne w potocznej grece). (2) Przekształcić R1 w r.sformalizowane R2 przez zapis w języku symbolicznym stosownego systemu logiki (jak D.Hilbert w logice predykatów). (3) zapisać R2 jako R3 – formułę w języku podatnym na przetwarzanie formuł przez program automatycznej weryfikacji twierdzeń — checker (np. „Mizar” A.Trybulca).

Analogiczna, mutatis mutandis, jest procedura automatycznego dowodzenia. Po zapisaniu formuły dowodzonej w odpowiednim języku programowania (np. Lisp) dowodzi jej program typu prover (np. „Boyer-Moore theorem prover”).

Zakres r.oglądowych poddających się formalizacji poszerza się dzięki sukcesywnemu zwiększaniu zaangażowania ontologicznego języków sformalizowanych użytych do utekstowienia r.oglądowych. Ogniwem pośredniczącym są języki potoczne o podobnym zaangażowaniu w ontologię; np. greka używana przez Euklidesa angażuje w uznanie istnienia takich obiektów jak punkty, co zostaje odtworzone w formalizacji geometrii przez Hilberta dokonanej w logice predykatów. Przykłady logik o większym (niż rachunek klasyczny) zaangażowaniu ontologicznym: modalna, deontyczna, epistemiczna, dynamiczna, logiki wyższych rzędów itp. Ten rodzaj zaangażowania jest istotą obecności filozofii w logice, a na ile logika wspiera informatykę – obecności filozofii w informatyce.

Ewentualne uwagi mogące pomóc autorowi w pracy proszę „mejlować” na adres: witold@marciszewski.eu

6 odpowiedzi na „Witold Marciszewski (UwB)
Rozumowania oglądowe a rozumowania sformalizowane

Dodaj komentarz

Twój adres e-mail nie zostanie opublikowany. Wymagane pola są oznaczone *