Задача на предикаты (привести к предваренной нормальн форме)

[eugrita]

Профессор Снэйп в сообщении #111260 писал(а):

Ну и чем это "читабельней" по сравнению с вариантом автора? Меня, к примеру, отсутствие скобок после предикатов сильно раздражает. У Виктории они хоть стоят.
А что же вы хотели. Те же самые логики (Ян Лукасевич) изобрели "польскую запись" более удобную для алгоритма вычисления выражения чем скобочная запись, вычисление по которой - вообще говоря алгоритм обхода дерева, т.е. более сложный. По мне - так я вообще бы со школы в алгебре а потом и в логике запретил бы использование скобок , как архаичный способ, сбивающий учеников с толку, заменив все польской нотацией.
Pan mówił w języku polskim
to Виктория123: Что, совсем-совсем ничего не знаете? Как же Вам, бедненькой помочь?.. Давайте начнём со следующего:

1) Дайте определение предварённой нормальной формы (заодно хоть узнаем, к чему стремимся :) )

2) Пользуясь эквивалентностью $\Phi \rightarrow \Psi \equiv \neg \Phi \vee \Psi$, избавьтесь от импликаций в исходной формуле.

[eugrita]

Ладно. Задачу решили. А объясните кто-нибудь мне реальное применение либо в алгоритмах, либо в практической логике (для юристов и пр.) применение понятия "приведенная НФ" и "предварённая НФ" ?
Я бы даже сделал программу - логический калькулятор на вход которого по обычным правилам калькулятора с кнопками V * , отрицание, импликация и кванторов вводилась любая формула а на выходе ее же выражение преобразованное к предваренной и/или приведенной НФ.
Только я не понимаю, зачем это и кто будет пользоваться такой программой в отличие от обычного инженерного калькулятора

[Xaositect]

Про язык программироваия Prolog почитайте.

[eugrita]

Xaositect в сообщении #310800 писал(а):

Про язык программироваия Prolog почитайте.

Ну читал немного.хотите сказать что эти предваренная и др формы реализованы там? Ну и что? В основном большинству обычных людей он недоступен. А если я делаю программу, так хочу ее доступности. Между прочим программа "Калькулятор логических выражений" для логики высказываний есть на рынке и предлагается школьникам. (Видимо считается что большинство взрослых людей закоснели и математикой-логикой не интересуется). А аналогичного калькулятора для логики предикатов что-то не знаю.
Так вот и вопрос то. Логика предикатов почти во всех школах (за искл может математических лицеев 2 школа, 57 шк, интернат Колмогорова...) не изучается.
Подавляющая масса взрослых - далека от этого. Кому предлагать то?

[Xaositect]

Предваренная форма - это технический инструмент, непосредственно она не используется, но во всяких пруверах может являться одним из шагов упрощения выражения

[eugrita]

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

[Xaositect]

eugrita в сообщении #310819 писал(а):

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

Если не париться с красивостью формул, то любой приличный юникодный шрифт подойдет.
Или Delphi7 не умеет работать с юникодом? Я уже не помню, давно это было...

[eugrita]

Delphi 7 без TNT -компонент не умеет работать с Юникодом.
Но это не проблема. Логические символы есть и в шрифте Symbol,
так что проблем с выводом логических символов нет.
А вот как преобразовывать введенное пользователем выражение, да еще со скобками (дань традиционному представлению) - сначала ли в польскую, а потом в приведенную или предваренную формы - еще подумать надо. И здесь пригодиться топик данной темы

[eugrita]

А вообще в логике предикатов для меня наиболее темным местом остается распознавание субъектов и предикатов в предложении.Т.е. соотношение математической логики (оперирующей исходно с высказываниями и предикатами) и формальной логики (скажем для гуманитариев, философов, богословов), где все привязывается к фразе языка. Есть разные типы суждений обще- и частно- утвердительные, силлогизмы, даже логический квадрат... тип суждения определяет вид предикатов, т.е. в какой-то степени кванторы существования или единственности, входящую в формулу предложения. Интересно, каков должен быть алгоритм разбора предложения на предикаты и построения логической предикатной формулы. Это вроде задача лингвистики. Возможно алгоритм решения зависит от правил построения фраз языка на котором написано предложение (суждение).

[Профессор Снэйп]

Самое сложное в математике --- перемены кванторов.

Когда высказывание находится в предварённой (пренексной) нормальной форме, сразу видно, сколько в нём перемен кванторов и какая у него сложность.

Есть такая штука --- арифметическая иерархия, в теории вычислимости один из основных объектов. Вот там обсуждаемый алгоритм применяется и даёт оценку сложности отношения. Называется алгоритм Тарского-Куратовского.

[eugrita]

Спасибо. Ознакомлюсь

[Чудо-в-перьях]

eugrita в сообщении #310951 писал(а):

А вообще в логике предикатов для меня наиболее темным местом остается распознавание субъектов и предикатов в предложении.Т.е. соотношение математической логики (оперирующей исходно с высказываниями и предикатами) и формальной логики (скажем для гуманитариев, философов, богословов), где все привязывается к фразе языка. Есть разные типы суждений обще- и частно- утвердительные, силлогизмы, даже логический квадрат... тип суждения определяет вид предикатов, т.е. в какой-то степени кванторы существования или единственности, входящую в формулу предложения. Интересно, каков должен быть алгоритм разбора предложения на предикаты и построения логической предикатной формулы. Это вроде задача лингвистики. Возможно алгоритм решения зависит от правил построения фраз языка на котором написано предложение (суждение).

Я преподавала логику для гуманитариев, и мы договаривались различать субъекты и предикаты следующим образом: субъект - это грамматическое подлежащее и все относящиеся к нему термины, а предикат - грамматическое сказуемое и все зависящие от него термины. Например, предложение "Нек-рые сдобные булочки не являются безумно вкусными" формализуется на языке КЛП следующим образом: субъект $S$ -"сдобные булочки"; предикат $P$ -"безумно вкусные" и при первом приближении у нас получается следующая логическая форма $\exists x(S(x)\wedge\neg P(x))$ Потом мы учились, в случае сложного субъекта или/и предиката, разбивать их на составные части (например в данном примере выраж. "сдобные булочки" можно разбить на два конъюнкта - "сдобный"и "вкусный"), но это у моих студентов был уже продвинутый уровень :))

-- Вс янв 16, 2011 14:39:23 --

Не могу не встрять в дискуссию о пруверах: одно время у нас на кафедре было модно писать пруверы для различных исчислений. Мой собственный диссер был посвящен алгоритму для такого прувера и, соответственно, самому пруверу - для натуральных исчислений типа Куайна, к-рый работал в КЛВ и различных силлогистических системах (КЛВ расширялась до силлогистических исчислений). Хоть прувер получился рабочим и вполне эффективным, со студентами я все равно его очень мало использую (надо же их заставить самостоятельно овладевать исчислениями, а то прувер так и будет за них считать - причем студенты согласны со мной::) и считаю на нем сама - по мере необходимости
Кроме того, нижняя граница сложности алгоритма, лежащего в его основе, оказалась $EXPTIME$, и на математической конференции, куда мы с прувером поехали, он был интеллегентно забракован и оставлен для решения задча для "малых и средних данных" - т.е. как раз для студентов, к-рые должны учиться решать сами::)
Т.о, написание автоматических генераторов доказательств - вещь неблагодарная.
Лучше писать интерактивные, обучающие пруверы, где требуется активное участие студиоза. Жаль, что такие пруверы - и очень хорошие- уже есть:))