Дулепов Е.Г., Ефремова А.Н.

Россия, Братский государственный университет

Теорема как инструмент анализа логической состоятельности утверждений

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

Утверждение, истинность которого доказана при условии предлагается считать логически состоятельным. Таким условием может выступать, в частности, выполнение полученного после формализации некоторого текстового документа в форме закона, договора, заявления, или его истинности. Показано, что введение в структуру теоремы переменных и постоянных величин делает ее не разовым, а постоянно действующим компьютерным инновационным инструментом исследования.

Ключевые слова: логическая состоятельность утверждения, обобщенная посылка теоремы, общее знание об объекте исследования.

Введение. Теорема – математическое утверждение, истинность которого устанавливают или опровергают с помощью доказательств.

Теоремы логики высказываний доказуемы [1], отсюда следует возможность построения универсального алгоритма доказательства теорем и преобразования последнего в инструмент анализа логической состоятельности утверждений. Структура теоремы как инструмента исследования и ее программная реализация частично изложены в [2,3].

Для доказательства теорем в логике высказываний чаще всего используют отношение порядка, которое существует между причиной и следствием. Со времен Аристотеля отношение порядка, как более общее, чем отношение эквивалентности, в форме правила вывода под латинским названием modus ponens широко использует современная логика и математика.

Теорема может устанавливать существование различных бинарных отношений между двумя утверждениями и , в частности, отношений эквивалентности и порядка. Действительно, существование двух теорем – прямой и обратной означает существование отношения эквивалентности , а существование одной из теорем или – отношения порядка.

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

Понятие в форме множества не имеет истинностной оценки, однако имеет ее – в форме тождественно-истинного логического произведения, сомножителями которого являются тождественно-истинные выражения, утверждающие все эти признаки [4]. Такую форму представления знаний в дальнейшем будем считать основной.

Постановка задачи. Рассмотрим структурную организацию теоремы как инструмента решения прикладных задач и перечислим методики решения некоторых из их.

Теорема представляет собой умозаключение в форме истинного условного предложения «если все посылки или гипотезы f₁, …, f_k истинны, то истинным будет и заключение или вывод f_зак»:

f₁ , … , f_k f_зак .

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

обобщенной посылкой f_оп , f_оп = f₁ … f_k , тогда теорема примет вид

f_оп f_зак .

В отличие от импликации f_оп f_зак в теореме f_оп f_зак посылка _, откуда следует, что область существования теоремы f_оп f_зак – это область истинности обобщенной посылки f_оп .

В рассматриваемом ниже универсальном алгоритме доказательства теорем логики высказываний, каждая из функций f₁ , …, f_k, f_зак зависит от одного и того же набора аргументов, часть которых может быть фиктивными. Если через Е_ОП и Е_ЗАК обозначить области истинности f_оп и f_зак , то критерий G существования теоремы f_оп f_зак будет означать выполнение условий (f_оп 0) и (f_оп f_зак ) или условия (Е_ОП Ø)(Е_ОП Е_ЗАК ), задаваемых предикатами:

G=( f_оп 0)&( f_оп f_зак) или G= (Е_ОП Ø)(Е_ОП Е_ЗАК ).

Универсальный алгоритм предполагает выполнение следующих условий:

1. Определение набора всех попарно различных аргументов функций для f_оп и f_зак и вычисление их совершенных ДНФ (СДНФ);

2. Вычисление значения критерия G существования теоремы по формулам

G=( f_оп 0)( f_оп f_зак) или G = (Е_ОП Ø) ( Е_ОП Е_ЗАК ).

Докажем, например, логическую состоятельность утверждения в форме известной с древности сложной конструктивной дилеммы

.

Решение.

1. Определяем набор () аргументов дилеммы и СДНФ функций

,

СДНФ

СДНФ;

2. Определяем множества Е_ОП , Е_ЗАК :

Е_ОП Ø, Е_ЗАК =и

вычисляем значение истинности критерия G:

G=( f_оп 0)( f_оп f_зак) или

G=( Е_ОП Ø)(Е_ОП Е_ЗАК ) =

=(Е_ОП Ø)&.

Вывод: логическая состоятельность дилеммы доказана, так как

Компьютерное решение по программе показано на рис. 1. В первой строке решения приведена запись дилеммы на языке программирования, связь между логическими операциями и символам языка устанавливает табл. 1.

Таблица 1

И	ИЛИ	НЕ	ЕСЛИ ТО	Разделитель «» посылки и заключения
&	|	!	>	;

утверждение , программа

решение:

Рис. 1 – Утверждение дилеммы

Для построения инструмента анализа логической состоятельности утверждений обобщенную посылку f_оп в утверждении f_оп f_зак выразим через общее знание о предмете и гипотезу , тогда утверждение будет иметь вид

В результате процедуры формализации утверждения о гипотезах, общих знаниях и заключениях переводятся на язык алгебры логики [2].

Гипотеза и заключение в утверждении – величины переменные, определяемые внешними причинами, например рынком, а общее знание о предмете – величина постоянная, она может быть определена логическим законом, договором, заявлением и записана в форме решения логического уравнения или утверждена теоремой .

Вывод: введение в структуру теоремы переменных и постоянных величин делает ее не разовым, а постоянно действующим компьютерным инновационным инструментом исследования.

Покажем работу теоремы как компьютерного инструмента при решении следующих прикладных задач с помощью программы [3]:

1. Мониторинг коммерческого договора;

2. Упрощение формул функций алгебры логики;

3. Выявление свойств функций и отношений между функциями.

Результаты решения прикладных задач

Задача №1. Мониторинг коммерческого договора:

Если курс доллара высок , то товар следует продавать в Китае , в противном случае , товар следует продавать в Братске» . Договор – это общее знание: === ^{= 1.}

^{Cокр ДНФ Мин ДНФ}

утверждение , программа , решение:

договор будет нарушен, так как он предполагает продажу товара не в Китае, а в Братске

утверждение , программа, решение:

договор будет выполнен, так как он предполагает продажу товара в Китае

Рис. 2 – Компьютерный мониторинг договора

Компьютерное решение задачи для и показано на рис. 2, оно устанавливает выполнение или логическую состоятельность договора .

Упрощение формул функций алгебры логики.

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

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

Для выявления лишних сомножителей в произведении и лишних слагаемых в сумме можно использовать универсальный алгоритм доказательства и опровержения утверждений профессора Дулепова Е.Г. [4]:

1. Если – теорема, то слагаемое – лишнее;

2. Если – теорема, то сомножитель – лишний.

Задача 2. В логической сумме определить являются ли лишними слагаемые и .

Компьютерные решения задачи показаны на рис. 3.

утверждение, программа, решение: , слагаемое - нелишнее

утверждение, программа, решение: , слагаемое - лишнее

Рис. 3 – Компьютерное упрощение логической суммы

Задача 3. В произведении определить являются ли лишними сомножители и .

Компьютерные решения задачи показаны на рис. 4.

Утверждение ,

программа,

решение: , сомножитель - нелишний.

утверждение,

программа ,

решение: , сомножитель - лишний.

Рис. 4 – Компьютерное упрощение логического произведения

Выявление свойств функций и отношений между функциями.

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

Как следует из решений задач 3 и 4, пары функций и , и связаны отношением порядка, а пары функций и , и – отношением эквивалентности.

Задача 4. Установить является ли функция самодвойственной?

Решение. Функция является самодвойственной, если она равна двойственной по отношению к ней функции , то есть если

Компьютерное решение показано на рис. 5.

Утверждение

программа

решение:

Рис. 5 – Компьютерное установление самодвойственности

Выводы

1. Теоремы логики высказываний доказуемы, отсюда следуют возможности построения универсального алгоритма для доказательства теорем и преобразования его в инструмент анализа логической состоятельности утверждений.

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

3. Введение в структуру теоремы переменных величин в виде гипотезы и заключения, определяемых, например, рынком, и постоянной величины, представляющей собой общее знание, например, в форме некоторого закона, договора, заявления делает теорем не разовым, а постоянно действующим компьютерным инновационным инструментом исследования;

Литература:

1. Gentzen K. Untersuchungen über das logische Dchlissen, Math. Zeitschrift, 1934 – 1935. T. 39.

2. Дулепов Е.Г., Ефремова А.Н. Структура и возможности универсального алгоритма доказательства теорем, // Системы. Методы. Технологии: научный периодический журнал № 2(10). – Братск: ГОУ ВПО «БрГУ», 2011. C.71–73.

3. Свидетельство о государственной регистрации программы для ЭВМ “Анализ логической состоятельности договора» (AnCont v. 1.00) / Витковский С.Л., Дулепов Е.Г., Кравченко Е.В. Заявка № 2013610966. Зарегистрировано в Реестре программ для ЭВМ 9 января 2013 г.

4. Е.Г. Дулепов. Теоретические основы вычислительной техники: Монография, Братс. гос. унт. – Братск, 2008.–236с: ил.– Библиогр. 14 назв. – Рус. – Деп. в ВИНИТИ. 04.07.2008, № 578 – В2008.