Вспомогательные выводы в ИВ

[Sinoid]

Здравствуйте! Вот я конъюнкцию из сомножителей (содержащих по одной переменной) вывел в другой задаче. Сейчас я получил более сложные сомножители. И мне нужно вывести их конъюнкцию. Скажите, пожалуйста, мне снова повторять по пунктам вывод конъюнкции?

[Xaositect]

Не обязательно, конечно, раз Вы это понимаете. Напишите где-нибудь себе лемму $A, B \vdash A \wedge B$, и ссылайтесь на нее.

[Sinoid]

А вот еще один момент. Доказательство теоремы о индукции конструктивно само по себе. При решении конкретной задачи я непосредственно пользуюсь пунктами этого доказательства. Вот я хочу получить вывод $(A\supset B)$ из списка $\Gamma$. Для этого я, как обычно, записал вывод $B$ из $\Gamma,\,\{A\}$, приписал к формулам этого вывода посылку $A$. И в ходе решения задачи выяснилось, что в выводе нужной мне формулы $(A\supset B)$ некоторые формулы вывода $B$ из $\Gamma,\,\{A\}$ с приписанной посылкой $A$ просто не участвуют. Мне же в чистовом варианте не нужно записывать выводы еще и этих формул?

[arseniiv]

Не нужно, но если не требуется предъявить полный вывод, а только факт выводимости чего-то из чего-то, можно даже его не строить. Или можно написать программу, которая к выводу сама применяет теорему о дедукции. (И ещё проверяет оба вывода, правильны ли они.) Тогда, если это успешно получится, можно будет позволить себе уж точно не расписывать её применение.

[Sinoid]

arseniiv в сообщении #1190859 писал(а):

Или можно написать программу, которая к выводу сама применяет теорему о дедукции. (И ещё проверяет оба вывода, правильны ли они.)

Ну, это мне еще о-очень долго не грозит. А вы не знаете калькулятора, который вычисляет СКНФ СДНФ? А то я точно знаю, что такие калькуляторы существуют (один ТС писал, что разные калькуляторы дают разные ответы - бывает же такое), а названий ни от кого не могу добиться.

[arseniiv]

Калькулятора не знаю, для всяких мелких подсчётов или пользуюсь Mathematica или пишу сам на чём-нибудь.

Попробовал в Wolfram|Alpha, но никак не удалось заставить выдать именно СДНФ. Можно таблицу истинности там попросить, а потом тривиально обработать.

[kernel1983]

Sinoid в сообщении #1191140 писал(а):

А вы не знаете калькулятора, который вычисляет СКНФ СДНФ?

http://tablica-istinnosti.ru

[Sinoid]

kernel1983 в сообщении #1191281 писал(а):

http://tablica-istinnosti.ru

Там у меня "Содержимое заблокировано, ... т.к. не подписано..." да и хочется иметь калькулятор на своем компе.

arseniiv в сообщении #1191280 писал(а):

или пишу сам на чём-нибудь.

arseniiv, скажите, пожалуйста, вы доктор каких-то наук? Просто вы столько обо всем знаете, столько умеете.

[knizhnik]

Sinoid в сообщении #1191297 писал(а):

arseniiv, скажите, пожалуйста, вы доктор каких-то наук? Просто вы столько обо всем знаете, столько умеете.

Да, скажите пожалуйста. Удваиваю этот вопрос

[arseniiv]

Оттуда писал(а):

Так как все значения в таблице истинности равны 0, то данная функция не имеет СДНФ.

Выдумщики. Намного удобнее считать, что она есть пустая дизъюнкция. А уж как её представлять — константу ли 0 рисовать или с самого начала считать СДНФ не формулой, а множеством формул — это уж на выбор.

Sinoid в сообщении #1191297 писал(а):

arseniiv, скажите, пожалуйста, вы доктор каких-то наук? Просто вы столько обо всем знаете, столько умеете.

Если я много пишу, это ещё не значит, что я много что-то ещё.

[Sinoid]

arseniiv в сообщении #1191349 писал(а):

Оттуда
писал(а):
Так как все значения в таблице истинности равны 0, то данная функция не имеет СДНФ. Выдумщики. Намного удобнее считать, что она есть пустая дизъюнкция.

Это писал не я, но я это знаю.

arseniiv в сообщении #1191349 писал(а):

А уж как её представлять — константу ли 0 рисовать или с самого начала считать СДНФ не формулой, а множеством формул — это уж на выбор.

то есть при таком понимании, например, $X\wedge\neg Y\vee\neg X\wedge Y$ будет представляться множеством из одного элемента $\{X\wedge\neg Y\vee\neg X\wedge Y\}$, противоречие - $\{\}$?

[arseniiv]

Sinoid в сообщении #1191426 писал(а):

то есть при таком понимании, например, $X\wedge\neg Y\vee\neg X\wedge Y$ будет представляться множеством из одного элемента $\{X\wedge\neg Y\vee\neg X\wedge Y\}$, противоречие - $\{\}$?

Первое — множеством из двух $\{X\wedge\neg Y,\neg X\wedge Y\}$, да и то если переменных только две интересуют. Если три — из четырёх и т. д., но это верно и случае СДНФ как формулы тоже.

[Sinoid]

Так это получается, при таком подходе только для дизъюнкции будет взаимно однозначное соответствие такого понимания СДНФ.

[arseniiv]

Взаимно однозначное соответствие с чем?

[Sinoid]

Я имел ввиду вот что. Если формуле $\phi_1$ однозначно соответствует множество $A_1$ конъюнктов ее СДНФ, а $\phi_2$ - $A_2$, то формуле $\phi_1 \vee \phi_2$ будет соответствовать множество $A_1 \cup A_2$. Со взаимной однозначностью перемудрил.