Эквивалентность при решении методом резолюций

[Kosat]

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

$a \longleftrightarrow b, a \longrightarrow c \Longrightarrow b \longrightarrow c;$
$(a \longrightarrow b), (a \longleftarrow b), b, \neg c;$
$( \neg a \vee b), ( \neg b \vee a), b, \neg c;$
$(( \neg a \vee b), ( \neg b \vee a)), b, \neg c;$
$( \neg b \vee b), b, \neg c;$
$b, \neg c;$

То есть отношение эквивалентности благодаря правилу резолюции всегда "схлопывается" в единицу. А этого быть не должно. Где же здесь ошибка? Помогите, пожалуйста.

Вот этот пример (я его придумал сам, так что не обессудьте):
Сократ - главный герой "Диалогов" (эквивалентность).
Сократ смертен (импликация).
Значит, главный герой "Диалогов" смертен (импликация).

[Sonic86]

Kosat в сообщении #829356 писал(а):

$(( \neg a \vee b), ( \neg b \vee a)), b, \neg c;$
$( \neg b \vee b), b, \neg c;$

Резольвенту Вы получили правильно, но исходные-то высказывания не надо выбрасывать, вот и все. Множество выводов в методе резолюции должно накапливаться.

Kosat в сообщении #829356 писал(а):

То есть отношение эквивалентности благодаря правилу резолюции всегда "схлопывается" в единицу.

Да, получается так.

Kosat в сообщении #829356 писал(а):

А этого быть не должно.

Почему бы и нет. Ведь вывод $(a\vee\bar{b})\wedge (\bar{a}\vee b)\vdash a\vee\bar{a}$ верен. Но он просто "необратим": $a\vee\bar{a} \not\vdash (a\vee\bar{b})\wedge (\bar{a}\vee b)$

[Kosat]

Большое спасибо, sonic86! Теперь проблема, которая беспокоила меня, разрешилась.

$a \longleftrightarrow b, a \longrightarrow c \Longrightarrow b \longrightarrow c;$

$(a \longrightarrow b), (a \longleftarrow b), b, \neg c;$

$( \neg a \vee b), ( \neg b \vee a), ( \neg a \vee с), b, \neg c;$

$(( \neg a \vee b), ( \neg b \vee a)), (( \neg a \vee с), \neg c), b;$

$( \neg b \vee b), ( \neg b \vee a), \neg a, b;$

$(( \neg b \vee a), \neg a), b;$

$\neg b, b;$

$\bot $

P.S. Сейчас может другие проблемы появятся.

Вот например:
Составить рекуррентное выражение для вычисления функции $f(n)=z^2 \bullet x+y$ (рекурсия проводится по переменной z), представив функции $h(x, y, z, m)$ и $g(x, y, z)$.

Что-то вообще ничего не вспоминается из того, что было на лекциях (правда, я не особо и ходил).

Есть ли какие-нибудь мысли?

[Deggial]

Kosat, новые вопросы оформляйте в виде отдельных тем.