- •Введение
- •Глава 1. Ведение в системы искусственного интеллекта
- •1.1. Архитектура систем искусственного интеллекта
- •1.2. База знаний и данных
- •1.1.1 Понятие модели
- •1.1.2. Логические модели
- •1.1.3 Модели знаний на основе продукций
- •1.1.4 Фреймовая модель знаний
- •1.1.5 Семантические сети
- •1.3. Машина вывода
- •1.3.1. Понятие формальной системы
- •Примеры стратегии вывода
- •Как функционирует машина вывода
- •1.4. Извлечение знаний и обучение
- •1.4.1. Извлечение знаний от многих экспертов
- •1.4.2 Проблема непротиворечивости формализованной базы знаний
- •1.5. Обучение системы
- •1.6. Интерфейс с пользователем
- •1.7. Организация работы
- •1.8. Инструментальные средства создания систем искусственного интеллекта
- •Языки программирования
- •1.8.2. Языки продукционного программирования
- •1. 8. 3. Языки инженерии знаний и инструментальные системы
- •1.8.3.1. Система vpExpert
- •1.8.3.2. Система kas
- •1.8.3.3. Система Expert-Ease
- •Глава 2. База знаний
- •2.1. Методы извлечения знаний
- •2.1.1. Классификация методов извлечения знаний
- •2.1.2. Пассивные методы
- •2.1.2.1. Наблюдения
- •2.1.2.2. Анализ протоколов «мыслей вслух»
- •2.1.2.3. Лекции
- •2.1.3. Активные индивидуальные методы
- •2.1.3.1. Анкетирование
- •2.1.3.2. Интервью
- •2.1.3.3. Свободный диалог
- •2.1.4. Активные групповые методы
- •2.1.4.1. «Круглый стол»
- •2.1.4.2. «Мозговой штурм»
- •2.1.4.3. Экспертные игры
- •2.1.4.3.1. Игры с экспертом
- •2.1.4.3.2. Ролевые игры в группе
- •2.1.4.4. Игры с тренажерами
- •2.1.4.4.1. Компьютерные экспертные игры
- •2.1.5. Текстологические методы
- •2.2.Формальное описание понятий предметной области (по)
- •2.2.1. Методы абстрагирования понятий
- •2.2.1.1.Агрегация и декомпозиция понятий
- •2.2.1.2.Обобщение и специализация понятий
- •2.2.1.3.Типизация и конкретизация понятий
- •2.2.1.4.Ассоциация и индивидуализация понятий
- •2.3.Методы классификации
- •2.3.1. Экстенсиональный и интенсиональный аспекты классификации
- •2.3.2. Таксономия и мерономия
- •2.3.3. Типы классификаций
- •2.3.4. Древовидные классификации
- •2.3.5. Булевы классификации
- •2.3.6. Комбинативные классификации
- •2.4.События и процессы
- •2.4.1. Состояния предметной области
- •2.4.2. Событие
- •2.4.3. Последовательные процессы
- •2.4.4. Рекурсивные процессы
- •2.4.5. Ветвящиеся процессы
- •2.5. Системы продукций: структура, технология, применение
- •2.5.1. Неформальное введение в системы продукций
- •2.5.1.1 Алгоритмические модели
- •2.5.2 Логический вывод
- •2.5.3 Прикладные модели
- •2.5.4. Метамодель систем продукций
- •2.5.4.1. Основные подсистемы
- •2.5.5.2. Метаструктура базы данных и операций
- •2.5.5.2.1. Характер организации данных
- •2.5.5.2.2 Операции над базой данных
- •2.5.5.2.3 Контроль несовместимости
- •2.5.5.2.4 Ассоциативная надстройка
- •2.5.6. Метаструктура модуля правил
- •2.5.6.1 Аппарат активации
- •2.5.6.2 Структура правил
- •2.5.7. Метаструктура модуля управления
- •2.5.8. Технология поддержки разработок продукционных систем
- •2.5.9. Формальные модели систем продукций
- •2.5.9.1. Алгебраическая модель
- •2.5.9.1.1. Основные определения
- •2.5.9.1.2. Операции преобразования ситуации
- •2.5.9.1.3. Условия корректности вычислений над конъюнктивной базой данных
- •2.5.9.1.4. Однозначность вычислений над дизъюнктивной базой
- •2.5.9.2. Управление выводом в системах продукций
- •2.5.9.3. Язык управления применением продукций
- •2.5.9.4. Язык управления выбором данных
- •2.5.9.5. Обзор формальных моделей вычислений
- •2.5.10. Экспериментальные системы продукций
- •2.5.10.1. Система скип
- •2.5.10.2. Система анализа топологических чертежей интегральных схем
- •P(слой) x0, y0 : Dx1, Dy2, .., Dxn-1, Dyn;
- •2.6. Выводы к второй главе
- •3. Машина логического вывода
- •3.1. Формальное определение задачи
- •3.2. Специфика решения задач в сии
- •3.3. Управление процессом решения задачи
- •3.4. Модели эвристического поиска решений
- •3.4.1 Стратегия поиска в глубину
- •3.4.2. Стратегии перебора с отсечениями
- •3.4.2.1. Метод ветвей и границ
- •3.4.2.2. Стратегии поиска на основе эвристической функции оценки
- •3.5. Методы вывода и доказательства теорем
- •3.5.1 Механизм резолюции Робинсона
- •3.5.2. Резолюция в логике высказываний
- •3.5.2.1 Линейная резолюция вL
- •Метод линейного вывода в lЛавленда, Ковальского и Кюнера
- •Эффективная реализация
- •3.5.2.3. Метод поиска в глубину
- •3.5.2.4 Эвристики поиска в дереве
- •3.5.2.5. Семантическая резолюция
- •3.5.3 Резолюция в pl
- •3.6. Методы индуктивного вывода
- •3.6.1. Виды индукции
- •3.6.2. Индукция как вывод и индукция как метод
- •3.6.3. Правила, необходимые для систем автоматического формирования знаний
- •3.7. Дедуктивный вывод на семантических сетях
- •3.7.1. Нерезолютивные методы вывода на семантических сетях
3.5.2.5. Семантическая резолюция
Обратимся теперь к стратегии семантической резолюции, предложенной Слэйглом. Стратегия на основе семантической резолюции также использует упорядочение литер, как и OL-резолюция. Кроме того, эта стратегия основывается на разделении всего множества исходных и порождаемых дизъюнктов на два непересекающихся класса, назовем ихТиF. Такое разбиение возможно, если задать некоторую интерпретациюIдля формул исходного множества. В интерпретацииIчасть дизъюнктов окажется истинной, а часть ложной. Множество истинных дизъюнктов в интерпретацииI- это по определению множествоТ; множество ложных дизъюнктов в интерпретацииI- это по определению есть множествоF.
При построении вывода требуется выполнение двух условий:
резольвента строится для дизъюнктовС1иС2таких, чтоС1 T, аC2 F
отсекаемая литера в дизъюнктеС2должна быть самой правой литерой.
Пусть E1, E2, ..., Eqнекоторое множество дизъюнктов, принадлежащихF, аN- дизъюнкт изТ.
Тогда множество {E1, E2, ..., Eq, N} называется клашем, если выполняется следующее условие:
R1 = N;
i < 1, Ri+1есть резольвентаRi-1иEi-1; отсекаемая литера - старшая вEi(самая правая);
Rq+1 F.
Rq+1называется резольвентой данного клаша.
Пример. Пусть
C1 = R ,
C2 = P R,
C3 = Q R,
C4 = ,
P > Q > R >
Пусть в интерпретации I R- ложен,Р- ложен,Q- ложен. Тогда клашами являются множества
K1 = {С3, C4},
K2 = {C2, C4}.
Вывод на основе семантической резолюции строится так, что каждый дизъюнкт либо принадлежит исходному множеству дизъюнктов, либо является резольвентой некоторого клаша.
Так резольвентой С5клашаК1являетсяQ; резольвентойС6клашаК2являетсяР.
Резольвентой С5иС1является дизъюнктC7 = R .
Резольвентой С7иС6является дизъюнктС8 = R.
Резольвентой дизъюнктов С8иС4является.
3.5.3 Резолюция в pl
Применению OL-вывода в PLпредшествует подготовительный этап, предложенный Девисом и Патнемом. Он включает в себя 3 стадии:
преобразование формулы в ПНФ;
преобразование матрицы в КНФ;
преобразование формулы в ССФ.
С реализацией второй стадии вы хорошо знакомы, поэтому рассмотрим 1-ю и 3-ю стадии.
В Lимеются две нормальные формы: ДНФ и КНФ, вPLроль нормальной формы играет ПНФ – предваренная нормальная форма.
Определение: Говорят, что формулаFвPLнаходится в ПНФ тогда и только тогда, когда формулаFимеет вид:(Q1x1)…(Qnxn)(M), где(Qixi) (i=1,…,n) есть либо(xi),либо(xi) иМесть формула, не содержащая кванторов.
(Q1x1)…(Qnxn) называется префиксом формулыF, М – матрицей формулыF.
Для преобразования формулы Fв ПНФ используются законы эквивалентных преобразований, называемых законами принесения кванторов через и :
(1а) (Qx)F(x)G=(Qx)(F(x)G)
(1б) (Qx)F(x)G=(Qx)(F(x)G)
(2а) ((x)F(x))=(x)(F(x))
(2б) ((x)F(x))=(x)(F(x))
(3а) (x)F(x)(x)M(x)=( x)( F(x)M(x))
(3б) (x)F(x)(x)M(x)=( x)( F(x)M(x))
Однако инельзяпроносить черезисоответственно. В подобных случаях нужно поступать специальным образом. Т.к. каждая связанная переменная в формуле может рассматриваться лишь как место для подстановки какой угодно переменной, то каждую связанную переменнуюхможно переименовать вzи формула(x)M(x) перейдет в(z)M(z), т.е.(x)M(x)= (z)M(z). Предположим, что мы выбираем переменнуюz, которая не встречается вF(x). Тогда(x)F(x) (x)M(x)= (x)F(x) (z)M(z) путем замены всехх, входящих в(x)M(x) наz, тогда согласно (1а):
(4а) (x)F(x) (x)M(x)= (x)(z)(F(x) M(z))
(4б) (x)F(x) (x)M(x)= (x)(z)(F(x) M(z)).
Преобразование формул в ПНФ:
используем законы, чтобы исключить логические связки и
(5) FG=(FG)(GF)
(6) FG=FG
используем законы, чтобы пронести знак отрицания внутрь формулы
(7) (F)=F
(8) (FG)=FG
(9) (FG)=FG
(10) ((x)F(x))=(x)(F(x))
(11) ((x)F(x))=(x)(F(x))
переименовываем связанные переменные, если это необходимо
используем законы (1а–4б), чтобы вынести кванторы в самое начало формулы для получения формулы, находящейся в ПНФ.
Пример 1: приведем формулу(x)P(x)(x)Q(x).
(x)P(x)(x)Q(x)=
=((x)P(x))(x)Q(x)= по (6)
=(x)(P(x))(x)Q(x)= по (2а)
=(x)(P(x)Q(x)) по (3б)
где (x) – префикс, а(P(x)Q(x)) – матрица.
Пример 2: получить ПНФ для формулы:
(x)(y)((z)P(x,z)P(y,z)) (u)Q(x,y,u))=
= (x)(y)(((z)P(x,z)P(y,z))) (u)Q(x,y,u))= по (6)
= (x)(y)(z)(P(x,z)P(y,z)) (u)Q(x,y,u))= по (2б) и (9)
= (x)(y)(z)(u)(P(x,z)P(y,z)) Q(x,y,u)) по (1а)
где (x)(y)(z)(u) – префикс, а (P(x,z)P(y,z)) Q(x,y,u)) – матрица.
Рассмотрим вопрос преобразования формулы F в скулемовскую стандартную форму (ССФ).
Для этого мы должны, сохраняя противоречивость формулы, элиминировать в ней кванторы существования путем использования скулемовских функций.
Условимся, что формула F находится в ПНФ:
(Q1x1)…(Qnxn)M, гдеМв свою очередь находится в КНФ, тогда:
выберем самый левый квантор существования Qr в префиксе(Q1x1)…(Qnxn) (1rn);
если никакой не стоит в префиксе левееQr, то выберем новую константуС, отличную от других констант, входящих вМ, заменим всехr, встречающиеся вМ, наСи вычеркнем(Qrxr) из префикса;
Если Qs1,…,Qsm – список всех, стоящих левееQr,(1S1<S2<…<Sm<r), то выберем новыйm-местный функциональный символf, отличный от других функциональных символов, заменим всеxr вM наf(xs1,…,xsm) и вычеркнем (Qr,xr) из префикса;
Весь этот процесс применим для всех в префиксе, двигаясь слева направо (следует отметить, что порядок выбора из префикса несущественен).
Последняя из полученных формул и есть ССФ формулы F (или просто стандартная форма формулыF). Константы и функции, используемые для замены переменных, называются скулемовскими функциями.
Пример 1: получить стандартную форму формулы(x)(y)(z)(u)(v)(w) P(x,y,z,u,v,w).
В этой формуле левее (x) нет ни одного, значит заменяемх наа.
(u) находится(y)(z), значит заменяемu наf(y,z)
(w) находится(y)(z)(v), значит заменяемw наg(y,z,v).
Тогда (y)(z)(v)P(a,y,z,f(y,z),v,g(y,z,v)) – стандартная форма.
При использовании процедур опровержения не происходит потери общности, поэтому при доказательстве кванторы общности можно опустить.
Рассмотрим теперь непосредственно метод резолюций, применяемый в PL при построенииOL-вывода.
Как и в Lздесь существенным является нахождение в дизъюнкте литеры, которая контрарна литере в другом дизъюнкте. Рассмотрим дизъюнкты:С1: P(x)Q(x) иC2: P(f(x))R(x).
С первого взгляда в С1нет литеры, контрарной какой-либо литере в С2, однако если подставитьf(0)вместоxвС1иaвместоxвC2, то получим: С1’: P(f(a))Q(f(a)) иC2’: P(f(a))R(a).
C1’ иC2’ называютсяосновными примерамиС1и С2соответственно, аP(f(a)) иP(f(a))контрарны друг другу. Следовательно, изC1’ иC2’ можно получить резольвенту:
C3’: Q(f(a))R(a).
В общем случае, подставив f(x) вместоx вC1, получим:C1*: P(f(x))Q(f(x)). СноваС1* есть примерС1. ЛитераP(f(x)) изС1* контрарна литереP(f(x)), тогда резольвента С1* иС2:
С3: Q(f(x))R(x).
При этом С3’ является примеромС3. Кроме того, дизъюнктС3 является наибольшим общим дизъюнктом в том смысле, что все другие дизъюнкты, порожденные подобным образом, есть приме
С3 будем называть резольвентойС1 и С2. Таким образом, получение резольвенты из двух дизъюнктов вPL связано с подстановкой.
Определение: Подстановка– это конечное множество вида{t1/v1,…,tn/vn}, где каждаяvi – переменная, аti – терм, отличный отvi, при этом всеvi различны. Еслиt1,…,tn – основные термы, то подстановка называетсяосновной. Подстановка, которая не содержит элементов, называетсяпустойи обозначается. Будем использовать греческие буквы для обозначения подстановки.
Определение: Пусть ={t1/v1,…,tn/vn} – подстановка иЕ – выражение. ТогдаЕ – выражение, полученное изЕзаменой одновременно всех вхождений переменнойvi (1in) вЕнаti.Е называютпримеромЕ.
Определение: Пусть ={t1/x1,…,tn/xn} и={u1/y1,…,um/ym} – две подстановки. Тогдакомпозиция есть подстановка, которая получается из множества{t1/x1,…,tn/xn,u1/y1,…,um/ym} вычеркиванием всех элементовtj/xj, для которыхtj = xj, и всех элементовui/yi, таких чтоyi{x1,…,xn}.
Пример: ={t1/x1, t2/x2}={f(y)/x, z/y}
={u1/y1, u2/y2, u3/y3}={a/x, b/y, y/z}, тогда
={t1/x1, t2/x2, u1/y1, u2/y2, u3/y3}={ f(y)/x, z/y, a/x, b/y, y/z}
Так как t2=x2, а именноz/y, то этот элемент вычеркивается из множестваy1 иy2 {x1, x2, x3}, т.е.a/x иb/y должны быть тоже вычеркнуты. Таким образом, получаем:={f(b)/x, y/z}.
Композиция подстановок ассоциативна, а пустая подстановка есть одновременно и левое и правое тождество, т.е.()=() и= для всех,, .
В процедуре доказательства по методу резолюций зачистую приходится отождествлять контрарные пары литер. Для этого необходимо унифицировать (склеивать) два и более выражение, т.е. мы должны найти подстановку, которая может сделать несколько выражений тождественными.
Рассмотрим унификацию выражений.
Определение: Подстановка называетсяунификаторомдля множества{E1,…,Ek} E1 =E2 =…=Ek.
Говорят, что множество {E1,…,Ek} унифицируемо, если для него существует унификатор.
Определение: Унификатор для множества выражений{E1,…,En} будет наиболее общим унификатором (НОУ)для каждого унификатора для этого множества существует такая подстановка, что = .
Определение: Множество рассогласований D непустого множества выраженийW получается выявлением первой (слева) позиции аргумента, на которой не для всех выражений изWстоит один и тот же символ.
Алгоритм унификации
Множество k = 0, Wk = W, k =.
Если Wk – единичный дизъюнкт, то остановка,k – НОУ дляW, иначе найдем множество рассогласованийDk дляWk.
Если существуют такие элементы vk иtk вDk, чтоvk – переменная, не входящая вtk,то перейдем к шагу 4. В противном случае остановка:W не унифицировано.
Пусть k+1=k{tk/vk}и Wk+1=Wk{tk/vk}
Присвоить значение k+1 и перейти к шагу 2.
Пример: Найти НОУ для W={P(a,x,f(g(y))),P(z,f(z),f(u))}.
v0= иw0=w
D0={a,z}. Переменной в этом множестве являетсяz, значитv0=z, аt0=a
v1=v0{t0/v0} = {a/z}={a/z}, w1=w0{t0/v0}={P(a, x, f(g(y))), P(z, f(z), f(u))} {a/z} = {P(a, x, f(g(y))), P(a, f(a), f(u))}
w1 – не единичный элемент.D1={x,f(a)}
Из D1 следуетv1=x,t1=f(a)
v2=v1{t1/v1} = {a/z}{f(u)/x}={a/z,f(u)/x},w2=w1{t1/v1}={P(a,x,f(g(y))),P(a,f(a),f(u))}{f(a)/x} = {P(a,f(a),f(g(y))),P(a,f(a),f(u))}
Для w2: D2={g(y),u}, v2=u, t2=g(y)
v3=v2{t2/v2} = {a/z, f(u)/x}{g(y)/u}={a/z, f(u)/x, g(y)/u} w3=w2{t2/v2}={P(a, f(a), f(g(y))), P(a, f(a), f(u))} {g(y)/u} = {P(a, f(a), f(g(y))), P(a, f(a), f(g(y)))}={P(a, f(a), f(g(y)))}
3= {a/z, f(a)/x, g(y)/u} – НОУ для W.
Пример:
S={M(a, S(c), S(b)), P(a), M(x, x, S(x)), M(x, y, z) M(y, z, x), M(x, y, z) D(x, z), D(a, b), P(w) M(y,z,z) D(w,z) D(w,x) D(w,y)}
Введем дополнительные определения.
Дизъюнктесть дизъюнкция литер. Иногда когда это удобно, мы будем рассматриватьмножество литеркак синонимдизъюнкта. Например,P Q R = {P, Q, R}.
Дизъюнкт, содержащий rлитер, называетсяr- литерным дизъюнктом;
Однолитерный дизъюнкт называется единичным дизъюнктом;
Когда дизъюнкт не содержит никаких литер, мы называем его пустым дизъюнктом.
Дизъюнкты P(x, f(x)) R(x,f(x),g(x)) и Q(x,g(x)) R(x, f(x), g(x))суть дизъюнкты. Считаем, что множество дизъюнктовSесть конъюнкция всех дизъюнктов изS, где каждая переменная вSсчитается управляемой квантором всеобщности. Благодаря этому соглашению стандартная форма может быть просто представлена множеством дизъюнктов. Например, стандартная форма впримере 2может быть представлена множеством
S = {P(x, f(x)) R(x, f(x), g(x)), Q(x, g(x)) R(x, f(x), g(x))}.
Мы можем элиминировать кванторы существования, сохраняя противоречивость формулы. Формула Fпротиворечива (не выполнена)не существует интерпретация, которая удовлетворяетF. Покажем это в следующей теореме.
Теорема 1.ПустьS– множество дизъюнктов, которые представляют стандартную форму формулыF. ТогдаFпротиворечива в том и только в том случае, когдаSпротиворечива.
Доказательство. Без потери общности можно положить, чтоFнаходится в предваренной нормальной форме, т.е.F = (Q1x1) … … (Qnxn) M [x1, …, xn]. (Мы используемM [x1, …, …, xn],чтобы указать, что матрицаМ содержит переменныеx1, …, xn).ПустьQr– первый квантор существования. ПустьF1 = (x1) … (xr-1) (Qr+1xr+1) … (Qnxn) M [x1, …, xr-1, f(x1, …, xr-1), xr+1, …, xn], гдеf – скулемовская функция, соответствующаяxr, 1 r n. Мы хотим показать, чтоFпротиворечива тогда и только тогда, когдаF1противоречива.
Предположим, что Fпротиворечива, аF1непротиворечива, еслиF1непротиворечива, то существует такая интерпретацияI, чтоF1истинна вI. Это означает, что для всехx1,…, xr-1существует по крайней мере один элемент , для которого формула(Qr+1xr+1) … (Qnxn) M[x1, …, …, xr-1 , f(x1, …, xr-1), xr+1 , …, xn]истинна вI. И этим элементом являетсяf (x1, …, xr-1).Таким образом,Fистинна вI, что противоречит предположению, чтоFппротиворечива. Следовательно,F1должна быть противоречива.
Предположим, что F1противоречива, аFнепротиворечива. ЕслиFнепротиворечива, то существует такая интерпретацияIна областиD, чтоFистинна вI, т.е. для всех x1, …, xr-1 существует такой элементхr, что(Qr+1xr+1) … (Qnxn) M[x1, …, …, xr-1, xr, xr+1, …, xn] истинна вI.
Расширим интерпретацию I, включая функциюf, которая отображает(x1 , …, …, xr-1)наxrдля всехx1, …, …, xr-1 вD, т.е.f (x1 , …, …, xr-1) = xr.Пусть это расширениеIобозначаетсяI'. Ясно, что для всехx1 , …, …, xr-1 (Qr+1xr+1) … (Qnxn) M[x1, …, …, xr-1 , f( x1 , …, …, xr-1) xr+1, …, xn]истинна вI', т.е.F1истинна вI', что противоречит предположению, чтоF1 противоречива. Следовательно,Fдолжна быть противоречивой. Мы разобрали случай, когда формула имеет один. Предположим теперь, что вF имеетсяmкванторов существования. ПустьF0 = F. ПустьFkполучается изFk -1заменой первого квантора существования вFk--1скулемовской функцией,k = 1, …, m. Следовательно, мы заключаем, чтоFпротиворечива тогда и только тогда, когдаSпротиворечива, что и требовалось доказать.
Пусть S- стандартная форма формулыF. ЕслиFпротиворечива, то потеореме 1 F = S. ЕслиFнепротиворечива, заметим, что, вообще говоря,Fне эквивалентнаS. Например, пустьF = (x) P(x) и S = P(a). Ясно, чтоSесть следующая интерпретация:
Область: D = {1, 2}.
Значения для а:
___а___
1
Значения для Р:
_________Р______
P(1) P(2)
Л И
Тогда ясно, что F истинна в I, но S ложна в I. Таким образом, F S.
Отметим, что формула может быть иметь более чем одну стандартную форму. Ради простоты, когда мы преобразуем формулу Fв стандартную формуS, мы будем заменять кванторы существования скулемовскими функциями настолько простыми, насколько возможно. Дальше, если мы имеемF = F1 … Fn,мы можем отдельно получить множество дизъюнктовSi, i = 1, …, n.Затем пустьS =S1U …U Sn. С помощью рассуждений, подобных тем, которые даны в доказательстветеоремы 1, нетрудно увидеть, чтоFпротиворечива тогда и только тогда, когдаSпротиворечива.
Пример 3. В этом примере покажем, как выразить следующую теорему в стандартной форме.
Если х*х = едля всеххв группеG, где*есть бинарный оператор иеесть единица группыG, тоGкоммутативна.
Сначала формализуем эту теорему вместе с некоторыми основными аксиомами теории групп и затем представим отрицание этой теоремы множеством дизъюнктов.
Известно, что группаGудовлетворяет следующим четырем аксиомам:
A1: x, y Gвлечетx*y G(свойство замкнутости);
A2: x, y, z Gвлечетx*(y*z) = (x*y)*z(свойство ассоциативности);
A3: x*e = e*x=xдля всехx G(свойство существования единичного элемента);
A4: для каждого элементаxGсуществует элементx-1Gтакой, чтоx*x-1 = x-1*x = e(свойство существования обратного элемента).
Пусть P(x, y, z) обозначаетx*y = z и i(x)обозначаетx-1. Тогда вышестоящие аксиомы примут вид:
A'1: (x) (y) (z) P(x, y, z);
A'2: (x) (y) (z) (u) (v) (w) (P (x, y, u) P(y, z, v) P(u, z, w) P(x, v, w)) (x) (y) (z) (u) (v) (w) (P (x, y, u) P(y, z, v) P(x, v, w)P(u, z, w));
A'3: (x) P (x, e, x) (x) P (e, x, x);
A'4: (x) P (x, i (x), e) (x) P (i(x), x, e).
Заключение теоремы такое:
B: Еслих*х = е для всехх G, тоGкоммутативна, т.е.u*v = v*uдля всехu,v G.
Вможет быть представлено формулой
B':(x) P(x, x, e) ((u) (v) (w) (P(u, v, w)P(v, u, w))).
Теперь вся формула представляется формулой F = A'1 … A'4B'. Таким образом,F = A'1 A'2 A'3 A'4 B'. Чтобы получить множество дизъюнктовSдляF, сперва получим множество дизъюнктовSiдля каждой аксиомыA’i = 1, 2, 3, 4,следующим образом:
S’1: {P (x, y, f(x, y))};
S’2: {P(x, y, u) P(y, z, v) P(u, z, w) P(x, v, w),
P(x, y, u) P(y, z, v) P(x, v, w) P(u, z, w)};
S3: {P(x, e, x), P(e, x, x)};
S4: {P(x, i(x), e), P(i(x), x, e)}.
Так как
B’ = ((x) P(x, x, e) ((u) (v) (w) (P(u, v, w) P(v, u, w))))
= ((x) P(x, x, e) ((u) (v) (w) (P(u, v, w) P(v, u, w))))
= (x) P(x, x, e) ((u) (v) (w) (P(u, v, w) P(v, u, w)))
= (x) P(x, x, e) ((u) (v) (w) (P(u, v, w) P(v, u, w))).
то множество дизъюнктов для B’дается ниже.
T: {P(x, x, e), P(a, b, c), P(b, a, c)}.
Таким образом, множество S = S1 S2 S3 S4 Tесть множество, состоящее из следующих дизъюнктов:
P(x, y, F(x, y)),
(2) P(x, y, u) P(y, z, v) P(u, z, w) P(x, v, w),
(3) P(x, y, u) P(y, z, v) P(x, v, w) P(u, z, w),
P(x, e, x),
P(e, x, x),
P(x, i(x), e),
P(i(x), x, e),
P(x, x, e),
P(a, b, c),
P(b, a, c).
Пример 3показывает, как получить множество дизъюнктовSдля формулы F. Изтеоремы 1известно, чтоFобщезначима тогда и только тогда, когдаSпротиворечива. Как говорилось в начале этого параграфа, для доказательства теоремы будем использовать процедуру опровержения. Таким образом, с этого места мы будем предполагать, что на входе процедуры опровержения стоит всегда множество дизъюнктов (такое как множествоS, полученное в приведенном выше примере). Дальше мы будем использовать для множества дизъюнктов термины«невыполнимо» («выполнимо») вместо«противоречиво» («непротиворечиво»).