Следовательно, при истинности всех посылок и истинности импликации заключение всегда будет истинным.
B.
Это правило называют modus tollens (m.t.).
Это правило называют modus ponens (m.p.).
Правила заключения
Это правило тождественно аксиоме А2;
12) если формулы F1 и (F1®F2) имеют значение “и”, то истинной является формула F2, т.е
F1; (F1®F2)
F2.
Эта запись при истинном значении посылки F1 и импликации (F1®F2) позволяет удалить логическую связку импликации и определить истинное значение заключения F2;
13) если формулы ù F2 и (F1®F2) имеют значение “и”, то истинной является формула ù F1, т.е
ù F2; (F1®F2)
ù F1.
Эта запись при истинном значении посылки ù F2 и импликации (F1®F2) позволяет удалить логическую связку импликации и определить истинное значение заключения ù F1;
14) если формулы (F1®F2) и (F2®F1) имеют значение “и”, то истинной является формула (F1«F2), т.е
( F1®F2); (F2®F1)
(F1«F2).
Эта запись при истинном значении (F1®F2) и (F2®F1) позволяет ввести логическую связку эквиваленции и определить значение формулы (F1«F2);
15) если формула (F1«F2) имеет значение “и”, то истинными являются формулы (F1®F2) и (F2®F1), т.е
(F1«F2) (F1«F2)
(F1®F2) и (F2®F1).
Эта запись при истинном значении (F1«F2) позволяет удалить логическую связку эквиваленции и определить истинное значение формул (F1®F2) и (F2®F1).
При выводе формулы из множества аксиом и посылок используют два основных правила:
а) если Fi и ( Fi ® Fj ) есть выводимые формулы, то Fj также выводимая формула, т.е.
Fi; (Fi®Fj)
Fj.
b) если формулы ù Fj и (Fi®Fj) есть выводимые формулы, то ù Fi также выводимая формула, т.е
ù Fj; (Fi®Fj)
ù Fi.
Пример: Суждение: “Сумма внутренних углов многоугольника равна 180о (А). Если сумма внутренних углов многоугольника равна 180о (A), то многоугольник есть треугольник (В). Следовательно, дан треугольник”.
А;A®B
Пример: Суждение: ”Дан не треугольник (ù B); если сумма внутренних углов многоугольника равна 180о(А), то многоугольник есть треугольник (В). Следовательно, сумма внутренних углов многоугольника не равна 180о(ùA)”.
ù B; A®B
ùA.
1.3. Метод дедуктивного вывода
Как уже отмечалось, теорема F1; F2;...Fn|¾В равносильна доказательству |¾(F1&F2&...&Fn®B ). Если каждая Fi=и, то F1&F2&...&Fn )=и, а если (F1&F2&...&Fn®B)=и, то В=и.
Используя правила эквивалентных преобразований алгебры высказываний, можно показать дедуктивный характер вывода заключения:
1) |¾(F1&F2&...&Fn®B);
2) |¾(ù(F1&F2&...&Fn )ÚB);
3) |¾(ùF1ÚùF2 Ú...ÚùFnÚB);
4) |¾(ùF1ÚùF2 Ú...ÚùFn-1Ú(Fn®B));
5) |¾(ùF1ÚùF2 Ú...Ú(Fn-1®(Fn®B)));
6) |¾(ùF1Ú(F2 ®...®(Fn-1®(Fn®B))...));
7) |¾(F1®(F2 ®...®(Fn-1®(Fn®B))...)
Так формируется система дедуктивного вывода от посылок до заключения.
5) F5=D®B заключение по формулам F3 и F4 и аксиоме А2 или правилу 11).
1.4 Принцип резолюции
Существует эффективный алгоритм логического вывода - алгоритм резолюции. Этот алгоритм основан на том, что выводимость формулы В из множества посылок F1; F2; F3; . . . Fn равносильна доказательству теоремы
|¾(F1&F2&F3&. . .&Fn®B),
формулу которой можно преобразовать так:
|¾(F1&F2&F3&. . .&Fn®B) =
|¾(ù(F1&F2&F3&. . .&Fn)ÚB) =
|¾ù(F1&F2&F3&. . .&Fn&( F2ù B)).
Следовательно, заключение В истинно тогда и только тогда, когда формула (F1&F2&F3&...&Fn&(ùB))=л. Это возможно при значении “л” хотя бы одной из подформул Fi илиùB.
Для анализа этой формулы все подформулы Fi иùB должны быть приведены в конъюнктивную нормальную форму и сформировано множество дизъюнктов, на которые распадаются все подформулы. Два дизъюнкта этого множества, содержащие пропозициональные переменные с противоположными знаками (контрарные атомы) формируют третий дизъюнкт - резольвенту, в которой будут исключены контрарные пропозициональные переменные. Неоднократно применяя это правило к множеству дизъюнктов и резольвент, стремятся получить пустой дизъюнкт. Наличие пустого дизъюнкта свидетельствует о выполнении условия F1&F2&F3&...&Fn&ùB=л.
