Актуальность исследования логики предикатов?

Друзья, приветствую каждого! Прошу знающих и понимающих математическую логику и, в том числе, логику предикатов людей объяснить мне простыми словами ЗАЧЕМ она нужна? В чем актуальность исследования этого раздела логики?

Выдали тему выпускной работы написать учебное ПО по анализу записи предикатных формул. В связи с этим хотела бы разобраться в чем актуальность такой программы, чем пригодилась бы автоматизация анализа таких формул. Функционал прог-мы будет включать определение связанной и свободной переменной, наличие повторов среди переменных, предложение вариантов для преобразования, нахождений обл.действия кванторов и тд и тп.
Благодаря этому в моей голове возникает тысяча и один вопрос зачем, например, определяется связанность переменных и где это дальше используется... В плане определений я уже все изучила, осталось понять для чего и зачем все это нужно))

Немного отмотаем назад, сразу хочу сказать, что гугл и иные поисковики меня не спасли, я изучила множество пособий и книг, но везде общими словами пишут, что вот она нужна для формализации высказываний и тд... и дальше уже описывают терминологию и кучу формул. А мне бы хотелось углубиться в подробности: каким именно образом формулы логики предикатов способствуют этой формализации, как они дальше перерастают в программный код и в каких областях (с подробностями КАК и ЗАЧЕМ) используются...

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

Благодарю за уделённое время и внимание, всем добра!)
  • Вопрос задан
  • 455 просмотров
Пригласить эксперта
Ответы на вопрос 3
hint000
@hint000
у админа три руки
Прежде всего, актуальность для вас в том, что это довольно хорошее упражнение, которое научит программировать не самые тривиальные штуки.
В реальной жизни, конечно, никакой новизны в этом нет. Существет софт, умеющий всё это и гораздо больше, на гораздо более продвинутом уровне, чем учащийся способен реализовать в выпускной работе.
гугл и иные поисковики меня не спасли
Ну вот это я нагуглил за несколько секунд, может быть вам это не попадалось, тут есть и про реальное применение.
https://ru.wikipedia.org/wiki/Автоматическое_доказ...
английская версия wiki описывает подробнее: https://en.wikipedia.org/wiki/Automated_theorem_proving
и автоматический перевод с английской версии: https://translated.turbopages.org/proxy_u/en-ru.ru...

https://habr.com/ru/post/519368/
и дальше уже описывают терминологию и кучу формул
Да, вот и они:
https://qudata.com/ds/ru/theory/theorem_proving.html
Кстати, с языком Prolog знакомы?
https://habr.com/ru/post/124636/
Ответ написан
Комментировать
Griboks
@Griboks
Если в двух словах, то это позволяет организовать ленивые вычисления и параллельные вычисления. Если вы можете просчитать логическую связь инструкций в программе, то вы сможете её оптимизировать, т.е. третьим направлением идут компиляторы.
Ответ написан
Комментировать
RAFAILgaley
@RAFAILgaley
Использование

Логика первого порядка как формальная модель рассуждений
Являясь формализованным аналогом обычной логики, логика первого порядка даёт возможность строго рассуждать об истинности и ложности утверждений и об их взаимосвязи, в частности, о логическом следовании одного утверждения из другого, или, например, об их эквивалентности. Рассмотрим классический пример формализации утверждений естественного языка в логике первого порядка.

Возьмём рассуждение «Каждый человек смертен. Сократ — человек. Следовательно, Сократ смертен». Обозначим «x есть человек» через ЧЕЛОВЕК(x) и «x смертен» через СМЕРТЕН(x). Тогда утверждение «каждый человек смертен» может быть представлено формулой: x(ЧЕЛОВЕК(x) → СМЕРТЕН(x)) утверждение «Сократ — человек» формулой ЧЕЛОВЕК(Сократ), и «Сократ смертен» формулой СМЕРТЕН(Сократ). Утверждение в целом теперь может быть записано формулой
Ответ написан
Комментировать
Ваш ответ на вопрос

Войдите, чтобы написать ответ

Войти через центр авторизации
Похожие вопросы