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

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

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

 

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

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

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

 

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

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

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

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

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

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

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

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

f1 , … , fk   fзак .

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

обобщенной посылкой  fоп ,   fоп = f1   fk ,  тогда теорема примет вид

       fоп  fзак  .

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

В рассматриваемом ниже универсальном алгоритме доказательства теорем логики высказываний, каждая из функций  f1 , …,  fk,  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.***