Wskaźniki dla logicznych aplikacji CS

Jestem studentem matematyki z solidnym doświadczeniem w logice. Wziąłem roczny kurs magisterski z logiki wraz z kursami absolwentów teorii modeli skończonych, a także teorii wymuszania i teorii mnożenia. Większość tekstów CS wydaje się przyjmować jedynie bardzo skromne tło logiki, które w większości obejmuje podstawy logiki zdań i logiki pierwszego rzędu.

Chciałbym uzyskać kilka wskazówek, gdzie szukać aplikacji CS, w których wykorzystuje się cięższy materiał z logiki. Jednym z moich zainteresowań byłaby teoria typów i ogólnie metody formalne. Czy ktoś mógłby zasugerować dobre lektury po wstępnych książkach na temat sprawdzania modeli i języków programowania?

Krótko przejrzałem niektóre obszary tutaj, starając się skupić na pomysłach, które mogłyby spodobać się komuś z doświadczeniem w zaawansowanej logice matematycznej.

Teoria modeli skończonych

Najprostszym ograniczeniem klasycznej teorii modeli z punktu widzenia informatyki jest badanie struktur w skończonym wszechświecie. Struktury te występują w postaci relacyjnych baz danych, wykresów i innych obiektów kombinatorycznych pojawiających się wszędzie w informatyce. Pierwsza obserwacja jest taka, że ​​kilka podstawowych twierdzeń teorii modeli pierwszego rzędu zawodzi, gdy ogranicza się do modeli skończonych. Należą do nich twierdzenie zwartości, twierdzenie o kompletności Godela i konstrukcje ultraproduktowe. Trakhtenbrot pokazał, że w przeciwieństwie do klasycznej logiki pierwszego rzędu, satysfakcja z modeli skończonych jest nierozstrzygalna.

Podstawowymi narzędziami w tym obszarze są miejscowość Hanf, miejscowość Gaifmana oraz liczne odmiany gier Ehrenfeucht-Fraisse. Badane tematy obejmują logikę nieskończoną, logikę z liczeniem, logikę punktu stałego itp. Zawsze ze szczególnym uwzględnieniem modeli skończonych. Trwają prace nad ekspresją w fragmentach logiki pierwszego rzędu o zmiennej skończonej i logiki te charakteryzują się poprzez gry żwirowe. Kolejnym kierunkiem dociekań jest identyfikacja właściwości klasycznej logiki, które przetrwają ograniczenie do modeli skończonych. Niedawny wynik Rossmana w tym kierunku pokazuje, że pewne twierdzenia o zachowaniu homomorfizmu nadal mają zastosowanie do modeli skończonych.

1. Teoria modeli skończonych , Ebbinghaus i Flum
2. Elementy teorii modeli skończonych , Libkin
3. O zwycięskich strategiach w grach Ehrenfeucht-Fraisse , Arora i Fagin, 1997.
4. Twierdzenia o zachowaniu homomorfizmu , Rossman

Zdanie rachunek różniczkowy$\mu$

Linia prac z końca lat 60. pokazała, że ​​liczne właściwości programów można wyrazić w rozszerzeniach logiki zdań, które wspierają rozumowanie na temat punktów stałych. Rachunek modalny jest jedną logiką opracowaną w tym okresie, która znalazła szeroki zakres zastosowań w zautomatyzowanych metodach formalnych. Wiele formalnych metod jest związanych z logiką czasową lub logiką typu Hoare'a i wiele z nich można rozpatrywać w kategoriach μ- rachunku różniczkowego. W rzeczywistości słyszałem, że powiedziano, że μ- calculus jest językiem asemblera logiki czasowej.$\mu$$\mu$$\mu$

W swoim artykule wprowadzającym $\mu$ calculus Kozen dał aksjatyzację i tylko udowodnił, że jest solidny i kompletny dla ograniczonego fragmentu logiki. Dowód kompletności był jednym z wielkich otwartych problemów w logicznej informatyce, dopóki Walukiewicz nie podał dowodu (opartego na nieskończonych automatach). Modelowa teoria rachunku ma wiele bogatych wyników. Podobnie jak twierdzenie van Benthema o logice modalnej, Janin i Walukiewicz udowodnili, że μ- rachunek jest wyraźnie równoważny bisimulacyjnemu niezmiennemu fragmentowi monadycznej logiki drugiego rzędu. $\mu$$\mu$$\mu$-kalkulus został również scharakteryzowany pod względem gier parzystości i automatów nad nieskończonymi drzewami. Problemem satysfakcji dla tej logiki jest WYŁĄCZENIE, a Emerson i Jutla wykazali, że logika ma właściwość małego modelu. Bradfield wykazał, że hierarchia przemian rachunku jest ścisła, podczas gdy Berwanger wykazał, że hierarchia zmiennych jest również ścisła. Ważnymi klasycznymi narzędziami stosowanymi w tym obszarze są twierdzenie Rabina i twierdzenie Martina.$\mu$

1. Wyniki na zdaniu calculus$\mu$ , Kozen, 1983
2. Podstawy -calculus$\mu$ Arnold i Niwinski, 2001
3. Kompletność aksomatyzacji Kozen'a twierdzenia Calculus$\mu$ , Walukiewicz 1995
4. Logika modalna i calculi$\mu$ , Bradfield i Stirling, 2001
5. Modalna hierarchia przemian mu-rachunek jest ścisła , Bradfield, 1996
6. Zmienna hierarchia rachunku mu jest ścisła , Berwanger, E. Grädel i G. Lenzi, 2005

Liniowa logika czasowa

Liniowa logika czasowa została przejęta z logiki filozoficznej do informatyki w celu uzasadnienia zachowania programów komputerowych. Uznano to za dobrą logikę, ponieważ może wyrażać właściwości takie jak niezmienność (brak błędów) i zakończenie. Teorię logiki czasowej opracowali Manna i Pnueli (i inni później) w swoich artykułach i książkach. Sprawdzenie modelu i problem satysfakcji dla LTL można rozwiązać zarówno za pomocą automatów, jak i nieskończonych słów.

Pnueli udowodnił także podstawowe rezolucje dotyczące LTL w swoim oryginalnym artykule, wprowadzając logikę rozumowania programów. Vardi i Wolper podali znacznie prostszą kompilację formuł LTL do automatów Buchi. Połączenie z logiką czasową doprowadziło do intensywnych badań algorytmów do wydajnego uzyskiwania automatów z LTL oraz do określania i uzupełniania automatów Buchi. Twierdzenie Kampa pokazuje, że LTL z od i do$\omega$$\mu$$\mu$ -calculus w czasie liniowym. W przeciwieństwie do modalnego odpowiednika, hierarchia naprzemiennej zmiany czasu ulega załamaniu na poziomie 2.

1. Czasowa logika programów , Pnueli 1977
2. From Church and Before to PSL , Vardi, 2008
3. Automatyzowane teoretycznie podejście do liniowej logiki czasowej , Vardi i Wolper, 1986
4. Temporalna logika układów reaktywnych i współbieżnych: specyfikacja , manna i pnueli
5. Hierarchia Until i inne zastosowania gry Ehrenfeucht-Fraïssé dla logiki czasowej , Etessami i Wilke, 2000

Logika drzewa obliczeniowego

$\mu$ rachunku. Różnica między LTL i CTL skłoniła Emersona i Halperna do opracowania CTL *, który pozwala na rozumowanie zarówno właściwości stanów, jak i śladów.

Problem sprawdzania modelu CTL w strukturach skończonych dotyczy czasu wielomianowego. Problem sprawdzania modelu dla CTL * jest zakończony WYŁĄCZNIE. Aksjatyzacja CTL * była trudnym otwartym problemem, który ostatecznie został rozwiązany przez Reynoldsa 2001. Analogię twierdzenia van Benthem'a dla logiki modalnej i twierdzenia Kampa dla LTL podano dla CTL * przez twierdzenie Hafera i Thomasa wykazujące, że CTL * odpowiada fragment monadycznej logiki drugiego rzędu nad drzewami binarnymi. Późniejszą charakterystyką Hirschfelda i Rabinovicha jest to, że CTL * jest wyraźnie równoważny bisimulacyjnemu niezmiennemu fragmentowi MSO z kwantyfikacją ścieżki.

1. „Czasami” i „nie nigdy” powrócono: na rozgałęzieniu w porównaniu z liniową logiką czasową , Emerson i Halpern, 1986
2. O mocy ekspresyjnej CTL , Moller, Rabinovich, 1999
3. Logika drzewa obliczeń CTL * i kwantyfikatory ścieżki w monadycznej teorii drzewa binarnego , Hafer i Thomas, 1987
4. Aksjatyzacja pełnej logiki drzewa obliczeniowego , Reynolds, 2001

Języki nieskończonych słów

$\omega$

$\omega$$\omega$$\omega$-słowa. Co więcej, stosując elementarną topologię, wykazali, że każdą właściwość czasu liniowego można wyrazić jako przecięcie właściwości bezpieczeństwa i żywotności. Ten wynik ma znaczące praktyczne konsekwencje, ponieważ oznacza, że ​​zamiast budować złożone kontrolery właściwości, wystarczy zbudować narzędzie sprawdzające bezpieczeństwo i kontrolę żywotności. Dalsza redukcja pokazuje, że wystarczy zbudować moduł sprawdzania niezmienności i moduł sprawdzania zakończenia. Charakterystyka bezpieczeństwa i żywotności została rozszerzona na drzewa przez Manoliosa i Treflera, a ostatnio na zestawy śladów, w ramach hiperpropozycji, przez Clarksona i Schneidera.

1. Infinite Words: Automata, Semigroups, Logic and Games , Perrin and Pin, 2004
2. $\omega$
3. $\omega$ , Bojanczyk, 2010
4. O zgodności syntaktycznej dla ω — języków , Maler i Staiger, 1993

Automaty o nieskończonych słowach

Tam, gdzie są języki, informatycy będą mieli automaty. Wprowadź teorię automatów na nieskończone słowa i nieskończone drzewa. To bardzo smutne, że chociaż automaty nad nieskończonymi słowami pojawiły się w ciągu dwóch lat od automatów na słowach skończonych, ten podstawowy temat rzadko jest ujęty w standardowych programach komputerowych. Automaty nad nieskończonymi słowami i drzewami zapewniają bardzo solidne podejście do udowodnienia zadowalającej satysfakcji dla bardzo bogatej rodziny logiki.

$\omega$

1. Rozstrzygalność teorii drugiego rzędu i automatów na drzewach nieskończonych , Rabin, 1969
2. Automaty o nieskończonych obiektach , Thomas, 1988
3. Automaty: od logiki do algorytmów , Vardi, 2007

Nieskończone gry

Gry logiczne i nieskończone są aktywnym obszarem badań. Pojęcia teoretyczne gier pojawiają się w informatyce wszędzie w dualności między niedeterminizmem a równoległością (naprzemienność), programem i jego środowiskiem, uniwersalną i egzystencjalną kwantyfikacją, modalnością pudełkową i diamentową itp. Gry okazały się świetny sposób na badanie właściwości różnych typów logiki nieklasycznej wymienionych powyżej.

Podobnie jak w przypadku kryteriów akceptacji automatów, mamy różne warunki wygranej dla gier i wiele z nich może być równoważnych. Ponieważ pytałeś o klasyczne wyniki, twierdzenie Borela o determinacji i gry Gale-Stewarta często leżą dyskretnie na tle kilku badanych modeli gier. Jednym z palących pytań naszych czasów była złożoność rozwiązywania gier parzystości. Jurdziński podał algorytm doskonalenia strategii i wykazał, że decyzja o zwycięstwie leży na przecięciu klas złożoności UP i coUP. Dokładna złożoność algorytmu Juryńskiego była otwarta, dopóki Friedmann nie wyznaczył jej dolnej granicy czasu wykładniczego w 2009 roku.

1. Zwycięzca w grach parzystości jest w UP ∩ co-UP , Jurdziński, 1998
2. Gry dla rachunku μ , Niwinski i Walukiewicz, 1996
3. Wykładnicza dolna granica dla algorytmu poprawy strategii gry parzystości, jaką znamy , Friedmann, 2009

Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Sprawdzanie modelu . MIT Press 1999 to fajna książka (dla mnie) na temat sprawdzania modeli.

Glynn Winskel: Formalna semantyka języków programowania: wprowadzenie . MIT Press 1994, jest jednym ze standardowych podręczników na temat języków programowania.

Mordechai Ben-Ari: Logika matematyczna dla informatyki . Springer 2001 to być może to, czego szukasz.

Teoria baz danych to rozległa dziedzina zapewniająca wiele zastosowań logiki. Złożoność opisowa i teoria modeli skończonych są ściśle powiązanymi dziedzinami. O ile mi wiadomo, wszystkie te obszary używają raczej algebraicznych stylów logiki (podążając śladami Birkhoffa i Tarskiego), a nie teorii teoretycznej. Jednak niektóre prace Petera Bunemana , Leonida Libkina , Wenfei Fan , Susan Davidson , Limsoon Wong , Atsushi Ohori i innych badaczy, którzy pracowali w UPenn w latach 80. i 90. XX wieku, miały na celu połączenie teorii języków programowania i baz danych. Wydaje się, że wymaga to wygody w obu stylach logiki. To samo dotyczy nowszej pracy autorstwa Jamesa CheneyaiPhilip Wadler .

Jeśli chodzi o konkretne odniesienia, standardowy podręcznik jest dostępny online w celu wygodnego korzystania z niego:

• Serge Abiteboul, Richard Hull, Victor Vianu. Podstawy baz danych , 1995. http://webdam.inria.fr/Alice/

Niestety nie znam żadnych aktualnych podręczników ani ankiet dotyczących tego szybko zmieniającego się obszaru. Przydały mi się dwie starsze ankiety. Pierwszy,

• Jan Van den Bussche, Zastosowanie pomysłów Alfreda Tarskiego w teorii baz danych , CSL 2001. doi: 10.1007 / 3-540-44802-0_2

pokazuje, jak połączyć kropki między Tarskim a konkretnym podpola, bazami danych ograniczeń. Druga,

• Victor Vianu, Bazy danych i teoria modeli skończonych , złożoność opisowa i modele skończone: Proceedings of DIMACS Workshop, 1996. http://leo.saclay.inria.fr/publifiles/gemo/GemoReport-107.ps.gz

przedstawia teorię baz danych (w stylu z 1996 r.) do teorii modeli skończonych, a proces uwypukla wiele interesujących zastosowań logiki w bazach danych. W przypadku nowszych prac (takich jak teoria XML, proweniencja, modele przesyłania strumieniowego lub bazy danych grafów) rozsądnym podejściem jest czytanie cytowanych prac naukowych.

Michael Huth i Mark Ryan: Logika w informatyce , Cambridge University Press, 2004.

Bardzo polecam tę książkę jako ogólne wprowadzenie do roli logiki w informatyce.

Kluczowym zastosowaniem logiki w CS jest logika programu, zwana także logiką Hoare.

Jednym dobrym sposobem myślenia o logice programów jest postrzeganie ich jako podliczenia teorii mnogości ZFC (lub jakiejkolwiek innej preferowanej podstawy matematyki, np. Logiki drugiego rzędu), która jest wystarczająco ekspresyjna, aby uzasadniać programy w danym zadaniu język programowania, ale nie więcej. Zawsze możesz argumentować o programach w teorii zbiorów ZFC, ale teoria zbiorów ma zbyt dużą moc ekspresyjną w tym sensie, że zawiera wiele formuł, które tak naprawdę nie są odpowiednie do rozumowania programów (np.$2 \in \sqrt(\pi^{17})$jest prawidłową formułą w ZFC, która może, ale nie musi być prawdą, w zależności od tego, jak kodujesz liczby rzeczywiste jako zestawy). Zbędna moc ekspresyjna jest wadą, gdy myśli się o poprawności programu, ponieważ (nieco upraszczając) zwiększa formułę i wielkość dowodu. Zatem w badaniu logiki programu szukamy logiki o zwięzłych formułach i dowodach.

Podobna sytuacja występuje w badaniu logiki modalnej, która (nieco upraszczając) nie jest tak ekspresyjna jak logika pierwszego rzędu, ale to, co mogą wyrazić, wyrażają się przy użyciu krótszych wzorów i dowodów.

Identyfikacja odpowiednich fragmentów ZFC nie jest trudna dla prostych języków programowania, ale staje się coraz trudniejsza, ponieważ języki programowania zyskują więcej funkcji. W ciągu ostatnich kilku lat odnotowano znaczny postęp w tym przedsięwzięciu.

Artykuł Aksjomatyczne podstawy programowania komputerowego T. autorstwa T. Hoare'a jest często postrzegany jako studium logiki programu na poważnie, jest łatwy do odczytania i prawdopodobnie dobry sposób na rozpoczęcie działalności w terenie. Tę samą logikę opisano bardziej szczegółowo w książce Winskela „Formalna semantyka języków programowania” wymienionej przez @vb le.

Teorię typów można zobaczyć w podobnym świetle. Kluczowym punktem sprzedaży teorii typów jest identyfikacja dowodów za pomocą (czysto funkcjonalnych) programów, co prowadzi do doskonałej ekonomii pojęć i potężnej automatyzacji (w postaci wnioskowania o typie i interaktywnego dowodzenia twierdzeń). Cena za teorię typów, będącą eleganckim sposobem organizowania dowodów, polega na tym, że nie działa ona tak dobrze w przypadku języków programowania, które nie są czysto funkcjonalne.

Najnowszym i na wskroś nowoczesnym tekstem, który wprowadza logikę programu w tonację teoretyczną, są Software Foundations autorstwa Pierce i in. Zaprowadzi Cię on do (a) najnowocześniejszych badań w zakresie weryfikacji programów i, jako podręcznik, prawdopodobnie rzuci okiem na to, w jaki sposób informatyka i matematyka będą nauczane w przyszłości.

Po opracowaniu logiki programu dla języka, następnym krokiem jest automatyzacja lub automatyzacja częściowa: konstruowanie dowodów dla programów nietrywialnych jest pracochłonne i chcielibyśmy, aby maszyny wykonały jak najwięcej. Wiele aktualnych badań formalnych metod związanych z taką automatyzacją.

W informatyce istnieje bardzo silna tradycja logiki. Badane przez nas problemy i estetyka społeczności logiki obliczeniowej nie są identyczne z problemami społeczności logiki matematycznej. Masz całkowitą rację, że znaczące zmiany w teorii modeli, meta-teorii logiki pierwszego rzędu i teorii zbiorów nie są powszechnie stosowane w logice obliczeniowej. Można z powodzeniem badać logiczne obliczenia bez oglądania lub korzystania z ultrafiltrów, niestandardowej analizy, wymuszania, twierdzenia Parisa-Harringtona i wielu innych fascynujących pojęć, które są uważane za ważne w logice klasycznej.

Tak jak ktoś stosuje matematyczne pomysły do ​​studiowania logiki, a także logiczne pomysły do ​​studiowania matematyki, tak my stosujemy logikę do studiowania informatyki, a także stosując perspektywy obliczeniowe do studiowania logiki. Ta odmienna koncentracja ma dość dramatyczne konsekwencje dla rodzajów wyników, które są dla nas ważne.

Oto cytat Johna Baeza na temat logiki i informatyki. Nie mam dokładnie tego samego poglądu, ponieważ nie znam zbytnio zaawansowanej logiki matematycznej.

Kiedy byłem studentem, byłem bardzo zainteresowany logiką i podstawami matematyki --- zawsze szukałem najbardziej oszałamiających koncepcji, jakie mogłem sobie wyobrazić, a twierdzenie Goedela, twierdzenie Loewenheima-Skolema i tak dalej jak na razie, z mechaniką kwantową i ogólną teorią względności. [...] Pamiętam, jak wtedy czułem, że logika stała się mniej rewolucyjna niż na początku stulecia. Wydawało mi się, że logika stała się gałęzią matematyki jak każda inna, badając niejasne właściwości modeli aksjomatów Zermelo-Fraenkela, zamiast kwestionować podstawowe domniemania zawarte w tych aksjomatach i odważać się na nowe, różne podejścia. [...]

W każdym razie jest dla mnie całkiem jasne, że po prostu nie czytałem właściwych rzeczy. Myślę, że Rota powiedział, że naprawdę interesująca praca w logice nosi teraz nazwę „informatyka”, [...] - Tydzień 40, W tym tygodniu, John Baez

Logika w informatyce jest rozległą i szybko rozwijającą się dziedziną. Uważam, że każdą perspektywę klasycznej logiki można modyfikować, aby uzyskać pewne spojrzenie na logikę obliczeniową. Wpis Wikipedii dotyczący logiki matematycznej dzieli pole na teorię zbiorów, teorię modeli, teorię dowodów i teorię rekurencji. Możesz esencjonalnie wziąć te obszary i dodać do nich smak obliczeniowy i uzyskać podpole logiki obliczeniowej.

Teoria modeli Lubimy studiować teorię modeli logiki nieklasycznej i nieklasyczne modele logiki klasycznej. Rozumiem przez to, że badamy logikę modalną, czasową i podstrukturalną oraz że badamy logikę nad drzewami, słowami i modelami skończonymi, w przeciwieństwie do klasycznych modeli takich jak algebry. Dwa podstawowe problemy to satysfakcja i sprawdzenie modelu. Oba mają ogromne znaczenie praktyczne i teoretyczne. Natomiast problemy te są mniej centralne w klasycznej logice.

Teoria dowodu Badamy złożoność i wydajność, z jaką możemy generować dowody w klasycznych systemach dowodów, a także opracowujemy nowe, nieklasyczne systemy dowodów, które są wrażliwe na złożoność i względy wydajności. Zautomatyzowane badania dedukcyjne generowane przez maszynę dowody, generalnie rzecz biorąc. Proces może obejmować interakcję człowieka lub być całkowicie automatyczny. Dużo pracy poświęcono opracowaniu procedur decyzyjnych dla teorii logicznych. Złożoność dowodów koncentruje się na wielkości dowodów i złożoności obliczeniowej generowania dowodów. Istnieje fascynująca linia prac związanych z programami do proofów, która łączy się z pracą od logiki liniowej w celu opracowania systemów proofów, aw konsekwencji języków programowania wrażliwych na zasoby.

Teoria rekurencji rekurencji Nasza rekurencji jest teorią złożoności. Zamiast badać, co jest obliczalne, badamy, jak wydajnie możemy obliczać. Istnieje wiele analogów teorii rekurencji w teorii złożoności, ale wyniki i oddzielenia teorii rekurencji nie zawsze są zgodne z ich teoretycznymi analogami złożoności. Zamiast zbiorów obliczeniowych i hierarchii arytmetycznej mamy czas wielomianowy, wielomianową hierarchię czasu i przestrzeń wielomianową obejmującą hierarchię. Zamiast ograniczonej kwantyfikacji w hierarchii arytmetycznej mamy zadowalające i skwantyfikowane formuły boolowskie oraz ograniczoną kwantyfikację formuł boolowskich.

Artykuł z ankiety

O niezwykłej skuteczności logiki w informatyce

jest dobrym punktem wyjścia do uzyskania bardzo wysokiego poziomu logiki obliczeniowej. Wymienię kilka logicznie ukierunkowanych dziedzin informatyki. Mam nadzieję, że inni edytują tę odpowiedź i dodają ją do tej listy tutaj i ewentualnie dodają link do odpowiedzi na tej stronie.

1. Teoria modeli skończonych
2. Dowód złożoności
3. Odliczenie algorytmiczne (procedury decyzyjne dla teorii logicznych)
4. Logika programów
5. Logika dynamiczna
6. Liniowa logika czasowa i jej warianty
7. Logika drzewa obliczeniowego i jej warianty
8. Logika epistemiczna
9. Teoria baz danych
10. Teoria typów
11. Automaty nad nieskończonymi słowami
12. Logika kategoryczna
13. Teoria współbieżności i algebra procesów
14. Teoria domen
15. Logika liniowa
16. Złożoność opisowa
17. Sprawdzanie modelu
18. Rachunki stałoprzecinkowe i logika zamykania przechodniego

obszarem silnego nakładania się logiki z informatyką jest automatyczne potwierdzanie twierdzeń , np. [4]. także np. ref [1] to użycie twierdzenia Boyera-Moore'a do sprawdzenia / weryfikacji twierdzenia Godelsa. innym ważnym ważnym / imponującym wynikiem jest niedawne zakończenie weryfikacji oprogramowania czterokolorowego twierdzenia (i innych, takich jak Odd Order i Feit-Thompson [3]) w badaniach Microsoftu przeprowadzonych przez Gonthiera. [2]

[1] Metamathematics, Machines and Gödel's Proof (Cambridge Tracts in Theoretical Computer Science, autor: Shankar

[2] Sprawdzony komputerowo dowód twierdzenia o czterech kolorach Georges Gonthier

[3] Interesujące algorytmy w formalizacji twierdzenia Feit-Thompson? tcs.se

[4] Gdzie i jak komputery pomogły udowodnić twierdzenie? tcs.se