Основы построения и функционирования интеллектуальных информационных систем. Былкин В.Д - 27 стр.

UptoLike

ВУЗ: 

ПГУ | Пенза

Составители: 

Рубрика: 

27
Исследование выводимости 24 модусов, верных в силлогистике Аристотеля, в ИП привело
к следующему результату. Если предполагать, что все классы сущностей не пуста, то приведенная
выше замена силлогистических выражений формулами ЛП будет полностью справедлива. При
допущении пустых классов сущностей оказываются невыводимыми все модусы силлогистики, в
которых вывод носит частный характер, а обе посылки носят, общий характер.
Формализация процесса доказательства в логике предикатов
Доказательство демонстрирует, что некоторая формула ЛП является теоремой на заданном
множестве аксиом , т. е. результатом, логически выводимым из аксиом.
Положим, что = {A
1
, A
2
, ... , A
n
}, а теорема есть B. В таком случае можно утверждать, что
доказательство показывает общезначимость формулы вида:
A
1
& A
2
& ... & An B (4.1)
Такое определение эквивалентно тому, что отрицание формулы (4.1.), т.е. формула ¬ (A
1
& A
2
& ...
& An B) является невыполнимой формулой. Ниже представлено поэтапное приведение формул
ЛП к клаузальной форме, используемой в методе резолюций одном из наиболее эффективных
методов доказательств в ЛП. Следует отметить, что не существует алгоритма, позволявшего
распознать общеназначимостъ, выполнимость или невыполнимость произвольной формулы ЛП.
Пусть задана формула A логики предикатов. Формула B называется предваренной нормальной
формой кия формулы A , если она удовлетворяет ниже перечисленным требованиям:
1. Формулы А и B равносильны.
2. Формула B удовлетворяет следующим условиям:
а) используются логические операции ┐, v , & , при этом отрицание применяется только в
атомарных формулах;
б) операции применения кванторов следуют за операциями алгебры высказываний ¬, &, v.
Алгоритм получения предваренной нормальной формы представлен ниже.
Шаг 1. Исключить связки эквивалентности ( ~ ) и импликации (→). Формула x ~ у заменяется на
(x → у) & (x → у), а формула A → B заменяется на (Ā v B). 
       Исследование выводимости 24 модусов, верных в силлогистике Аристотеля, в ИП привело
к следующему результату. Если предполагать, что все классы сущностей не пуста, то приведенная
выше замена силлогистических выражений формулами ЛП будет полностью справедлива. При
допущении пустых классов сущностей оказываются невыводимыми все модусы силлогистики, в
которых вывод носит частный характер, а обе посылки носят, общий характер.
Формализация процесса доказательства в логике предикатов
Доказательство демонстрирует, что некоторая формула ЛП является теоремой на заданном
множестве аксиом , т. е. результатом, логически выводимым из аксиом.
Положим, что         = {A1 , A2 , ... , An }, а теорема есть B. В таком случае можно утверждать, что
доказательство показывает общезначимость формулы вида:
A1 & A2 & ... & An      B (4.1)
Такое определение эквивалентно тому, что отрицание формулы (4.1.), т.е. формула ¬ (A1 & A2 & ...
& An    B) является невыполнимой формулой. Ниже представлено поэтапное приведение формул
ЛП к клаузальной форме, используемой в методе резолюций одном из наиболее эффективных
методов доказательств в ЛП. Следует отметить, что не существует алгоритма, позволявшего
распознать общеназначимостъ, выполнимость или невыполнимость произвольной формулы ЛП.
Пусть задана формула A логики предикатов. Формула B называется предваренной нормальной
формой кия формулы A , если она удовлетворяет ниже перечисленным требованиям:
1. Формулы А и B равносильны.
2. Формула B удовлетворяет следующим условиям:
а) используются логические операции          ┐, v , & , при этом отрицание применяется только в
атомарных формулах;
б) операции применения кванторов следуют за операциями алгебры высказываний ¬, &, v.
Алгоритм получения предваренной нормальной формы представлен ниже.
Шаг 1. Исключить связки эквивалентности ( ~ ) и импликации (→). Формула x ~ у         заменяется на
(x → у) & (x → у), а формула A → B заменяется на (Ā v B).




                                                  27

Страницы