Автоматическое доказательство теорем

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

Метод, что контролирует соотношение G |-T S для формулы S, множества формул G и теории T именуется методом автоматического доказательства теорем.

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

Теорема 7.1. В случае если G, OS |- F, где F – любое несоответствие, то G |- S.

Подтверждение. В случае если G, OS |- F, то GU(OS)|- F, поскольку GU(OS)|- G и GU(OS)|- OS. Следовательно, |- GU(OS) ® F. Так как

GU(OS) ® F º º º º ,

то |- и, следовательно, G |- S.

Способ резолюций трудится со стандартной формой формул, именуемой предложениями. Предложением именуется бескванторная дизъюнкция литералов. Каждая формула исчисления предикатов возможно преобразована в множество предложений по следующему методу.

1. Выстроить предварённую обычную форму формулы. Отметим, что для этого необходимо:

a) преобразовать формулу к приведённому виду, т.е. исключить операцию ® и спустить операцию отрицания до атомарных формул;

b) совершить разделение связанных переменных;

c) вынести операции связывания переменных в начало формулы.

2. Преобразовать предварённую обычную форму в предклазуальную, т.е. привести матрицу U обычной формы к КНФ.

3. Совершить сколемизацию обычной формы (выстроить клазуальную обычную форму, исключив операции связывания переменных).

4. Удалить операции U (дизъюнкции клазуальной обычной формы составят искомое множество предложений).

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

Определение. Пускай – предложения исчисления высказываний, такие что , . Правило вывода

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

Замечание. Многие рассмотренные ранее правила вывода являются частными случаями правила резолюции. К примеру, главное правило исчисления ИВ – правило заключения возможно представить в виде .

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

Задание 1. Доказать способом резолюций |- .

Ответ. В данном примере G – пусто, . Преобразуем формулу в множество предложений.

º º

º º º

º º

1. A

2.

3. OA

4. ?

Применив к предложениям 1, 3 правило резолюции, возьмём пустую формулу, другими словами несоответствие. Следовательно, формула S есть выводимой из безлюдного множества посылок либо теоремой разглядываемой теории.

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

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

К примеру, множества и являются подстановками сигнатуры .

Пускай U – формула, а q – подстановка сигнатуры s. Обозначим через формулу, взятую заменой всех вхождений на термы .

Определение. Подстановка q сигнатуры s именуется унификатором для множества формул сигнатуры s, в случае если . Множество формул сигнатуры s, именуется унифицируемым, в случае если для него существует унификатор сигнатуры s.

К примеру, множество формул сигнатуры унифицируемо, поскольку подстановка есть его унификатором.

Определение.Пускай и – подстановки сигнатуры s. Композицией подстановок q и l (обозначается q ° l) именуется подстановка, которая получается из множества вычеркиванием всех элементов , для которых , и всех элементов , для которых .

Пример. Пускай , . Тогда = , а так как и , то .

Определение.Унификатор t для множества формул сигнатуры s именуется самый общим унификатором (НОУ), в случае если для каждого унификатора q этого множества и сигнатуры существует подстановка l сигнатуры s такая, что .

Так для множества самый общим унификатором есть подстановка .

Определение. Пускай – предложения исчисления предикатов, такие что , , а атомарные формулы унифицируемы самый общим унификатором t. Правило вывода

именуется правилом резолюции исчисления предикатов.

Задание 2. Проверить G |- , где

G: , , , .

Ответ. Выпишем множество предложений G, OS, пронумеровав их.

1.

2.

3.

4.

5.

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

6. R (1, 5)

7. (2, 6)

8. R (6, 7)

9. (4, 8)

10. ? R (8, 9)

Следовательно, G |- .

Работа способа резолюций может иметь следующие варианты результатов:

1) на следующем шаге получено безлюдное предложение и, следовательно, формула S есть следствием G (теорема доказана);

2) в случае если во множестве предложений нет новых резольвируемых предложений, то теорема опровергнута;

3) множество предложений всегда пополняется новыми предложениями (зацикливание), что свидетельствует, что средств данной теории не хватает ни чтобы доказать теорему, ни чтобы её опровергнуть.

Представим метод работы способа резолюций на языке описания методов. Итог 1 – в случае если S выводимо из G, 0 – в другом случае. Обозначим M – множество предложений, C – множество предложений, полученное из G и OS. Функция choose делает выбор резольвируемых предложений, R – вычисляет резольвенту.

while yIC

begin choose ( )

if then return 0

R( )

end

return 1

Jenis


Также читать:

Понравилась статья? Поделиться с друзьями: