Logika w informatyce
Logika w informatyce obejmuje nakładanie się dziedziny logiki i informatyki . Temat można zasadniczo podzielić na trzy główne obszary:
- Podstawy teoretyczne i analiza
- Wykorzystanie technologii komputerowej do pomocy logikom
- Wykorzystanie pojęć z logiki do zastosowań komputerowych
Podstawy teoretyczne i analiza
Logika odgrywa fundamentalną rolę w informatyce. Niektóre z kluczowych obszarów logiki, które są szczególnie znaczące, to teoria obliczalności (wcześniej nazywana teorią rekurencji), logika modalna i teoria kategorii . Teoria obliczeń opiera się na koncepcjach zdefiniowanych przez logików i matematyków, takich jak Alonzo Church i Alan Turing . Church po raz pierwszy wykazał istnienie problemów nierozwiązywalnych algorytmicznie, używając swojego pojęcia definiowalności lambda. Turing przedstawił pierwszą przekonującą analizę tego, co można nazwać procedurą mechaniczną i Kurt Gödel zapewnił, że uznał analizę Turinga za „doskonałą”. Ponadto niektóre inne główne obszary teoretycznego pokrywania się logiki i informatyki to:
- Twierdzenie Gödla o niezupełności dowodzi, że każdy system logiczny wystarczająco potężny, aby scharakteryzować arytmetykę, będzie zawierał stwierdzenia, których nie można ani udowodnić, ani obalić w ramach tego systemu. Ma to bezpośrednie zastosowanie do zagadnień teoretycznych dotyczących możliwości udowodnienia kompletności i poprawności oprogramowania.
- Problem z ramą jest podstawowym problemem, który należy rozwiązać, używając logiki pierwszego rzędu do reprezentowania celów i stanu agenta sztucznej inteligencji.
- Curry'ego – Howarda to relacja między systemami logicznymi a oprogramowaniem. Teoria ta ustaliła dokładną zgodność między dowodami a programami. W szczególności wykazało, że terminy w prostym rachunku lambda odpowiadają dowodom intuicjonistycznej logiki zdań.
- Teoria kategorii reprezentuje pogląd na matematykę, który kładzie nacisk na relacje między strukturami. Jest ściśle powiązany z wieloma aspektami informatyki: systemami typów dla języków programowania, teorią systemów przejściowych, modelami języków programowania i teorią semantyki języków programowania.
Komputery wspomagające logików
Jedną z pierwszych aplikacji, w których użyto terminu sztuczna inteligencja , był system teorii logiki opracowany przez Allena Newella , JC Shawa i Herberta Simona w 1956 roku. wnioski (twierdzenia dodatkowe), które zgodnie z prawami logiki muszą być prawdziwe. Na przykład, jeśli biorąc pod uwagę system logiczny, który stwierdza, że „Wszyscy ludzie są śmiertelni” i „Sokrates jest człowiekiem”, prawidłowym wnioskiem jest „Sokrates jest śmiertelny”. Oczywiście to trywialny przykład. W rzeczywistych systemach logicznych instrukcje mogą być liczne i złożone. Wcześnie zdano sobie sprawę, że tego rodzaju analizy mogą być znacznie wspomagane przez wykorzystanie komputerów. Teoretyk logiki potwierdził pracę teoretyczną Bertrand Russell i Alfred North Whitehead w swojej wpływowej pracy na temat logiki matematycznej, zatytułowanej Principia Mathematica . Ponadto kolejne systemy były wykorzystywane przez logików do sprawdzania poprawności i odkrywania nowych twierdzeń i dowodów logicznych.
Aplikacje logiczne dla komputerów
Logika matematyczna zawsze wywierała silny wpływ na dziedzinę sztucznej inteligencji (AI). Od początku istnienia tej dziedziny zdano sobie sprawę, że technologia automatyzacji wnioskowania logicznego może mieć ogromny potencjał rozwiązywania problemów i wyciągania wniosków z faktów. Ron Brachman opisał logikę pierwszego rzędu (FOL) jako metrykę, według której cała reprezentacja wiedzy AI należy ocenić formalizmy. Nie ma bardziej ogólnej ani potężniejszej znanej metody opisywania i analizowania informacji niż FOL. Powodem, dla którego sam FOL po prostu nie jest używany jako język komputerowy, jest to, że jest on w rzeczywistości zbyt ekspresyjny w tym sensie, że FOL może z łatwością wyrażać stwierdzenia, których żaden komputer, bez względu na to, jak potężny, nigdy nie byłby w stanie rozwiązać. Z tego powodu każda forma reprezentacji wiedzy jest w pewnym sensie kompromisem między ekspresyjnością a obliczalnością. Im bardziej ekspresyjny jest język, im bliżej FOL, tym bardziej prawdopodobne jest, że będzie wolniejszy i podatny na nieskończoną pętlę.
Na przykład zasady JEŚLI TO TO stosowane w systemach eksperckich są zbliżone do bardzo ograniczonego podzbioru FOL. Zamiast arbitralnych formuł z pełnym zakresem operatorów logicznych punktem wyjścia jest po prostu to, co logicy nazywają modus ponens . W rezultacie systemy oparte na regułach mogą obsługiwać obliczenia o wysokiej wydajności, zwłaszcza jeśli korzystają z algorytmów optymalizacji i kompilacji.
Innym ważnym obszarem badań teorii logicznej była inżynieria oprogramowania. Projekty badawcze, takie jak Knowledge Based Software Assistant i Programmer's Apprentice, stosowały teorię logiczną do sprawdzania poprawności specyfikacji oprogramowania. Wykorzystali je również do przekształcenia specyfikacji w wydajny kod na różnych platformach oraz do udowodnienia równoważności między implementacją a specyfikacją. To formalne podejście oparte na transformacji jest często znacznie bardziej pracochłonne niż tradycyjne tworzenie oprogramowania. Jednak w określonych domenach z odpowiednimi formalizmami i szablonami wielokrotnego użytku podejście to sprawdziło się w przypadku produktów komercyjnych. Odpowiednimi domenami są zwykle takie dziedziny, jak systemy uzbrojenia, systemy bezpieczeństwa i systemy finansowe czasu rzeczywistego, w przypadku których awaria systemu pociąga za sobą zbyt wysokie koszty ludzkie lub finansowe. Przykładem takiej domeny jest Very Large Scale Integrated design (VLSI) — proces projektowania układów scalonych używanych w procesorach i innych krytycznych komponentach urządzeń cyfrowych. Błąd w chipie jest katastrofalny. W przeciwieństwie do oprogramowania, układów nie można łatać ani aktualizować. W rezultacie istnieje komercyjne uzasadnienie stosowania metod formalnych w celu udowodnienia zgodności implementacji ze specyfikacją.
Inne ważne zastosowanie logiki w technologii komputerowej dotyczy języków ramek i automatycznych klasyfikatorów. Języki ramowe , takie jak KL-ONE, mają sztywną semantykę. Definicje w KL-ONE można bezpośrednio odwzorować na teorię mnogości i rachunek predykatów. Pozwala to wyspecjalizowanym dowodnikom twierdzeń, zwanym klasyfikatorami, analizować różne deklaracje między zbiorami, podzbiorami i relacjami w danym modelu. W ten sposób model może zostać zweryfikowany, a wszelkie niespójne definicje oznaczone. Klasyfikator może również wywnioskować nowe informacje, na przykład zdefiniować nowe zestawy na podstawie istniejących informacji i zmienić definicję istniejących zestawów na podstawie nowych danych. Poziom elastyczności jest idealny do obsługi ciągle zmieniającego się świata Internetu. Technologia klasyfikatorów opiera się na językach takich jak Web Ontology Language , aby umożliwić logiczny poziom semantyczny w istniejącym Internecie. Ta warstwa nazywana jest Siecią Semantyczną .
Logika temporalna jest używana do wnioskowania w systemach współbieżnych .
Zobacz też
Dalsza lektura
- Ben-Ari, Mordechaj (2012). Logika matematyczna dla informatyki (wyd. 3). Springer-Verlag. ISBN 978-1447141280 .
- Harrison, John (2009). Podręcznik praktycznej logiki i zautomatyzowanego wnioskowania (wyd. 1). Wydawnictwo Uniwersytetu Cambridge. ISBN 978-0521899574 .
- Huth, Michael; Ryan, Mark (2004). Logika w informatyce: modelowanie i wnioskowanie o systemach (wyd. 2). Wydawnictwo Uniwersytetu Cambridge. ISBN 978-0521543101 .
- Burris, Stanley N. (1997). Logika dla matematyki i informatyki (wyd. 1). Sala Prentice'a. ISBN 978-0132859745 .
Linki zewnętrzne
- Artykuł o logice i sztucznej inteligencji w Stanford Encyclopedia of Philosophy .
- Sympozjum IEEE na temat logiki w informatyce (LICS)
- Alwen Tiu, Wprowadzenie do logiki nagranie wideo wykładu na ANU Logic Summer School '09 (skierowane głównie do informatyków)
| Pola |
|
||||
|---|---|---|---|---|---|
| Podwaliny | |||||
| Listy |
|
||||
