Если (а1  а2), то в.

Формула для вычисления коэффициента определенности общей посылки имеет вид:

КО (А₁  А₂) = max (КО (А₁), КО (А₂)),

2. Приведите структуру доказательств на основе резолюции.

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

.

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

Докажем, что если какая-либо интерпретация удовлетворяет исходным предложениям, то она удовлетворяет и резольвенте. Пусть какая-либо интерпретация I удовлетворяет исходным предложениям. Возможны два случая:

• интерпретация I удовлетворяет ;

• интерпретация I удовлетворяет .

В первом случае интерпретация I будет удовлетворять исходным предложениям, если она удовлетворяет R(z). Следовательно, в этом случае I удовлетворяет резольвенте. Во втором случае интерпретация I будет удовлетворять исходным предложениям, если она удовлетворяет P(x). Следовательно, и во втором случае I удовлетворяет резольвенте.

Если любая интерпретация, удовлетворяющая всем формулам (предложениям) множества Ф, удовлетворяет и формуле (предложению) F, т. е. F логически следует из Ф, то F называют следствием Ф. Совокупность правил, используемых при получении следствий – резольвент из заданных предложений, называют принципом резольвенции или принципом резолюции.

Принцип резолюции включает следующие два принципа:

- принцип силлогизма в исчислении высказываний, состоящий в том, что из и логически следует : ,т. е. пропозиционная форма является тавтологией;

- принцип отыскания частных случаев в исчислении предикатов, заключающийся в том, что формула F(t₁, … ,t_n), получающаяся из F(x_1...,x_n) при подстановке вместо x_i произвольных термов t_i является частным случаем F(x₁, … , x_n) и, следовательно .

Рассмотренный выше силлогизм («Все люди смертны», «Сократ – человек», «Сократ – смертен») можно, введя обозначения (Р – Сократ, Q – человек, R – смертен), представить в виде: .

Фактически принцип резолюции реализует цепочку (P  Q и Q R)  (  R), т. е. силлогизм и эквивалентен последовательному применению правил modus ponens и «специализация» к правилам P  Q и Q R. Действительно, из истинности P и P  Q следует истинность Q, а из истинности Q и QR следует истинность R, следовательно, истинно заключение   R.

Другими словами, помня, что

PQ= ,

из истинности и следует истинность .

В рассмотренном примере для простоты изложения сути принципа резолюции литералы P,Q,R не содержали переменных.

Напомним, что предложения представляют собой дизъюнкцию литералов. Каждый литерал это элементарный предикат в прямой или инверсной форме. Литерал L₁ будем называть дополнительным литералу L₂, если L₁ является отрицанием L₂, т. е. . Например и являются дополнительными литералами; а и не являются дополнительными.

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

В общем случае любую подстановку, используемую при применении принципа резолюции, можно представить в виде множества упорядоченных пар:

,

где пара означает, что всюду, где производится данная подстановка, переменная x_i заменяется термом t_i. Напомним, что подстановка осуществляется в соответствии с правилом «специализации», и после ее реализации получаются частные случаи.

Применяя, например, к литералу подстановки получим соответствующие им частные случаи исходного литерала:

.

Множество литералов унифицируемо, если существует такая подстановка P, что . Подстановка P в таком случае называется унификатором. Существует алгоритм, называемый алгоритмом унификации, который позволяет найти простейший унификатор для унифицируемого множества .

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

Если в паре родительских предложений после проведения унификации содержатся два дополнительных литерала L₁ и , то новое предложение, называемое резольвентой, формируется взятием дизъюнкции этих предложений с последующим исключением дополнительной пары и .

Билет №26