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