Студопедия — A®B; B®C; C 7 страница. Это правильная подстановка, т.к
Студопедия Главная Случайная страница Обратная связь

Разделы: Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

A®B; B®C; C 7 страница. Это правильная подстановка, т.к






Это правильная подстановка, т.к. x1 –свободная переменная.

 

2. x1òf(x2, t) $x3(P21(x1, x3)® P2 (x2))

$x3(P21(f(x2, t), x3)® P2 (x2)).

Это - правильная подстановка, т.к. x1 –свободная переменная.


3. x3òx2$x3(P21(x1, x3)® P2 (x2))

$x3(P21(x1, x2)® P2 (x2)).

Это - неправильная подстановка, т.к. x3 –связанная квантором $.

4. x2òx3$x3(P1(x1, x3)® P2 (x2))

$x3(P1(x1, x3)® P2 (x3)).

Это - неправильная подстановка, т.к. предикат P2 (x3) попадает в область действия квантора $.

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


"x F(x)

F(t)

 

и введения квантора существования

F(t)

$xF(x).

 

 

2.2.2.2 Правила введения и удаления кванторов

Наиболее распространенными правилами являются:

1) Введение квантора общности: “если F1(t)® F2(x) выводимая формула и F1(t) не содержит свободной переменной x, то F1(t)® "x(F2(x)) также выводима”, т.е.

(F1(t)® F2(x))

(F1(t)® "x(F2(x))).

2) Удаление квантора общности: "если "x(F(x)) выводимая формула, то вместо x можно выполнить подстановку терма t, свободного от x, и получить также выводимую формулу F (t), т.е.

"x(F(x))

. F (t).

3) Введение квантора существования: "если терм t вхо­дит в предикат F(t), то существует, по крайней мере одна предмет­ная переменная x, удовлетворяющая требованиям $x(F(x)) ”, т.е.

F(t)

$x(F(x)).

4) Смена квантора:

"x(F(x)) $x(F(x))

ù$x(ùF(x)); ù"x(ùF(x)).

5) Перенос квантора, если терм t не содержит переменной x:

a) Âx(F1(x))Ú F2(t)

Âx(F1(x)Ú F2(t));

b) Âx(F1(x))&F2(t)

Âx(F1(x)& F2(t);

c) F1(t)® Âx(F2(x))

Âx(F1(t)®F2(x));

d) "x(P(x))®F(t)

$x(P(x)®F(t));

 

e) $x(P(x))®F(t)

"x(P(x)®F(t)).

6) Введение новой переменной:

a) "x(F1(x))Ú"x(F2(x))

"y"x(F1(y)Ú F2(x));

b) $x(F1(x))&$x(F2(x))

$y$x(F1(y)Ú F2(x)).

 

 

2.2.2.3 Правила заключения

Существует два основных правила определения истинности заключения:

а) если F1 и (F1®F2) выводимые фор­мулы, то F2 также выводима. Это - правило modus ponens (m.p).

F1; (F1®F2)

F2.

b) если ùF2 и (F1®F2) выводимые формулы, то ùF1 также. выводима. Это - правило modus tollens (m.t).

ù F2; (F1®F2)

ùF1.

 

Эти правила определяют схему вывода и позволяют использовать правила подстановки, введения и удаления кванторов и делать вывод об истинности заключения.

 

 

2.2.3 Метод дедуктивного вывода

В логике предикатов вывод определяется так же, как в исчислении высказываний. Все правила вывода логики высказываний включены в множество правил логики предикатов.

Пример: “Таможенные чиновники обыскивают каждого, кто въезжает в страну, кроме высокопоставленных лиц. Если некоторые люди способствуют провозу наркотиков, то на внутреннем рынке есть наркотик. Никто из высокопоставленных лиц не способствовает провозу наркотиков. Следовательно, некоторые из таможников способствуют провозу наркотиков?”

Пусть P1(x):=”x - таможенный чиновник”, P2(x,y):=”x обыскивает y”, P3(y):=”y въезжает в страну”, P4(y):=”y – высокопоставленное лицо”, P5(y):=”y способствует провозу наркотиков”.

"y(P3(y)&ùP4(y)®"x(P1(x)&P2(x,y)));

$y(P3(y)&P5(y));

"y(P3(y)&P4(y)®ùP5(y));

$x(P1(x)&P5(x)).

1) F1= $y(P3(y)&P5(y)) - посылка;

2) F2=P3(a)&P5(a) - заключение по формуле F1 и правилу удаления квантора существования;

3) F3= P3(a) - заключение по формуле F2 и правилу удаления логической связки конъюнкции;

4) F4= P5(a) - заключение по формуле F2 и правилу удаления логической связки конъюнкции;

5) F5="y(P3(y)&P4(y)®ùP5(y)) посылка;

6) F6= P3(t)&P4(t)®ùP5(t) - заключение по формуле F5 и правилу удаления квантора общности;

7) F7=ùP3(t)ÚùP4(t)ÚùP5(t) - заключение по формуле F6 и ее эквивалентным преобразованиям;

8) F8=ùP4(a) - заключение по формуле F7 при t=a для ùP3(a)=л и ùP5(a)=л;

9) F9="y(P3(y)&ùP4(y)®"x(P1(x)&P2(x,y))) - посылка;

10) F10="y"x (P3(y)&ùP4(y)® (P1(x)&P2(x,y))) - заключение по формуле F9 и правилу приведения к ПНФ;

11) F11=P3(a)&ùP4(a)®P1(t)&P2(t,a) - заключение по формуле F10 и правилу удаления квантора общности;

12) F12= P3(a)&ùP4(a) - заключение по формулам F3 и F8 и правилу введения логической связки конъюнкции исчисления высказываний;

13) F13=(P1(t)&P2(t,a)) - заключение по формулам F11 и F12 и правилу modus ponens;

14) F14= P1(t) -заключение по формуле F13 и правилу удаления логической связки конъюнкции исчисления высказываний;

15) F15=P5(a)=P5(t) -заключение по формуле F4 и замене предметной постоянной термом;

16) F16= P1(t) &P5(t) -заключение по формулам F14 и А15 и правилу введения логической связки конъюнкция исчисления высказываний;

17) F17=$x(P1(x)&P5(x)) -заключение по формуле F16 и правилу введения квантора существования. Так доказана истинность формулы $x(P1(x)&P5(x)).

 


P1(t)
ùP4(a)
t=a

P3(a)&ùP4(a)

a=t
P5(t)
P1(t) &P5(t)

$x(P1(x)&P5(x))

 

 

Рис. 11. Граф вывода заключения

 

Пример: Доказать истинность заключения

"x(P1(x)®(ù P2(x))); "x(P3(x)®P1(x))

"x(P3(x)®(ù P2(x))).

1) F1="x(P1(x)®(ù P2(x))) - посылка;

2) F2="x(P3 (x)®P1 (x)) -посылка;

3) F3=(P1 (t)®(ù P2 (t))) - заключение по формуле F1 и правилу 2) удаления квантора общности;

4) F4= P3 (t)® P1 (t) - заключение по формуле F2 и правилу 2) удаления квантора общности;

5) F5= (P3 (t)®(ù P2 (t))) - заключение по формулам F3, F4 и закону силогизма исчисления высказываний (см 1.2.3.2 правило 11);

6) F6="x(P3(x)®(ùP2(x))) - заключение по формуле F5 и правилу 1 введения квантора общности.

Так доказана истинность формулы "x(P3(x)®(ùP2(x))).

На рис. 12 приведен граф, иллюстрирующий процесс дедуктивного вывода.

       
   

 

 


(P3 (t)®(ù P2 (t)))


 

"x(P3(x)®(ùP2(x)))

 


Рис. 12. Граф вывода заключения

Пример: Доказать истинность заключения

"x($y(P21.(x; y)&P2(y))®$y((P3(y)& P24.(x; y))); ù$x(P3(x))

ù$x(P3(x))®"x"y(P21.(x; y)®(ùP2(y))).

 

1) F1="x($ y(P21.(x; y)&P2(y))®$y((P3(y)& P24.(x; y))) - посылка;

2) F2=ù $x(P3(x)) -посылка;

3) F3="x(ùP3(x)) - заключение no формуле F2 и правилу 5) смены кванторов (закон де Моргана);

4) F4=ùP3 (t) - заключение по формуле F3 и правилу 2) удаления квантора общности;

5) F5=ùP3(t)ÚùP24.(x;t) - заключение по формуле F4 и правилу 4) исчисления высказываний;

6) F6="y(ùP3(y)Ú(ùP24 (x; y))) - заключение по формуле F5 и правилу 1) введения квантора общности;

7) F7=ù$y(P3(y)&P24 (x; y)) - заключение по формуле F6 и правилу смены кванторов (закон де Моргана);

8) F8=$y(P21.(t; y)&P2(y)®$y(P3(y)&P24.(t; y)) - заключение по формуле F1 и правилу 2) удаления квантора общности;

9) F9=ù $y(P21.(t; y)&P2(y)) - заключение пo формулам F7 и F8при условии t=x и правилу modus tollens;

10) F10="y(ù P21.(t; y)ÚùP2(y)) - заключение по формуле F9 и правилу смены кванторов (закон де Моргана);

11) F11="y(P21. (t; y)®ù (P2 (y)) - заключение пo формуле F10 и эквивалентным преобразованиям алгебры предикатов;

12) F12="x"y(P21. (x; y)®ù (P2 (y)) - заключение по формуле F11 и правилу 1) введения квантора общности;

13) ù$x(P3(x))®"x"y(P21.(x; y)®(ù P2(y))) – заключение по формулам F2 и F12 и правилу modus ponens. Что и требовалось доказать.

На рис. 13 приведен граф вывода этой задачи.


 

 

 


рис. 13 Граф вывода заключения

 

Пример. Доказать истинность заключения

$x(P1(x)&"y(P2(y)®P24.(x; y))); "x(P1(x)®"y(P3(y)®ùP24.(x; y)))

"x(P2(x)®ùP3(x)).

 

1) F1=$x(P1(x)&"y(P2(y)®P24.(x; y))) - посылка;

2) F2="x(P1(x)®"y(P3(y)®ùP24 (x; y))) - посылка;

3) F3=P1(а)&"y(P2(y)®P24.(a; y))-заключение по формуле F1, правилу формирования ССФ;

4) F4=P1(a)- заключение по формуле F3 и правилу удаления конъюнкции исчисления высказываний

5) F5="y(P2(y)® P24.(a; y)) - заключение пo формуле F3 и правилу удаления конъюнкции исчисления высказываний;

6) F6=P2(t)® P24.(a; t) - заключение по формуле F5 и правилу 2) удаления квантора общности;

7) F7=P1(t)®"y(P3(y)®ùP24 (t; y))- заключение по формуле F2 и правилу 2) удаления квантора общности;

8) F8="y(P3(y)®ù P24 (a; y)) - заключение по формулам F3 и F7 при t=a и правилу modus ponens;

9) F9=P3(t)®ùP24.(a; t) - заключение по формуле F8 и правилу 2) удаления квантора общности;

10) F10=P24.(a; t)®ùP3(t) - заключение по формуле F9 и закону контрапозиции (правило 8) исчисления высказываний);

11) F11=P2(t)®ùP3(t) - заключение по формулам F6 и F10 и закону силлогизма (правило 11) исчисления высказываний);

12) F12="x(P2 (x)®ùP3(x)) - заключение по формуле F11 и правилу 1) введения квантора "x. Что требовалось доказать.

На рис. 14 приведен граф вывода этой задачи.


 

 

       
   

 


x=a

 

 


Рис. 14. Граф вывода заключения

 

 

2.2.4 Принцип резолюции

Если матрица формулы в результате приведения к виду ПНФ не будет содержать свободных переменных и сколемовских функций, то для вывода заключения полностью пpuменим алгоритм принципа резолюции, рассмотренный в исчислении высказываний. Этот алгоритм основывается на том, что если две формулы состоящие из дизъюнкции атомов (в дальнейшем такие формулы будем называть дизъюнктами) связаны конъюнкцией, и в них имеются два одинаковых или приводимых к одинаковым (унифицируемых) атома с разными знаками, то из них можно получить третий дизъюнкт, который будет логическим следствием первых двух, и в нем будут исключены эти два атома. Однако, если в результате приведения к виду ССФ аргументы атомов содержат сколемовские функции, то для поиска контрарных атомов необходимо выполнить подстановки термов вместо предметных переменных и получить новые формулы дизъюнктов, которые допускают их унификацию при формировании контрарных пар. Множество подстановок нужно формировать последовательно, просматривая каждый раз только одну предметную переменную.

Например, если даны два дизъюнкта (P1(x)ÚùP2(x)) и (ùP1(f(x))ÚP3(y)), то для получения контрарной пары атомов возможна подстановка

xòf(х)(P1(x)ÚùP2(x))=(P1(f(x))ÚùP2(f(x))) и

xòf(х)(ùP1(f(x))ÚP3(y))= (ùP1(f(x))ÚP3(y)).

В результате склеивания этих дизъюнктов может быть получена резольвента: (P1(f(x))ÚùP2(f(x)))Ú(ùP1(f(x))ÚP3(y))= (ùP2(f(x))Ú P3(y)).

Если пара дизъюнктов имеет вид (P1(f1(x))ÚùP2(x)) и (ùP1(f2(x))ÚP3(y)), то никакая подстановка не позволит сформировать резольвенту.

 

Пример: Даны две формулы P3(a;x;f(q(y))) и ùP3(z;f(z);f(u)).

Выполнить унификацию контрарных атомов.

1) zòa ùP3(z;f(z);f(u))=ùP3(a;f(a);f(u));

2) xòf(a) P3(a;x;f(q(y)))=P3(a;f(a);f(q(y)));

3) uòq(y) ùP3(a;f(a);f(u))=ùP3(a;f(a);f(q(y))).

В результате получены два контрарных атома: P3(a;f(a);f(q(y))) и ùP3(a;f(a);f(q(y))). Если в эти формулы атомов вместо предметной переменной y сделать подстановку предметной постояннойb, т.е.

yòbP3(a;f(a);f(q(y)))=P3(a;f(a);f(q(b))) и

yòbùP3(a;f(a);f(q(y)))= P3(a;f(a);f(q(b))),

то получим два контрарных высказывания.

Пример. Даны две формулы P3(x;a;f(q(a))) и ùP3(z;y;f(u)).

Выполнить унификацию контрарных формул.

1) xòbP3(x;a;f(q(a)))=P3(b;a;f(q(a)));

2) yòaù P3(z;y;f(u))=ùP3(z;a;f(u));

3) yòaùP3(z;a;f(u))=ùP3(b;a;f(u));

4) uòq(a)ùP3(b;a;f(u))=ùP3(b;a;f(q(a))).

В результате получены две контрарных формулы: P3(b;a;f(q(a))) и ùP3(b;a;f(q(a))).

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

Линейным выводом из множества дизъюнктов K называется последовательность дизъюнктов D1, D2,...Dn, где каждый член DiÎK, а каждый Di+1 является резольвентой центрального дизъюнкта (или предшествующей резольвенты) и бокового дизъюнкта из множества K.

Упорядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом P j старше атома P i в упорядоченном дизъюнкте тогда и только тогда, когда j > i. Например, в упорядоченном дизъюнкте (P1ÚP2ÚP3ÚP4) младшим считается атом P1, а старшим - P4. При наличии в упорядоченном дизюънкте двух одинаковых атомов, по закону идемпотенции, следует удалить старший атом, сохранив на прежнем месте младший.

Другим усилением принципа резолюции является использование информации о резольвируемых атомах. Обычно при выполнении процедуры унификации происходит удаление резольвируемых атомов. Од­нако они несут полезную информацию. Поэтому вмес­то удаления резольвируемых атомов при унификации предлагается удалять только старший атом, а младший - сохранить в резольвенте, выделив какой-либо рамкой. Если за обрамленным атомом в резольвенте не следует никакой другой атом, то обрамленный атом удалить. Если за обрамленным атомом резольвенты следует какой-либо необрамленный атом, то его следует оставить для последующего исследования. И наконец, если последний необрамленный атом резольвенты унифицируется с отрицанием атома боковой ветви, то его следует обрамить и удалить вместе с литерой боковой ветви. Используя резольвенты на последующих этапах, можно получить обрамленными все атомы последней резольвенты, т.е.получить пустой дизъюнкт.

Пример: Суждение “Преподаватели принимали зачеты у всех студентов, не являющихся отличниками. Некоторые аспиранты и студенты сдавали зачеты только аспирантам. Ни один из аспирантов не был отличником. Следавательно, некоторые преподаватели были аспирантами.” [1] Пусть P1(x):=”x – отличник”, P2(x):=”x – аспирант”, P3(x):=”x –студент”, P24 (x; y):=”x сдает зачет y”, P5(x):=”x – преподаватель”. Формулы этого суждение имеют вид:


 

"x(P3(x)&ùP1 (x)®$y(P5(y)&P24 (x; y))); $x(P2(x)&P3(x)&"y(P24 (x; y)®P2 (y)));

"x(P2(x)®ùP1(x)).

$x(P5(x)&P2(x)).

· Преобразовать посылки и отрицание заключения в ССФ:

1) F1="x(P3(x)&ùP1 (x)®$y(P5(y)&P24 (x; y)))=

"x$y(P3(x)&ùP1 (x)®(P5(y)&P24 (x; y)))=

"x(P3(x)&ùP1 (x)®(P5(f(x))&P24 (x; f(x)))).

M1=(P3(x)&ùP1 (x)®P5(f(x))&P24 (x; f(x)))=

ù(P3(x)&ùP1 (x))Ú P5(f(x))&P24 (x; f(x)) =

(ùP3(x)ÚP1 (x)Ú P5 (f(x))&P24 (x; f(x))=

(ùP3(x)ÚP1 (x)Ú P5(f(x)))&(ùP3(x)ÚP1 (x)Ú P24 (x; f(x))).

2) F2=$x(P2(x)&P3(x)&"y(P24 (x; y)®P2 (y)))=

$x"y(P2(x)&P3(x)&(P24 (x; y)®P2 (y)))=

"y(P2(a)&P3(a)&(P24 (a; y)®P2 (y))).

M2=(P2(a)&P3(a)&(P24 (a; y)®P2 (y)))=

P2(a)&P3(a)&(ùP24 (a; y)ÚP2 (y))).

3) F3="x(P2(x)®ùP1(x)).

M3=(P2(x)®ùP1(x))= (ùP2(x)ÚùP1(x)).

4) F4=ù$x(P5(x)&P2(x))= "x(ù (P5(x)&P2(x))).

M4=(ù (P5(x)&P2(x)))= (ùP5(x)Úù P2(x))).







Дата добавления: 2015-09-15; просмотров: 341. Нарушение авторских прав; Мы поможем в написании вашей работы!



Композиция из абстрактных геометрических фигур Данная композиция состоит из линий, штриховки, абстрактных геометрических форм...

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

ТЕОРЕТИЧЕСКАЯ МЕХАНИКА Статика является частью теоретической механики, изучающей условия, при ко­торых тело находится под действием заданной системы сил...

Теория усилителей. Схема Основная масса современных аналоговых и аналого-цифровых электронных устройств выполняется на специализированных микросхемах...

ТЕОРИЯ ЗАЩИТНЫХ МЕХАНИЗМОВ ЛИЧНОСТИ В современной психологической литературе встречаются различные термины, касающиеся феноменов защиты...

Этические проблемы проведения экспериментов на человеке и животных В настоящее время четко определены новые подходы и требования к биомедицинским исследованиям...

Классификация потерь населения в очагах поражения в военное время Ядерное, химическое и бактериологическое (биологическое) оружие является оружием массового поражения...

Примеры задач для самостоятельного решения. 1.Спрос и предложение на обеды в студенческой столовой описываются уравнениями: QD = 2400 – 100P; QS = 1000 + 250P   1.Спрос и предложение на обеды в студенческой столовой описываются уравнениями: QD = 2400 – 100P; QS = 1000 + 250P...

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

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

Studopedia.info - Студопедия - 2014-2024 год . (0.01 сек.) русская версия | украинская версия