Powód, dla którego warto nauczyć się logiki zdań i predykatów

Rozumiem znaczenie, jakie informatycy lub inżynierowie związani z opracowywaniem oprogramowania powinni rozumieć jako podstawy badania logiki podstawowej.

Ale czy są jakieś zadania / zadania, które wyraźnie wymagają wiedzy na ich temat, inne niż zadania wymagające jakiejkolwiek reprezentacji wiedzy przy użyciu Knowledge Base? Chcę usłyszeć rodzaje zadań, a nie koncepcyjne odpowiedzi.

Powód, dla którego o to pytam, wynika z mojej ciekawości. Podczas gdy studenci CS muszą poświęcić pewną ilość czasu na ten temat, niektóre intensywne kursy praktyczne (np. Klasa AI ) całkowicie pominęły ten temat. Zastanawiam się tylko, czy na przykład wiedza predicate logicmoże pomóc w rysowaniu, ER diagramale może nie być wymogiem.

Aktualizacja 27.05.2012) Dziękujemy za odpowiedzi. Teraz myślę, że całkowicie rozumiem i zgadzam się ze znaczeniem logicCS w jego ogromnej ilości zastosowań. Właśnie wybrałem najlepszą odpowiedź naprawdę z imponującego wrażenia, jakie uzyskałem dzięki rozwiązaniu problemu Windows„niebieskiego ekranu”.

Lubię Unifikację i wszystko, co się z tym wiąże. Jeśli nie znasz logiki zdań i predykatów, pomijasz podstawy logiki. Jeśli interesuje Cię coś na liście , byłoby to jak matematyka i pomijanie dodawania i mnożenia. Logika dotyczy nie tylko sztucznej inteligencji.

Jako praktyczną odpowiedź pamiętasz problem zmiennoprzecinkowy Intela i jak go już nie widzisz? Dzięki zastosowaniu dowodu twierdzenia należą one do przeszłości. Pamiętaj niebieski ekran śmierci Microsoft . Dzięki rozwiązaniom SAT, sprawdzaniu modeli i innym rozwiązaniom opartym na logice są gatunkiem zagrożonym.

Istnieją niezwykle głębokie i wszechobecne powiązania między logiką a informatyką. Rozumiejąc, czym mogą być, pamiętaj, że informatyka jest również nazywana „technologią informatyczną” lub „informatyką”, co oznacza, że ​​systemy komputerowe przechwytują, przetwarzają i dostarczają informacje. Cóż, logika jest podobna. Bada, w jaki sposób informacje są przechwytywane w zdaniach i jak możliwe jest, aby jedno oświadczenie było konsekwencją drugiego, tj. W jaki sposób jego treść informacyjna jest już obecna w innym oświadczeniu (lub zbiorze oświadczeń). W tym sensie logika i informatyka są zasadniczo takie samedyscyplina, koncentrująca się na różnych aspektach. Logicyści (Church, Kleene, Turing, Post oraz ich studenci i koledzy) stworzyli dyscyplinę informatyki, a wielu logików nadal przyczynia się do informatyki, w szczególności Jean-Yves Girard i jego uczniowie.

Oto niektóre standardowe zastosowania logiki w informatyce:

• Projektowanie obwodów cyfrowych jest całkowicie oparte na logice propozycji, do tego stopnia, że ​​inżynierowie nazywają to „projektem logiki”, a nie „projektem obwodu”. Często nawet uważa się, że pisanie programu komputerowego wymaga opracowania jego „logiki”. (Należy zauważyć, że „logika” w tym drugim sensie jest nieformalnym pomysłem, a nie logiką formalną, stosowaną w odniesieniu do przepływu informacji przez program i tego, czy jest przetwarzana poprawnie).

• Logika predykatów i jej kuzyn matematyczny, teoria mnogości, są używane w różnych językach obliczeniowych , np. W języku SQL do kwerend relacyjnych baz danych. Istnieją również języki programowania oparte na logice, zwane „logicznymi językami programowania”.

• Reprezentacja wiedzy , o której już wspomniałeś, ma wiele formalizmów opartych na logice. Nawet jeśli używa nielogicznych formalizmów, wiele z nich nadal ma logiczne znaczenie , a zatem są oparte na logice.

• Logika probabilistyczna, w której stwierdzenia mają nie tylko prawdziwe / fałszywe wartości, ale poziomy pewności / niepewności, jest coraz częściej podstawą systemów uczenia maszynowego .

• Jeśli chcesz formalnie stwierdzić, co robi program, tj. Podać specyfikację programu , skończysz na jakimś logicznym języku. Rzeczywiście istnieje wiele języków specyfikacji programów, takich jak Z i B, które są oparte na logice predykatów i teorii mnogości. Istnieją również języki specyfikacji oparte na logice równikowej, takie jak Larch. Informatycy często wynajdują nowe logiki, które odzwierciedlają potrzeby informatyki, np. Logikę Hoare'a i Logikę separacyjną, lub też wychwytują i rozwijają różne niewykorzystane formy tradycyjnych logik, takich jak logika czasowa i logiczna, i rozwijają je dalej.

• Jeśli chcesz sprawdzić, czy program robi to, co powinien, to w końcu używasz nie tylko języka logiki, ale całej maszynerii logiki: teorii dowodu, teorii modelu i procedur decyzyjnych. Technologia weryfikacji rozwija się teraz skokowo i spodziewam się, że za około dekadę będą one rutynowo wykorzystywane do prawie całego tworzenia oprogramowania.

W rzeczywistości powiązania między logiką a informatyką są tak głębokie i wszechobecne, że powiedziałbym, że trudno jest być dobrym informatykiem bez dogłębnego zrozumienia logiki.

Powodem, dla którego niektórzy naukowcy zajmujący się sztuczną inteligencją jest niedocenianie logiki w tym czasie, jest fakt, że niektórzy z pierwszych twórców AI zaproponowali gotową logikę jako narzędziezamiast podstawy. AI ze swej natury obiecuje dostarczać magię. Nie musimy wykonywać trudnych zadań związanych z programowaniem systemów, aby dostarczać wyniki. Byliby w stanie sami wymyślić, jak tworzyć rozwiązania, ponieważ byliby „inteligentni”. Logika wydawała się wskazywać drogę, ponieważ gdyby systemy komputerowe rozumiały logikę i wiedziały, jak przetwarzać informacje za pomocą reguł logiki, byłyby w stanie dostarczyć magię. Tego rodzaju wiara w logikę była z perspektywy czasu niewłaściwa. Po pierwsze, gotowa logika jest jednocześnie zbyt silna i zbyt słaba. Jest zbyt silny w tym sensie, że reguły logiki są zbyt ogólne, aby opracować skuteczne procedury. Jest również zbyt słaby, ponieważ jest to logika opracowana przez matematyków na potrzeby matematyki i nie • mają słownictwo potrzebne do radzenia sobie z wieloma innymi rzeczywistymi informacjami, z którymi muszą sobie radzić systemy AI (takie jak niepewność, informacje kontekstowe, takie jak czas, zmiana, wiedza, sprawność itp.). Tak więc AI przechodzi obecnie reakcję logiczną. Ale myślę, że kiedy pokonają ten luz, naukowcy AI zdadzą sobie sprawę, że wszystkie nowsze metody są nadal opartelogika szeroko rozumiana .

Logika ma fundamentalne znaczenie dla całej teoretycznej informatyki. Bez ich opanowania nie będziesz w stanie właściwie zrozumieć semantyki języka programowania, maszyn Turinga, programowania logiki, obliczalności i tak dalej. Bez tego nawet rozumowanie programów będzie trudniejsze. Z pewnością próba matematycznego potwierdzenia jakiegoś pojęcia CS jest praktycznie niemożliwa.

A może pytasz o zastosowania w przemyśle. Logika uczenia się stanowi podstawę do nauki jasnego rozumowania i dostrzegania dziur w argumentach innych ludzi. Logika ma fundamentalne znaczenie, niezależnie od tego, czy używasz symboli formalnych, czy nie.

Jednym z powtarzających się zadań, przed którymi stają praktykujący i teoretycy CS, jest uzyskanie pewności co do poprawności ich kodu.

Istnieją dwa główne podejścia:

1. Dowód: Opracuj logiczny dowód, że część systemu ma pewne właściwości, być może wspomagane przez warunki wstępne, projekt po umowie, sprawdzanie kodu.
2. Testowanie: sprawdź, czy niektóre właściwości zachowują dla różnych danych wejściowych, a następnie indukuj, że ta właściwość obowiązuje dla innych danych wejściowych.

Pierwsza, oparta na metodach logicznych, jest często jedyną opcją, kiedy

1. Nie ma typowego wejścia. Na przykład podczas testowania właściwości zabezpieczeń należy się martwić o nietypowe dane wejściowe, więc o ile nie można logicznie uzasadnić, które dane wejściowe są nietypowe, uzyskanie dobrego zasięgu jest mało prawdopodobne.
2. Przestrzeń konfiguracji jest bardzo duża, więc musisz ją rozłożyć na części, logicznie zastanawiając się, które części mogą wpływać na które inne części przed testowaniem lokalnym.
3. Masz tylko dokumentację opisującą zachowanie na krawędzi systemów poza Twoją kontrolą. Być może możesz je zasymulować, ale nie możesz przetestować, co dzieje się, gdy zależność zewnętrzna zawiedzie, ponieważ nie jesteś w stanie spowodować jej awarii z powodów prawnych lub etycznych.

Testy empiryczne przy braku dowodu w zasadzie zastępują dowód. Projektując system, który ma być testowalny, tworzysz szkic próbny, w którym wypełniasz części dowodu „testem X, Y i Z”. Umiejętność logicznego rozumowania jest niezbędna, aby móc zaprojektować testowalny system. Jeśli system nie jest testowalny ani nie da się go udowodnić, to jego projektant / architekt nie musi twierdzić, że jest odpowiedni do zamierzonego zastosowania.

Dwa najważniejsze pola, w których logika odgrywa istotną rolę, to:

1. Specyfikacja i weryfikacja języka formalnego .
2. Naprawiono parametry klasy możliwej do przełknięcia .

$Z$

W skrócie: 1. Definicja języka wymaga logiki, 2: Sprawiedliwość jego procedur wymaga logiki, 3. procedury weryfikacji wymagają logiki.

Powinienem wspomnieć, że różni się to od projektu kompilatora lub ... Jest to „Formalna” definicja języków, głównym powodem tego jest udowodnienie poprawności języka lub modelu, również posiadanie formalnego dowodu. Można to wykorzystać do weryfikacji modeli oprogramowania, znalezienia błędów przed wdrożeniem, ponownego znalezienia impasu przed wdrożeniem ... W przypadku oprogramowania, które to symuluje, możesz zapoznać się z NModel .

Teraz, dlaczego w problemach z ustalonymi parametrami możliwymi do pracy musisz pracować z logiką, możesz podzielić klasy zdolności do ustalania parametrów z różnymi poziomami logiki, można je konwertować między sobą: logika do automatów, automaty do wykresu i vice versa, ale jeśli jesteś ekspertem w logice, możesz dzielić i decydować o nich po prostu, najważniejsze twierdzenie (po twierdzeniu Robertsona i Seymoura ), w tej dziedzinie jest twierdzenie Courcelle'a . Aby uzyskać więcej informacji, przeczytaj ankietę Meta Algorytmic Theorem .