Логика в информатике - Logic in computer science
Логика в информатике перекрывает области логики и информатики . По сути, эту тему можно разделить на три основных направления:
- Теоретические основы и анализ
- Использование компьютерных технологий в помощь логикам
- Использование концепций из логики для компьютерных приложений
Теоретические основы и анализ
Логика играет фундаментальную роль в информатике. Некоторые из ключевых областей логики, которые имеют особое значение, - это теория вычислимости (ранее называемая теорией рекурсии), модальная логика и теория категорий . Теория вычислений основана на концепциях , определенных логиков и математиков , таких как Алонзо Церкви и Алан Тьюринг . Черч впервые показал существование алгоритмически неразрешимых проблем, используя свое понятие лямбда-определимости. Тьюринг дал первый убедительный анализ того, что можно назвать механической процедурой, а Курт Гёдель утверждал, что он нашел анализ Тьюринга «совершенным». Кроме того, некоторые другие основные области теоретического пересечения логики и информатики:
- Теорема Гёделя о неполноте доказывает, что любая логическая система, достаточно мощная, чтобы характеризовать арифметику, будет содержать утверждения, которые нельзя ни доказать, ни опровергнуть в рамках этой системы. Это имеет прямое приложение к теоретическим вопросам, касающимся возможности доказательства полноты и правильности программного обеспечения.
- Проблема фрейма - это основная проблема, которую необходимо преодолеть при использовании логики первого порядка для представления целей и состояния агента искусственного интеллекта.
- Соответствие Карри – Ховарда - это связь между логическими системами и программным обеспечением. Эта теория установила точное соответствие между доказательствами и программами. В частности, он показал, что термины в простом типизированном лямбда-исчислении соответствуют доказательствам интуиционистской логики высказываний.
- Теория категорий представляет собой взгляд на математику, который подчеркивает отношения между структурами. Он тесно связан со многими аспектами информатики: системами типов для языков программирования, теорией систем переходов, моделями языков программирования и теорией семантики языков программирования.
Компьютеры в помощь логикам
Одним из первых приложений, в которых использовался термин « искусственный интеллект», была система Logic Theorist, разработанная Алленом Ньюэллом , Дж. К. Шоу и Гербертом Саймоном в 1956 году. Одна из вещей, которую делает логик, - это взять набор логических утверждений и вывести их выводы (дополнительные утверждения), которые должны соответствовать законам логики. Например, если дана логическая система, которая гласит: «Все люди смертны» и «Сократ - человек», правильным выводом будет «Сократ смертен». Конечно, это банальный пример. В реальных логических системах утверждения могут быть многочисленными и сложными. С самого начала стало понятно, что этому виду анализа может значительно помочь использование компьютеров. Теоретик логики подтвердил теоретические работы Бертрана Рассела и Альфреда Норта Уайтхеда в их влиятельной работе по математической логике под названием Principia Mathematica . Кроме того, логики использовали последующие системы для проверки и открытия новых логических теорем и доказательств.
Логические приложения для компьютеров
Математическая логика всегда оказывала сильное влияние на область искусственного интеллекта (ИИ). С самого начала работы в этой области было понятно, что технология автоматизации логических выводов может иметь большой потенциал для решения проблем и вывода выводов из фактов. Рон Брахман описал логику первого порядка (FOL) как метрику, с помощью которой должны оцениваться все формализмы представления знаний ИИ . Нет более общего или мощного известного метода описания и анализа информации, чем FOL. Причина, по которой FOL просто не используется в качестве компьютерного языка, заключается в том, что он на самом деле слишком выразителен в том смысле, что FOL может легко выражать утверждения, которые ни один компьютер, независимо от его мощности, никогда не сможет решить. По этой причине каждая форма представления знаний в некотором смысле является компромиссом между выразительностью и вычислимостью. Чем выразительнее язык, чем он ближе к FOL, тем больше вероятность того, что он будет медленнее и склонен к бесконечному циклу.
Например, правила ЕСЛИ ТО, используемые в экспертных системах, соответствуют очень ограниченному подмножеству ВОЛС. Вместо произвольных формул с полным набором логических операторов отправной точкой является просто то, что логики называют modus ponens . В результате системы на основе правил могут поддерживать высокопроизводительные вычисления, особенно если они используют преимущества алгоритмов оптимизации и компиляции.
Другой важной областью исследований логической теории была программная инженерия. В исследовательских проектах, таких как программы Knowledge Based Software Assistant и Programmer's Apprentice, применялась логическая теория для проверки правильности спецификаций программного обеспечения. Они также использовали их для преобразования спецификаций в эффективный код на различных платформах и для доказательства эквивалентности реализации и спецификации. Этот формальный подход, основанный на преобразовании, часто требует гораздо больше усилий, чем традиционная разработка программного обеспечения. Однако в определенных областях с соответствующими формализмами и шаблонами многократного использования этот подход оказался жизнеспособным для коммерческих продуктов. Подходящими областями обычно являются такие, как системы вооружений, системы безопасности и финансовые системы в реальном времени, где отказ системы имеет чрезмерно высокие человеческие или финансовые затраты. Примером такой области является проектирование очень крупномасштабной интегрированной (СБИС) - процесс проектирования микросхем, используемых для ЦП и других критических компонентов цифровых устройств. Ошибка в микросхеме - это катастрофа. В отличие от программного обеспечения, чипы не могут быть исправлены или обновлены. В результате существует коммерческое обоснование использования формальных методов для доказательства того, что реализация соответствует спецификации.
Еще одно важное применение логики в компьютерных технологиях было в области языков фреймов и автоматических классификаторов. Фреймовые языки, такие как KL-ONE, имеют жесткую семантику. Определения в KL-ONE можно напрямую сопоставить с теорией множеств и исчислением предикатов. Это позволяет специализированным средствам доказательства теорем, называемым классификаторами, анализировать различные объявления между множествами, подмножествами и отношениями в данной модели. Таким образом, модель может быть проверена и отмечены любые несогласованные определения. Классификатор также может выводить новую информацию, например определять новые наборы на основе существующей информации и изменять определение существующих наборов на основе новых данных. Уровень гибкости идеален для работы в постоянно меняющемся мире Интернета. Технология классификаторов построена на основе таких языков, как язык веб-онтологий, чтобы обеспечить логический семантический уровень существующего Интернета. Этот слой называется семантической сетью .
Временная логика используется для рассуждений в параллельных системах .
Смотрите также
использованная литература
дальнейшее чтение
- Бен-Ари, Мордехай (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 (ориентировано в основном на компьютерных ученых)