Логика в информатике
Логика в информатике охватывает область пересечения областей логики и информатики . По сути, эту тему можно разделить на три основных направления:
- Теоретические основы и анализ
- Использование компьютерных технологий в помощь логикам
- Использование концепций из логики для компьютерных приложений.
основы анализ Теоретические и
Логика играет фундаментальную роль в информатике. Некоторые из ключевых областей логики, которые имеют особенно важное значение, — это теория вычислимости (ранее называвшаяся теорией рекурсии), модальная логика и теория категорий . Теория вычислений основана на концепциях, определенных логиками и математиками, такими как Алонзо Чёрч и Алан Тьюринг . [1] [2] Черч первым показал существование алгоритмически неразрешимых проблем, используя свое понятие лямбда-определимости. Тьюринг дал первый убедительный анализ того, что можно назвать механической процедурой, а Курт Гёдель утверждал, что он нашел анализ Тьюринга «идеальным». [3] Кроме того, некоторые другие основные области теоретического совпадения логики и информатики:
- Теорема Гёделя о неполноте доказывает, что любая логическая система, достаточно мощная, чтобы охарактеризовать арифметику, будет содержать утверждения, которые нельзя ни доказать, ни опровергнуть в рамках этой системы. Это имеет прямое применение к теоретическим вопросам, связанным с возможностью доказательства полноты и правильности программного обеспечения. [4]
- — Проблема фрейма это базовая проблема, которую необходимо преодолеть при использовании логики первого порядка для представления целей агента искусственного интеллекта и состояния его среды. [5]
- Соответствие Карри -Ховарда — это связь между логическими системами и языками программирования. Эта теория установила точное соответствие между доказательствами и программами. В частности, он показал, что термины в просто типизированном лямбда-исчислении соответствуют доказательствам интуиционистской логики высказываний .
- Теория категорий представляет собой взгляд на математику, который подчеркивает отношения между структурами. Она тесно связана со многими аспектами информатики: системами типов языков программирования, теорией переходных систем , моделями языков программирования и теорией семантики языков программирования . [6]
- Логическое программирование — это парадигма программирования , баз данных и представления знаний , основанная на формальной логике . Логическая программа — это набор предложений о некоторой проблемной области. Вычисления выполняются путем применения логических рассуждений для решения проблем в предметной области. Основные семейства языков логического программирования включают Prolog , Answer Set Programming (ASP) и Datalog .
Компьютеры логикам помощь в
Одним из первых применений термина « искусственный интеллект» была система «Теоретик логики» , разработанная Алленом Ньюэллом , Клиффом Шоу и Гербертом Саймоном в 1956 году. Одна из задач логика — это взять набор логических утверждений и вывести выводы (дополнительные утверждения), которые должны быть истинны по законам логики. Например, если даны утверждения «Все люди смертны» и «Сократ — человек», действительным выводом будет «Сократ смертен». Конечно, это тривиальный пример. В реальных логических системах утверждения могут быть многочисленными и сложными. Вскоре стало понятно, что такого рода анализу может существенно помочь использование компьютеров. Теоретик логики подтвердил теоретические работы Бертрана Рассела и Альфреда Норта Уайтхеда в их влиятельной работе по математической логике под названием Principia Mathematica . Кроме того, последующие системы использовались логиками для проверки и открытия новых математических теорем и доказательств. [7]
Логические приложения для компьютеров [ править ]
Математическая логика всегда имела сильное влияние на область искусственного интеллекта (ИИ). С самого начала было понятно, что технология автоматизации логических выводов может иметь большой потенциал для решения проблем и получения выводов на основе фактов. Рон Брахман описал логику первого порядка (FOL) как метрику, с помощью которой представления знаний следует оценивать все формализмы ИИ. Логика первого порядка — это общий и мощный метод описания и анализа информации. Причина, по которой сам FOL просто не используется в качестве компьютерного языка, заключается в том, что он на самом деле слишком выразителен в том смысле, что FOL может легко выражать утверждения, которые ни один компьютер, каким бы мощным он ни был, никогда не сможет решить. По этой причине каждая форма представления знаний является в некотором смысле компромиссом между выразительностью и вычислимостью . Чем выразительнее язык, чем ближе он к FOL, тем больше вероятность того, что он будет медленнее и склонен к бесконечному циклу. [8]
Например, правила ЕСЛИ-ТО, используемые в экспертных системах, соответствуют очень ограниченному подмножеству FOL. Вместо произвольных формул с полным набором логических операторов отправной точкой является просто то, что логики называют modus ponens . В результате системы, основанные на правилах , могут поддерживать высокопроизводительные вычисления, особенно если они используют преимущества алгоритмов оптимизации и компиляции. [9]
С другой стороны, логическое программирование , сочетающее в себе подмножество предложений Хорна логики первого порядка с немонотонной формой отрицания , обладает как высокой выразительной силой, так и эффективными реализациями . В частности, язык логического программирования Пролог является полным по Тьюрингу языком программирования. Datalog расширяет модель реляционной базы данных рекурсивными отношениями, а программирование набора ответов — это форма логического программирования, ориентированная на сложные (в первую очередь NP-трудные ) задачи поиска .
Другой важной областью исследований логической теории является разработка программного обеспечения . В исследовательских проектах, таких как программы Knowledge Based Software Assistant и Programmer's Apprentice, логическая теория применялась для проверки правильности спецификаций программного обеспечения . Они также использовали логические инструменты для преобразования спецификаций в эффективный код на различных платформах и для доказательства эквивалентности реализации и спецификации. [10] Этот формальный подход, основанный на трансформации, часто требует гораздо больше усилий, чем традиционная разработка программного обеспечения. Однако в конкретных областях с соответствующими формализмами и шаблонами многократного использования этот подход оказался жизнеспособным для коммерческих продуктов. Соответствующими областями обычно являются такие, как системы вооружений, системы безопасности и финансовые системы реального времени, где отказ системы влечет за собой чрезмерно высокие человеческие или финансовые затраты. Примером такой области является проектирование сверхкрупной интеграции (СБИС) — процесс проектирования микросхем, используемых для процессоров и других критически важных компонентов цифровых устройств. Ошибка в чипе может иметь катастрофические последствия. В отличие от программного обеспечения, чипы нельзя исправлять или обновлять. В результате появляется коммерческое обоснование использования формальных методов для доказательства соответствия реализации спецификации. [11]
Другое важное применение логики в компьютерных технологиях связано с языками фреймов и автоматическими классификаторами. Языки фреймов , такие как KL-ONE, могут быть напрямую сопоставлены с теорией множеств и логикой первого порядка. Это позволяет специализированным средствам доказательства теорем , называемым классификаторами, анализировать различные объявления между множествами , подмножествами и отношениями в данной модели. Таким образом, модель может быть проверена и отмечены любые противоречивые определения. Классификатор также может выводить новую информацию, например определять новые наборы на основе существующей информации и изменять определения существующих наборов на основе новых данных. Уровень гибкости идеален для работы в постоянно меняющемся мире Интернета. Технология классификаторов построена на основе таких языков, как язык веб-онтологии , чтобы обеспечить логический семантический уровень поверх существующего Интернета. Этот уровень называется семантической паутиной . [12] [13]
Темпоральная логика используется для рассуждений в параллельных системах . [14]
См. также [ править ]
Ссылки [ править ]
- ^ Льюис, Гарри Р. (1981). Элементы теории вычислений . Прентис Холл .
- ^ Дэвис, Мартин (11 мая 1995 г.). «Влияние математической логики на информатику» . В Рольфе Херкене (ред.). Универсальная машина Тьюринга . Спрингер Верлаг. ISBN 9783211826379 . Проверено 26 декабря 2013 г.
- ^ Кеннеди, Джульетта (21 августа 2014 г.). Интерпретация Гёделя . Издательство Кембриджского университета. ISBN 9781107002661 . Проверено 17 августа 2015 г.
- ^ Хофштадтер, Дуглас Р. (5 февраля 1999 г.). Гёдель, Эшер, Бах: Вечная золотая коса . Основные книги. ISBN 978-0465026562 .
- ^ Маккарти, Джон ; Пи Джей Хейс (1969). «Некоторые философские проблемы с точки зрения искусственного интеллекта» (PDF) . Машинный интеллект . 4 : 463–502.
- ^ Барр, Майкл; Чарльз Уэллс (1998). Теория категорий для информатики (PDF) . Центр математических исследований .
- ^ Ньюэлл, Аллен; Джей Си Шоу; ХК Саймон (1963). «Эмпирические исследования с помощью машины логической теории» . В Эде Фейгенбауме (ред.). Компьютеры и мысль . МакГроу Хилл. стр. 109–133 . ISBN 978-0262560924 .
- ^ Левеск, Гектор; Рональд Брахман (1985). «Фундаментальный компромисс в представлении и рассуждении знаний» . В Рональде Брахмане и Гекторе Дж. Левеске (ред.). Чтение в представлении знаний . Морган Кауфманн. п. 49 . ISBN 0-934613-01-Х .
Хорошей новостью при сведении службы КР к доказательству теорем является то, что теперь у нас есть очень четкое и очень конкретное представление о том, что должна делать система КР; Плохая новость заключается в том, что также очевидно, что услуги не могут быть предоставлены... решить, является ли предложение в FOL теоремой... неразрешимо.
- ^ Форги, Чарльз (1982). «Rete: быстрый алгоритм решения задачи сопоставления шаблонов «многие шаблоны» и «многие объекты» *» (PDF) . Искусственный интеллект . 19 :17–37. дои : 10.1016/0004-3702(82)90020-0 . Архивировано из оригинала (PDF) 27 декабря 2013 г. Проверено 25 декабря 2013 г.
- ^ Рич, Чарльз; Ричард К. Уотерс (ноябрь 1987 г.). «Проект ученика программиста: обзор исследования» (PDF) . Эксперт IEEE . Архивировано из оригинала (PDF) 6 июля 2017 г. Проверено 26 декабря 2013 г.
- ^ Ставриду, Виктория (1993). Формальные методы в схемотехнике . Пресс-синдикат Кембриджского университета. ISBN 0-521-443369 . Проверено 26 декабря 2013 г.
- ^ МакГрегор, Роберт (июнь 1991 г.). «Использование классификатора описания для улучшения представления знаний». Эксперт IEEE . 6 (3): 41–46. дои : 10.1109/64.87683 . S2CID 29575443 .
- ^ Бернерс-Ли, Тим ; Джеймс Хендлер; Ора Лассила (17 мая 2001 г.). «Семантическая сеть. Новая форма веб-контента, имеющая смысл для компьютеров, откроет революцию новых возможностей» . Научный американец . 284 : 34–43. doi : 10.1038/scientificamerican0501-34 . Архивировано из оригинала 24 апреля 2013 года.
- ^ Колин Стирлинг (1992). «Модальная и временная логика». У С. Абрамского ; ДМ Габбай ; TSE Майбаум (ред.). Справочник по логике в информатике . Том. II. Издательство Оксфордского университета. стр. 477–563. ISBN 0-19-853761-1 .
Дальнейшее чтение [ править ]
- Бен-Ари, Мордехай (2012). Математическая логика для информатики (3-е изд.). Спрингер-Верлаг. ISBN 978-1447141280 .
- Харрисон, Джон (2009). Справочник по практической логике и автоматическому рассуждению (1-е изд.). Издательство Кембриджского университета. ISBN 978-0521899574 .
- Хут, Майкл; Райан, Марк (2004). Логика в информатике: моделирование и рассуждения о системах (2-е изд.). Издательство Кембриджского университета. ISBN 978-0521543101 .
- Беррис, Стэнли Н. (1997). Логика для математики и информатики (1-е изд.). Прентис Холл. ISBN 978-0132859745 .
Внешние ссылки [ править ]
- Статья о логике и искусственном интеллекте в Стэнфордской энциклопедии философии .
- Симпозиум IEEE по логике в информатике (LICS)
- Алвен Тиу, «Введение в логику», видеозапись лекции в Летней школе логики ANU '09 (предназначена в основном для ученых-компьютерщиков)
