Доказать теорему

2.2. A1:

T:

Получим дизъюнкты.

Д1:

Д2:

Чтобы получить дизъюнкты из теоремы, надо взять ее отрицание.

Д3:

Д4:

Д5:

Таким образом получаем систему дизъюнктов:

Д1:

Д2:

Д3:

Д4:

Д5:

Вывод:

1. Унифицируем Д1 и Д3: ,
получаем

2. Получаем резольвенту Д1-Д3: , обозначим ее как Д6

3. Унифицируем Д6 и Д4: ,
получаем

4. Получаем резольвенту Д6-Д4: , обозначим ее как Д7

5. Унифицируем Д7 и Д5: ,
получаем

6. Получаем резольвенту Д7-Д5:  (пустой дизъюнкт)

Теорема доказана.

2.4. А1:
Т:

Получим дизъюнкты.

Д1:

Чтобы получить дизъюнкты из теоремы, надо взять ее отрицание.

Д2:

Таким образом получаем систему дизъюнктов:

Д1:

Д2:

???

Вывод:

1. Унифицируем Д1 и Д2: ,
получаем

2. Получаем резольвенту Д1-Д2: