Логические модели

M =, где: T счетное множество базовых символов (алфавит) П(T); P множество, называемое формулами П(P); A выделенное подмножество априори истинных формул (аксиом) П(А); B конечное множество отношений между формулами, называемое правилами вывода П(B).

( x)F(x) P = ( x)(F(x) P); ( x)F(x) P = ( x)(F(x) P). ( x)F(x) ( x)P(x) = ( x)(F(x) P(x)), ( x)F(x) ( x)P(x) = ( x)(F(x) P(x)). ( x)F(x) ( x)P(x) ( x)(F(x) P(x)), ( x)F(x) ( x)P(x) ( x)(F(x) P(x)). ( x)F(x) ( x)P(x) = ( x)F(x) ( y)P(y) = ( x)( y)(F(x) P(y)), ( x)F(x) ( x)P(x) = ( x)F(x) ( y)P(y) = ( x)( y)(F(x) P(y)) при условии, что переменная y не появляется в F(x).

Шаг 1. Исключение логических связок и с помощью известных правил. Шаг 2. Продвижение связки до атома с использованием законов де Моргана. В результате выполнения этого шага получается формула, у которой знаки могут стоять только перед атомами. Шаг 3. Переименование связных переменных. Шаг 4. Вынесение кванторов с помощью формул (*)

( y)( x)P(x,y) «Для всех y существует некоторый x (возможно зависящий от y), такой, что P(x,y)» ( y)P(f(y),y) ( x)( y)( z)F(x, y, z) - ( x)( z)F(x, f(x), z) ( x)( z)( y)F(x, y, z) - ( x)( z)F(x, f(x, z),z) ( x)P(x) становится P(A)

(x 1 x 2 ) {x 1,x 2 } Q(A, f(g(B)))-Q(x, y)

P 1 P 2 … P N и P 1 Q 2 … Q M P 1, P 1 Родительские предложения РезольвентыКомментарии P и P Q(т.е. P Q) QМодус поненс P Q и P Q Q Предложение Q Q «сворачивается» в Q. Эта резольвента называется слиянием. P Q и P QQ P Здесь две возможные резольвенты; в данном случае обе являются тавтологиями. P и P NILПустое предложение, является признаком противоречия P Q и Q R (т.е. P Q и Q R) P R (т.е. P R) Цепочка.

L(x) и L(A), где x – переменная, а A – константа {t/x} {t 1 /x 1 ; t 2 /x 2 ; …, t n /x n } Условия, допускающие подстановку, состоят в следующем: x i является переменной, а t i – термом (константа, переменная, функция), отличным от x i. для любой пары элементов из группы подстановок в правых частях символов «/» не содержатся одинаковые переменные.

S – группа подстановок {t 1 /x 1 ; t 2 /x 2 ;…,t n /x n } LS S – унификатор {L 1, L 2, …, L m } L 1 S = L 2 S =… L m S Множество {L(x), L(A)} – унифицируемо, при этом унификатором является подстановка {A/x} {L(x, y)}, L{z, f(x)} S = {x/z, f(x)/y} S' = {A/x; A/z; f(A)/y}, что все другие унификаторы являются подстановками, выражаемыми в виде S

Множество литералов Наиболее общие подстановочные частные случаи {P(x), P(A)}P(A) {P(f(x), y, g(y)), P(f((x), z, g(x))} P(f(x), x, g(x)) {P(f(x, g(A, y)),g(A, y)), P(f(x, z), z)} P(f(x, g(A, y)), g(A, y))

{L i } и {M i } {l i } - подмножество {L i } {m i } – подмножеством {M i } для объединения множеств {l i } и { m i } существует НОУ S

P(x, f(A)) P(x, f(y)) Q(y) P(z, f(A)) Q(z) Если {l i } = {P(x, f(A))} и {m i } = { P(z,f(A))}, получаем резольвенту P(z, f(y)) Q(z) Q(y), S = {z/x}. При {l i } = {P(x, f(A)), P(x, f(y)) и {m i } = P(z, f(A))} получаем резольвенту Q(A) Q(z), S = {z/x, A/y}.

S - ППФ {A 1, A 2, …, A n } W - ППФ, для которой требуется выяснить, является ли она теоремой (A 1 A 2 … A n W) C i = P i1 P i2 … P im Q = C 1 C 2 … C k. {P i1, P i2, …, P im }

1. Кто умеет читать, тот грамотный ( x)(Ч(x) Г(x)) 2. Дельфины не грамотны ( x)(Д(x) Г(x)) 3. Некоторые дельфины обладают интеллектом ( x)(Д(x) И(x)) 4. Некоторые из тех, кто обладает интеллектом, не умеет читать ( x)(И(x) Ч(x))

1. Ч(x) Г(x). 2. Д(y) Г(y). 3а. Д(А). 3б. И(А). 4. И(z) Ч(z). 5. Ч(A) резольвента 3б и Г(А) резольвента 5 и Д(А) резольвента 6 и 2. 8 NIL резольвента 7 и 3а.

конъюнктивная нормальная форма (conjunctive normal form CNF) полная фразовая форма (full clausal form) и фраза Хорна (Horn clause)

1. ¬(pvq)(-p^-q) Исходное выражение. 2. ¬¬(pvq)v(-p^-q) Исключение. 3. (pvq)v(-p^-q) Ввод - внутрь скобок. 4. (¬pv(pvq)) ^ (¬qv(pvq)) Занесение v внутрь скобок. 5. {{-p, р, q}, {¬q, р, q} } Отбрасывание ^ и v в конъюнктивной нормальной форме.

p,qp и p,qq p 1, …, p m q 1, …, q n, m=>0 и n=>0 p 1,..., р m < q 1,...q n х 1,..., х k, для всех x 1,..., х k p 1 или... или p m является истинным, если q 1 и... и q n являются истинными. n=0 для всех x 1,..., x k p 1 или... или р m является истинным m=0 для всех x 1,..., x k не имеет значения, что q 1 и... и q n являются истинными

р < q 1,...q n. р :- q 1,...,q n. «Для всех значений переменных в фразе p истинно, если истинны q 1 и... и q n », т.е. пара символов «:-» читается как «если», а запятые читаются как «и».