[stextbox id=”info” caption=”Abstrakt”]<\/p>\n
Odczyt jest pr\u00f3b\u0105 odpowiedzi, w jakim zakresie rozumowania ogl\u0105dowe<\/em> poddaj\u0105 si\u0119 formalizacji i automatyzacji. Argumentuje si\u0119 (wbrew behawiorystom, nominalistom etc.), \u017ce istniej\u0105 r.ogl\u0105dowe czyli takie, kt\u00f3re polegaj\u0105 na uzyskiwaniu wniosk\u00f3w w wyniku my\u015blowego przetwarzaniu obraz\u00f3w, nie daj\u0105c si\u0119 w pe\u0142ni wyrazi\u0107 jako tekstowe<\/em>, tj. teksty w kt\u00f3rym\u015b z j\u0119zyk\u00f3w potocznych lub symbolicznych; te drugie to j\u0119zyki sformalizowane za pomoc\u0105 symboliki logicznej. R.ogl\u0105dowe ca\u0142kowicie pozbawione mo\u017cliwo\u015bci utekstowienia (tj. wyra\u017cenia w tek\u015bcie) s\u0105 charakterystyczne dla zwierz\u0105t, a r.tekstowe nie maj\u0105ce oparcia w ogl\u0105dowych s\u0105 charakterystyczne dla komputer\u00f3w.<\/p>\n Jak przekszta\u0142ci\u0107 rozumowanie ogl\u0105dowe R0 w r.zautomatyzowane w procedurze automatycznej weryfikacji (por. anons J.Goli\u0144skiej-Pilarek)? Oto kolejne kroki. (1) Stworzy\u0107 \u015brodki wyrazu w okre\u015blonym j\u0119zyku potocznym<\/em> przekszta\u0142caj\u0105ce R0 w r.tekstowe R1 w tym j\u0119zyku (tak Euklides wyrazi\u0142 ogl\u0105dowe r.geometryczne w potocznej grece). (2) Przekszta\u0142ci\u0107 R1 w r.sformalizowane<\/em> R2 przez zapis w j\u0119zyku symbolicznym stosownego systemu logiki (jak D.Hilbert w logice predykat\u00f3w). (3) zapisa\u0107 R2 jako R3 – formu\u0142\u0119 w j\u0119zyku podatnym na przetwarzanie formu\u0142 przez program automatycznej weryfikacji twierdze\u0144 — checker<\/em> (np. „Mizar” A.Trybulca).<\/p>\n Analogiczna, mutatis mutandis<\/em>, jest procedura automatycznego dowodzenia. Po zapisaniu formu\u0142y dowodzonej w odpowiednim j\u0119zyku programowania<\/em> (np. Lisp) dowodzi jej program typu prover<\/em> (np. „Boyer-Moore theorem prover”).<\/p>\n Zakres r.ogl\u0105dowych poddaj\u0105cych si\u0119 formalizacji poszerza si\u0119 dzi\u0119ki sukcesywnemu zwi\u0119kszaniu zaanga\u017cowania ontologicznego<\/em> j\u0119zyk\u00f3w sformalizowanych u\u017cytych do utekstowienia r.ogl\u0105dowych. Ogniwem po\u015brednicz\u0105cym s\u0105 j\u0119zyki potoczne o podobnym zaanga\u017cowaniu w ontologi\u0119; np. greka u\u017cywana przez Euklidesa anga\u017cuje w uznanie istnienia takich obiekt\u00f3w jak punkty, co zostaje odtworzone w formalizacji geometrii przez Hilberta dokonanej w logice predykat\u00f3w<\/em>. Przyk\u0142ady logik o wi\u0119kszym (ni\u017c rachunek klasyczny) zaanga\u017cowaniu ontologicznym: modalna, deontyczna, epistemiczna, dynamiczna, logiki wy\u017cszych rz\u0119d\u00f3w itp. Ten rodzaj zaanga\u017cowania jest istot\u0105 obecno\u015bci filozofii w logice<\/em>, a na ile logika wspiera informatyk\u0119 – obecno\u015bci filozofii w informatyce.<\/em> [stextbox id=”warning”]Ewentualne uwagi mog\u0105ce pom\u00f3c autorowi w pracy prosz\u0119 „mejlowa\u0107” na adres: witold@marciszewski.eu[\/stextbox]<\/p>\n \n","protected":false},"excerpt":{"rendered":" [stextbox id=”info” caption=”Abstrakt”] Odczyt jest pr\u00f3b\u0105 odpowiedzi, w jakim zakresie rozumowania ogl\u0105dowe poddaj\u0105 si\u0119 formalizacji i automatyzacji. Argumentuje si\u0119 (wbrew behawiorystom, nominalistom etc.), \u017ce istniej\u0105 r.ogl\u0105dowe czyli takie, kt\u00f3re polegaj\u0105 na uzyskiwaniu wniosk\u00f3w w wyniku my\u015blowego przetwarzaniu obraz\u00f3w, nie daj\u0105c … Czytaj dalej
\n[\/stextbox]<\/p>\n