Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Информацию об академической конференции LICS см. Симпозиум по логике в компьютерных науках .
Схематическое изображение логических вентилей компьютера

Логика в информатике перекрывает области логики и информатики . По сути, эту тему можно разделить на три основных направления:

  • Теоретические основы и анализ
  • Использование компьютерных технологий в помощь логикам
  • Использование концепций из логики для компьютерных приложений

Теоретические основы и анализ [ править ]

Логика играет фундаментальную роль в информатике. Некоторые из ключевых областей логики, которые имеют особое значение, - это теория вычислимости (ранее называемая теорией рекурсии), модальная логика и теория категорий . Теория вычислений основана на концепциях , определенных логиков и математиков , таких как Алонзо Церкви и Алан Тьюринг . [1] [2] Черч впервые показал существование алгоритмически неразрешимых проблем, используя свое понятие лямбда-определимости. Тьюринг дал первый убедительный анализ того, что можно назвать механической процедурой, а Курт Гёдель утверждал, что он нашел анализ Тьюринга «совершенным».[3] Кроме того, некоторые другие основные области теоретического пересечения логики и информатики:

  • Теорема Гёделя о неполноте доказывает, что любая логическая система, достаточно мощная, чтобы характеризовать арифметику, будет содержать утверждения, которые нельзя ни доказать, ни опровергнуть в рамках этой системы. Это имеет прямое приложение к теоретическим вопросам, касающимся возможности доказательства полноты и правильности программного обеспечения. [4]
  • Проблема фрейма - это основная проблема, которую необходимо преодолеть при использовании логики первого порядка для представления целей и состояния агента искусственного интеллекта. [5]
  • Соответствие Карри – Ховарда - это связь между логическими системами и программным обеспечением. Эта теория установила точное соответствие между доказательствами и программами. В частности, он показал, что термины в простом типизированном лямбда-исчислении соответствуют доказательствам интуиционистской логики высказываний.
  • Теория категорий представляет собой взгляд на математику, который подчеркивает отношения между структурами. Он тесно связан со многими аспектами информатики: системами типов для языков программирования, теорией систем переходов, моделями языков программирования и теорией семантики языков программирования. [6]

Компьютеры в помощь логикам [ править ]

Одним из первых приложений, в которых использовался термин искусственный интеллект, была система Logic Theorist, разработанная Алленом Ньюэллом , Дж. К. Шоу и Гербертом Саймоном в 1956 году. Одна из вещей, которые делает логик, - это взять набор логических утверждений и вывести выводы (дополнительные утверждения), которые должны соответствовать законам логики. Например, если дана логическая система, которая гласит: «Все люди смертны» и «Сократ - человек», правильным выводом будет «Сократ смертен». Конечно, это банальный пример. В реальных логических системах утверждения могут быть многочисленными и сложными. С самого начала стало понятно, что этому виду анализа может значительно помочь использование компьютеров. Теоретик логики подтвердил теоретические работыБертран Рассел и Альфред Норт Уайтхед в их влиятельной работе по математической логике под названием Principia Mathematica . Кроме того, логики использовали последующие системы для проверки и открытия новых логических теорем и доказательств. [7]

Логические приложения для компьютеров [ править ]

Математическая логика всегда оказывала сильное влияние на область искусственного интеллекта (ИИ). С самого начала работы в этой области было понятно, что технология автоматизации логических выводов может иметь большой потенциал для решения проблем и вывода выводов из фактов. Рон Брахман описал логику первого порядка (FOL) как метрику, с помощью которой все представления знаний AIформализмы должны быть оценены. Нет более общего или мощного известного метода описания и анализа информации, чем FOL. Причина, по которой FOL просто не используется в качестве компьютерного языка, состоит в том, что он на самом деле слишком выразителен в том смысле, что FOL может легко выражать утверждения, которые ни один компьютер, независимо от его мощности, никогда не сможет решить. По этой причине каждая форма представления знаний - это в некотором смысле компромисс между выразительностью и вычислимостью. Чем выразительнее язык, чем он ближе к FOL, тем больше вероятность того, что он будет медленнее и склонен к бесконечному циклу. [8]

Например, правила ЕСЛИ ТО, используемые в экспертных системах, приблизительно соответствуют очень ограниченному подмножеству ВОЛС. Вместо произвольных формул с полным набором логических операторов отправной точкой является просто то, что логики называют modus ponens . В результате системы на основе правил могут поддерживать высокопроизводительные вычисления, особенно если они используют преимущества алгоритмов оптимизации и компиляции. [9]

Другой важной областью исследований логической теории была программная инженерия. В исследовательских проектах, таких как программы Knowledge Based Software Assistant и Programmer's Apprentice, применялась логическая теория для проверки правильности спецификаций программного обеспечения. Они также использовали их для преобразования спецификаций в эффективный код на различных платформах и для доказательства эквивалентности реализации и спецификации. [10] Такой формальный подход, основанный на преобразовании, часто требует гораздо больше усилий, чем традиционная разработка программного обеспечения. Однако в определенных областях с соответствующими формализмами и шаблонами многократного использования этот подход оказался жизнеспособным для коммерческих продуктов. Подходящими доменами обычно являются такие, как системы вооружений, системы безопасности и финансовые системы в реальном времени, где отказ системы требует чрезмерно высоких человеческих или финансовых затрат. Примером такого домена является очень крупномасштабная интегрированная (СБИС).дизайн - процесс проектирования микросхем, используемых для процессоров и других критических компонентов цифровых устройств. Ошибка в микросхеме - это катастрофа. В отличие от программного обеспечения, чипы не подлежат исправлению или обновлению. В результате существует коммерческое обоснование использования формальных методов для доказательства того, что реализация соответствует спецификации. [11]

Еще одно важное применение логики в компьютерных технологиях - это языки фреймов и автоматические классификаторы. Рамочные языки, такие как KL-ONEимеют жесткую семантику. Определения в KL-ONE можно напрямую сопоставить с теорией множеств и исчислением предикатов. Это позволяет специализированным средствам доказательства теорем, называемым классификаторами, анализировать различные объявления между наборами, подмножествами и отношениями в данной модели. Таким образом, модель может быть проверена, и любые несогласованные определения будут отмечены. Классификатор также может выводить новую информацию, например определять новые наборы на основе существующей информации и изменять определение существующих наборов на основе новых данных. Уровень гибкости идеален для работы в постоянно меняющемся мире Интернета. Технология классификаторов построена на основе таких языков, как язык веб-онтологий, чтобы обеспечить логический семантический уровень существующего Интернета. Этот слой называется семантической сетью .[12] [13]

Временная логика используется для рассуждений в параллельных системах . [14]

См. Также [ править ]

  • Автоматизированное рассуждение
  • Вычислительная логика
  • Логическое программирование

Ссылки [ править ]

  1. ^ Льюис, Гарри Р. (1981). Элементы теории вычислений . Прентис Холл .
  2. ↑ Дэвис, Мартин (11 мая 1995 г.). «Влияние математической логики на информатику» . В Рольф Херкен (ред.). Универсальная машина Тьюринга . Springer Verlag. ISBN 9783211826379. Проверено 26 декабря 2013 года .
  3. ^ Кеннеди, Juliette (2014-08-21). Устный перевод Гёделя . Издательство Кембриджского университета. ISBN 9781107002661. Проверено 17 августа 2015 года .
  4. ^ Хофштадтер, Дуглас Р. (1999-02-05). Гедель, Эшер, Бах: вечная золотая коса . Основные книги. ISBN 978-0465026562.
  5. ^ Маккарти, Джон ; П. Дж. Хейс (1969). «Некоторые философские проблемы с точки зрения искусственного интеллекта» (PDF) . Машинный интеллект . 4 : 463–502.
  6. ^ Барр, Майкл; Чарльз Уэллс (1998). Теория категорий для компьютерных наук (PDF) . Centre de Recherches Mathématiques .
  7. ^ Ньюэлл, Аллен; Джей Си Шоу; ХК Саймон (1963). «Эмпирические исследования с помощью машины логической теории» . В Эде Фейгенбауме (ред.). Компьютеры и мысль . Макгроу Хилл. С.  109–133 . ISBN 978-0262560924.
  8. ^ Левеск, Гектор; Рональд Брахман (1985). «Фундаментальный компромисс в представлении знаний и рассуждении» . В Рональде Брахмане и Гекторе Дж. Левеке (ред.). Чтение в представлении знаний . Морган Кауфманн. п. 49 . ISBN 0-934613-01-X. Хорошая новость в сокращении обслуживания KR до доказательства теорем состоит в том, что теперь у нас есть очень четкое, очень конкретное представление о том, что должна делать система KR; Плохая новость заключается в том, что также ясно, что услуги не могут быть предоставлены ... решить, является ли предложение в FOL теоремой ... неразрешимо.
  9. ^ Forgy, Чарльз (1982). «Rete: быстрый алгоритм для решения проблемы соответствия множеству шаблонов / множеству объектов *» (PDF) . Искусственный интеллект . 19 : 17–37. DOI : 10.1016 / 0004-3702 (82) 90020-0 . Архивировано из оригинального (PDF) 27 декабря 2013 года . Проверено 25 декабря 2013 года .
  10. ^ Рич, Чарльз; Ричард С. Уотерс (ноябрь 1987 г.). «Проект ученика программиста: обзор исследования» (PDF) . Эксперт IEEE . Проверено 26 декабря 2013 года .
  11. ^ Ставриду, Виктория (1993). Формальные методы в схемотехнике . Синдикат прессы Кембриджского университета. ISBN 0-521-443369. Проверено 26 декабря 2013 года .
  12. ↑ МакГрегор, Роберт (июнь 1991 г.). «Использование классификатора описания для улучшения представления знаний». Эксперт IEEE . 6 (3): 41–46. DOI : 10.1109 / 64.87683 . S2CID 29575443 . 
  13. ^ Бернерс-Ли, Тим ; Джеймс Хендлер; Ора Лассила (17 мая 2001 г.). «Семантическая сеть Web. Новая форма веб-контента, значимая для компьютеров, откроет революцию новых возможностей» . Scientific American . 284 : 34–43. DOI : 10.1038 / Scientificamerican0501-34 . Архивировано из оригинального 24 апреля 2013 года .
  14. ^ Колин Стирлинг (1992). «Модальная и временная логика». У С. Абрамского; DM Gabbay; TSE Maibaum (ред.). Справочник по логике в компьютерных науках . II . Издательство Оксфордского университета. С. 477–563. ISBN 0-19-853761-1.

Дальнейшее чтение [ править ]

  • Бен-Ари, Мордехай (2012). Математическая логика для компьютерных наук (3-е изд.). Springer-Verlag. ISBN 978-1447141280.
  • Харрисон, Джон (2009). Справочник по практической логике и автоматизированному мышлению (1-е изд.). Издательство Кембриджского университета. ISBN 978-0521899574.
  • Хут, Майкл; Райан, Марк (2004). Логика в компьютерных науках: моделирование и рассуждения о системах (2-е изд.). Издательство Кембриджского университета. ISBN 978-0521543101.
  • Беррис, Стэнли Н. (1997). Логика для математики и информатики (1-е изд.). Прентис Холл. ISBN 978-0132859745.

Внешние ссылки [ править ]

  • Статья о логике и искусственном интеллекте в Стэнфордской энциклопедии философии .
  • Симпозиум IEEE по логике в компьютерных науках (LICS)
  • Алвен Тиу, Введение в логическую видеозапись лекции на Летней школе логики ANU '09 (ориентировано в основном на компьютерных ученых)