2091577363

ne umożliwiło Johniakowi śledzenie tylko łańcuchów logicznych, które prowadziły do uzyskania poprawnego dowodu, przy czym kolejne kroki były wykonywane z wystarczająco dużym prawdopodobieństwem. W ten sposób komputer wzniósł się ponad dotychczasowy poziom mechanicznego rozwiązywania problemów, a jego praca nabrała subtelności i mogła świadczyć o posiadaniu czegoś w rodzaju intuicji. Wytłumaczenie istoty tego zjawiska wymagałoby przedtem obszernego wykładu z programowania, a następnie śledzenia programu Joh-niaka rozkaz po rozkazie. Ponieważ niniejsza książka nie jest encyklopedią informatyki — poprzestaniemy tu jedynie na obserwacji rezultatów działania programów. Wnikanie w ich naturę wymagałoby bowiem osobnej publikacji.

„Maszyna” została użyta do dowodzenia twierdzeń logiki formalnej (rachunku zdań) opartych na zadanych aksjomatach i regułach wnioskowania. Swoje umiejętności potwierdziła dowodząc 38 z 52 twierdzeń umieszczonych w drugim rozdziale książki B. Russela i A. N. Whiteheada Principia Mathematica. Z twierdzeniem

(p implikuje nie p) implikuje nie p uporała się w 10 sekund, a

7iie (p lub q) implikuje nie p zajęło jej 12 minut. Przy dowodzeniu twierdzenia

p lub (q lub r) implikuje (p lub q) lub r dała jednak za wygraną po 23 minutach.

Napisanie programu, choć nie heurystycznego, zdolnego udowodnić wszystkie zawarte w Principia Mathematica twierdzenia, udało się w trzy lata później H. Wangowi.¹ Zastosował

59

1

H. Wang, Toward Mechanical Mathematics, IBM Journal of Research and Development 1960.