Причина для изучения логики высказываний и предикатов

Я могу понять важность того, что компьютерные ученые или любые инженеры, связанные с разработкой программного обеспечения, должны были понимать основы логики как основу.

Но есть ли какие-либо задачи / задания, которые явно требуют знания об этом, кроме задач, которые требуют какого-либо представления знаний с использованием Knowledge Base? Я хочу услышать типы задач, а не концептуальные ответы.

Причина, по которой я спрашиваю это, просто из моего любопытства. В то время как студенты CS должны потратить определенное количество времени на этот предмет, некоторые интенсивные курсы (например, AI-класс ) полностью пропустили эту тему. И мне просто интересно, что, например, знание predicate logicможет помочь рисовать, ER diagramно не может быть обязательным требованием.

Обновление 27.05.2012) Спасибо за ответы. Теперь я думаю, что полностью понимаю и согласен с важностью использования logicCS в огромном количестве приложений. Я только что выбрал лучший ответ из впечатляющего решения, которое я получил благодаря решению проблемы Windows«синего экрана».

Мне нравится Объединение и все, что с ним связано. Если вы не знаете логику высказываний и предикатов, вы пропускаете основы логики. Если у вас есть интерес к чему-либо из перечисленного , то это все равно, что интересоваться математикой, пропуская сложение и умножение. Логика не только для ИИ.

В качестве практического ответа вспомните проблему Intel с плавающей точкой и как вы их больше не видите? Благодаря использованию доказателей теорем они ушли в прошлое. Вспомните синий экран смерти Microsoft . Благодаря SAT решателям, проверке моделей и другим решениям на основе логики, они находятся под угрозой исчезновения.

Есть очень глубокая и повсеместная связь между логикой и информатикой. Чтобы понять, какими они могут быть, имейте в виду, что компьютерные науки также называют «информационными технологиями» или «информатикой», что означает, что компьютерные системы собирают, обрабатывают и доставляют информацию. Ну, логика - вещь похожая. Он изучает, как информация собирается в предложениях и как возможно, чтобы одно утверждение было следствием другого, т. Е. Как его информационное содержание уже присутствует в другом утверждении (или совокупности утверждений). В этом смысле логика и информатика - это одно и то жедисциплина, ориентируясь на разные аспекты. Логики (Черч, Клин, Тьюринг, Пост и их ученики и коллеги) создали дисциплину «Информатика», и многие логики продолжают вносить свой вклад в информатику, особенно Жан-Ив Жирар и его ученики.

Вот некоторые стандартные приложения логики в информатике:

• Проектирование цифровых схем полностью основано на логике предложения, настолько, что его инженеры называют это «логическим дизайном», а не «схемотехникой». Считается, что даже написание компьютерной программы предполагает разработку ее «логики». (Обратите внимание, что «логика» в последнем смысле - это неформальная идея, а не формальная логика, используемая для обозначения потока информации через программу и правильности ее обработки.)

• Логика предикатов и ее математическая родственница, теория множеств, используются в различных вычислительных языках , например, в языке SQL для запросов к реляционной базе данных. Существуют также языки программирования, основанные на логике, называемые «языки логического программирования».

• Представление знаний , о котором вы уже упоминали, имеет много формализмов, основанных на логике. Даже если он использует нелогические формализмы, многие из них все же имеют логическое значение и, следовательно, основаны на логике.

• Вероятностная логика, где утверждения имеют не только истинные / ложные значения, но и уровни уверенности / неопределенности, все чаще становится основой для систем машинного обучения .

• Если вы хотите официально заявить о том, что делает программа, то есть дать спецификацию программы , вы в конечном итоге будете использовать какую-то форму логического языка. Действительно, существует много языков спецификации программ, таких как Z и B, которые основаны на логике предикатов и теории множеств. Существуют также языки спецификации, основанные на эквациональной логике, такие как Larch. Ученые-информатики часто изобретают новую логику для представления потребностей информатики, например, логику Хоара и логику разделения, или они выбирают и развивают различные недоиспользуемые формы традиционной логики, такие как временная логика и модальная логика, и развивают их дальше.

• Если вы хотите проверить , выполняет ли программа то, что должна, то в конечном итоге вы используете не только язык логики, но и весь механизм логики: теорию доказательств, теорию моделей и процедуры принятия решений. Технологии верификации сейчас растут как на дрожжах, и я ожидаю, что примерно через десятилетие они будут использоваться практически для любой разработки программного обеспечения.

На самом деле, связи между логикой и информатикой настолько глубоки и распространены, что я бы сказал, что трудно быть хорошим ученым без глубокого понимания логики.

Причина, по которой некоторые ученые ИИ недооценивают логику в настоящее время, заключается в том, что некоторые из первых разработчиков ИИ предложили готовую логику в качестве инструмента.а не фундамент. ИИ по своей природе обещает доставить магию. Нам не нужно выполнять тяжелую работу по программированию систем для достижения результатов. Они смогут сами понять, как создавать решения, потому что они будут «умными». Логика, казалось, указывала путь, потому что, если компьютерные системы понимали логику и знали, как обрабатывать информацию, используя правила логики, они были бы способны создавать магию. Вера в логику в ретроспективе была неуместна. Во-первых, готовая логика слишком сильна и слишком слаба одновременно. Он слишком силен в том смысле, что логические правила слишком общие, чтобы разрабатывать эффективные процедуры. Это также слишком слабо, потому что это логика, разработанная математиками для нужд математики, и она не у него есть словарь, необходимый для работы со множеством других видов информации реального мира, с которыми должны работать системы ИИ (таких как неопределенность, контекстная информация, такая как время, изменения, знания, агентство и так далее). Таким образом, ИИ в настоящее время подвергается негативной реакции против логики. Но я думаю, что, когда они преодолеют эту обратную реакцию, ученые ИИ поймут, что все более новые методы все еще основаны налогика, в широком смысле .

Логика является фундаментальной для всей теоретической информатики. Без их изучения вы не сможете правильно понять семантику языка программирования, машины Тьюринга, логическое программирование, вычислимость и так далее. Даже рассуждения о ваших программах будут сложнее без него. Конечно, попытка сделать математическое доказательство некоторой концепции КС практически невозможна.

Или, может быть, вы спрашиваете об использовании в промышленности. Изучение логики составляет основу для обучения четкому рассуждению и видению дыр в аргументах других людей. Логика фундаментальна, используете ли вы формальные символы или нет.

Одна из повторяющихся задач, с которыми сталкиваются специалисты и теоретики CS, - это обретение уверенности в правильности своего кода.

Есть два основных подхода:

1. Доказательство: придумайте логическое доказательство того, что часть системы обладает определенными свойствами, возможно, благодаря предварительным условиям, проектированию по контракту, проверке кода.
2. Тестирование: проверьте, что определенные свойства сохраняются для различных входных данных, а затем определите, что это свойство сохраняется для других входных данных.

Первый, основанный на логических методах, часто является единственным вариантом, когда

1. Там нет типичного ввода. Например, при тестировании свойств безопасности вам следует беспокоиться о нетипичных входных данных, поэтому, если вы не сможете логически обосновать, какие входные данные являются нетипичными, вы вряд ли получите хорошее покрытие.
2. Пространство конфигурации очень велико, поэтому вы должны разбить его на части, логически рассуждая о том, какие части могут повлиять на какие другие, прежде чем проводить локальное тестирование.
3. У вас есть только документация, описывающая поведение пограничных систем вне вашего контроля. Возможно, вы сможете имитировать их, но не сможете проверить, что происходит в случае сбоя внешней зависимости, потому что вы не способны ее вызвать по юридическим или этическим причинам.

Эмпирическое тестирование в отсутствие доказательства является в основном заменой доказательства. Когда вы разрабатываете систему, пригодную для тестирования, вы создаете эскиз доказательства, в котором вы заполняете части доказательства с помощью «теста X, Y и Z здесь». Способность логически рассуждать крайне важна для разработки тестируемой системы. Если система не подлежит тестированию или доказуемости, то ее разработчик / архитектор не имеет права утверждать, что она подходит для использования по назначению.

Две наиболее важные области, которые логика играет жизненно важную роль:

1. Формальная спецификация языка и проверка .
2. Фиксированный параметр tractable классов .

$Z$

Вкратце: 1. Определение языка нуждается в логике, 2: Справедливость его процедур нуждается в логике, 3. Процедура верификации нуждается в логике.

Я должен отметить, что это отличается от дизайна компилятора или ..., это "Формальное" определение языков, основной причиной для этого является доказательство правильности языка или модели, также имеющее формальное доказательство. Это может быть использовано при проверке моделей программного обеспечения, поиске ошибок перед реализацией, повторном обнаружении взаимоблокировок перед реализацией .... Для программного обеспечения, имитирующего это, вы можете взглянуть на NModel .

Теперь, почему в задачах с фиксированным параметром вам нужно работать с логикой, вы можете разделить классы возможности фиксированного параметра с разными уровнями логики, они могут быть преобразованы друг в друга: логика в автоматы, автоматы в граф и наоборот, но если вы являетесь экспертом в области логики, вы можете разделить и решить их просто, самая важная теорема (после теоремы Робертсона и Сеймура ), в этой области - теорема Курселя . для получения дополнительной информации читайте обзор мета-алгоритмической теоремы .