Моделирование рассуждений. Опыт анализа мыслительных актов, стр. 17

Пусть, например, надо узнать, выводима ли в исчислении высказываний формула ((

Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
?
Моделирование рассуждений. Опыт анализа мыслительных актов - rarr.png
?)
Моделирование рассуждений. Опыт анализа мыслительных актов - rarr.png
?). В эту формулу входит одно высказывание ?. Поэтому нужно проверить лишь две комбинации истинности: когда ? истинно и когда оно ложно. В первом случае по свойству импликации первая скобка является истинной, ибо
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
? ложно. Но тогда истинна и вся формула, ибо импликация истинна, когда истинны ее левая и правая части. Если же ? ложно, то первая скобка является ложной, так как левая часть импликации (
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
?
Моделирование рассуждений. Опыт анализа мыслительных актов - rarr.png
?) истинна, а правая ложна. Но тогда вся формула является истинной. Тем самым доказано, что интересующая нас формула является тождественно истинной и, следовательно, выводимой в исчислении высказываний.

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

Проиллюстрируем эту процедуру еще на одном примере. Проверим, является ли выводимой формула ((?

Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
?)
Моделирование рассуждений. Опыт анализа мыслительных актов - rarr.png
((
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
?
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
?)&?)). В этой формуле (будем обозначать ее ?) имеется три высказывания, что приводит к необходимости рассмотрения истинного значения ? на 23=8 комбинациях. Эти комбинации и соответствующие шаги по определению истинностного значения ? на них даны в табл. 3, в которой И и Л означают соответственно значения «истина» и «ложь».

Таблица 3

Моделирование рассуждений. Опыт анализа мыслительных актов - p074_1.png

Появление в пятой строке в столбце ? значения Л свидетельствует о невыводимости исследуемой формулы. На этом шаге процесс вывода можно прекратить. Остальные строки в таблице приведены лишь для полноты картины.

«Логик-теоретик»

Так была названа программа для ЭВМ, созданная в середине шестидесятых годов американским кибернетиком А. Ньюэллом в содружестве с психологом Г. Саймоном. Она была предназначена для доказательства теорем в исчислении высказываний, т.е. для поиска обоснования тождественной истинности некоторых утверждений. Для того чтобы перейти к описанию программы «Логик-теоретик», введем предварительно понятие о равенстве двух выражений исчисления высказываний. Будем говорить, что выражения ?1 и ?2 равны между собой, и записывать этот факт обычным образом ?1=?2, если на всех возможных наборах интерпретации истинности входящих в них элементарных высказываний истинность ?1 и ?2 одинакова.

Появление знака равенства, которого не было в исчислении высказываний, не должно нас смущать. Его легко можно исключить из рассмотрения, введя формулу ((?1&?2)

Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
(
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
?1&
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
?2)). Читатели могут проверить, что эта формула будет истинной только в том случае, когда оценки истинности ?1 и ?2 одинаковы. Тогда утверждение, что ?1=?2, становится эквивалентным утверждению, что формула ((?1&?2)
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
(
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
?1&
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
?2)) является истинной.

«Логик-теоретик» должен был доказывать справедливость утверждений вида ?1=?2 для различных ?1 и ?2. Однако авторы «Логика-теоретика» не пошли по прямому пути. Не стали строить таблицы для ?1 и ?2 и проверять совпадение истинности ?1 и ?2 на всех возможных интерпретациях истинности их аргументов. Ведь с ростом числа аргументов n число строк в этих таблицах растет как 2n. А. Ньюэлл и Г. Саймон пошли по пути приближения процедуры доказательства к тому, как это делают люди.

В основу процесса доказательства они положили идею ликвидации различий в формульной записи ?1 и ?2. Авторы программы составили перечень из шести различий.

1. В ?1 и ?2 различное число членов в формулах. Например, ?1=?

Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
Моделирование рассуждений. Опыт анализа мыслительных актов - alpha_overlined.png
?, а ?2=?
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
? [6].

2. В ?1 и ?2 имеется различие в основной связке (т.е. в связке, которая выполняется последней). Например, ?1=(??)

Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
(
Моделирование рассуждений. Опыт анализа мыслительных актов - alpha_overlined.png
Моделирование рассуждений. Опыт анализа мыслительных актов - beta_overlined.png
), а ?2=(?
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
Моделирование рассуждений. Опыт анализа мыслительных актов - beta_overlined.png
)
Моделирование рассуждений. Опыт анализа мыслительных актов - rarr.png
?.

3. Перед всем выражением для ?1(?2) стоит знак отрицания, а перед ?2(?1) его нет. Например, ?1=

Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
(?
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
?), а ?2=??.

4. Аналогичное различие, но оно касается не всего выражения для ?i (i=1,2), а некоторого его подвыражения.

5. Скобки в ?1 расставлены не так, как в ?2. Например, ?1=?

Моделирование рассуждений. Опыт анализа мыслительных актов - rarr.png
(?
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
?), а ?2=(?
Моделирование рассуждений. Опыт анализа мыслительных актов - rarr.png
?)
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
?.

6. Записи для ?1 и ?2 отличаются порядком следования подвыражений. Например, ?1=(??)

Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
?, а ?2=?
Моделирование рассуждений. Опыт анализа мыслительных актов - or.png
(??).

Для того чтобы иметь возможность ликвидировать подобные различия, используются 12 преобразований формул исчисления высказываний. Первые семь преобразований носят тождественный характер, т.е. не меняют истинного значения преобразуемых формул. Последние пять верны только при условии, что левая часть их является тождественно истинной (T–выражением).

Моделирование рассуждений. Опыт анализа мыслительных актов - p076_1.png

В преобразованиях использованы большие латинские буквы, которые могут соответствовать любым подвыражениям формул ?1 и ?2. Стрелки

Моделирование рассуждений. Опыт анализа мыслительных актов - rarrow.png
и
Моделирование рассуждений. Опыт анализа мыслительных актов - bidirarrow.png
показывают направление преобразований. (Знак
Моделирование рассуждений. Опыт анализа мыслительных актов - rarrow.png
есть по сути знак
Моделирование рассуждений. Опыт анализа мыслительных актов - perpendicular.png
.)

вернуться

6

Для более компактной записи формул будем писать

Моделирование рассуждений. Опыт анализа мыслительных актов - alpha_overlined.png
вместо
Моделирование рассуждений. Опыт анализа мыслительных актов - not.png
? и опускать знак конъюнкции там, где это не мешает однозначному пониманию формулы.