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

.

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

Снова пример со средой чудовища. Вернемся к решению задачи нахождения агентом золота в среде чудовища. Выше были сформулированы необходимые для решения задачи аксиомы. Перечислим их в несколько виде и перенумеруем, вводя дополнительно два атома: находится (Препятствие, , 0), находится (Препятствие, 0 ,). Здесь используется дополнительная константа Препятствие, соответствующая некоторому вымышленному объекту, который ограничивает передвижение объекта в ячейки, хотя бы одна координата которых равна нулю.

Предварительно напомним, что восприятие агента позволяет ему определять наличие зловония, сквозняка или блеска только в той ячейке, где он находится. Поэтому полное начальное состояние среды чудовища агенту неизвестно. Находясь в ячейке (1,1), он может воспользоваться только восприятиями в этой ячейке.

Формулы, определяющие начальные знания агента:

находится (Агент, 1,1)

ориентация (1,2)

Ø находится (Зловоние, 1,1)

Ø находится (Сквозняк, 1,1)

Ø находится (Яма, 1,1)

" находится (Препятствие, , 0)

" находится (Препятствие, 0, )

Для того чтобы выразить возможность восприятия агентом зловония, сквозняка или блеска в ячейках (1,2), (2,1), (3,1), соответственно введём следующие формулы:

находится (Агент, 1,2)É находится (Зловоние, 1, 2),

находится (Агент, 2,1)É находится (Сквозняк, 2, 1)Ù

Ù Ø находится (Зловоние, 1, 2),

находится (Агент, 2,3)É находится (Блеск, 2, 3),

находится (Агент, 1,2)É Ø находится (Сквозняк, 1,2),

находится (Агент, 2,2)É Ø находится (Зловоние 2,3),

находится (Агент, 2,2)É Ø находится (Сквозняк, 2,2).

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

находится (Зловоние, находится

(Чудовище, )Ù Ø находится (Чудовище, )Ù

Ù Ø находится (Чудовище, )Ù

Ù Ø находится (Чудовище, )Ù

Ù Ø находится (Чудовище, ),

находится (Сквозняк, находится

(Яма, )Ù Ø находится (Яма, )Ù

Ù Ø находится (Яма, )Ù

Ù Ø находится (Яма, )Ù

Ù Ø находится (Яма, ),

находится (Чудовище, находится

(Зловоние, )Ù Ø находится (Зловоние, )Ù

Ù Ø находится (Зловоние, )Ù

Ù Ø находится (Зловоние, )Ù

Ù Ø находится (Зловоние, ),

находится (Чудовище, )É находится

(Зловоние, )Ù находится (Зловоние, )Ù

Ù находится (Зловоние, )Ù

Ù находится (Зловоние, )Ù

Ù находится (Зловоние, ),

находится (Зловоние, находится

(Чудовище, )Ú находится (Чудовище, )Ú

Ú находится (Чудовище, )Ú

Ú находится (Чудовище, )Ú

Ú находится (Чудовище, ),

находится (Сквозняк, находится

(Яма, )Ú находится (Яма, )Ú

Ú находится (Яма, )Ú

Ú находится (Яма, )Ú

Ú находится (Яма, ).

Формулы, определяющие условия выполнения агентом действий:

находится (Агент, )Ù ориентация Ù

Ù Ø находится (Чудовище, )Ù

Ù Ø находится (Яма, )É

É перейти Ù находится (Агент, )Ù

Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù Ø находится (Чудовище, )Ù

Ù Ø находится (Яма, )É

É перейти Ù находится (Агент, )Ù

Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù Ø находится (Чудовище, )Ù

Ù Ø находится (Яма, )É

É перейти Ù находится (Агент, )Ù

Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù Ø находится (Чудовище, )Ù

Ù Ø находится (Яма, )É

É перейти Ù находится (Агент, )Ù

Ù ориентация ,

находится (Агент, )Ù

Ù находится (Блеск, ) É взять ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_направо ориентация Ù

Ù находится (Агент, )Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_направо ориентация Ù

Ù находится (Агент, )Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_направо Ù

Ù находится (Агент, )Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_направо Ù

Ù находится (Агент, )Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_налево Ù

Ù находится (Агент, )Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_налево Ù

Ù находится (Агент, )Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_налево Ù

Ù находится (Агент, )Ù ориентация ,

находится (Агент, )Ù ориентация Ù

Ù (находится (Чудовище, )Ú

Ú находится (Яма, )Ú

Ú находится (Препятствие, ))É

É повернуться_налево Ù

Ù находится (Агент, )Ù ориентация .

Формула цели:

взять .

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

Шаг 1.В соответствии с правилом исключения квантора общности и формулой (10.14) получаем

Ø находится (Зловоние, 1,1)É Ø находится

(Чудовище,1,1)ÙØ находится (Чудовище, 1,2)Ù

ÙØ находится (Чудовище, 2,1).

Шаг 2.В соответствии с формулами (10.3), (10.34) и правилом модус поненс получаем

Ø находится (Чудовище, 1,1)Ù

ÙØ находится (Чудовище,1,2)Ù

ÙØ находится (Чудовище, 2,1).

Шаг 3.В соответствии с формулой (10.35) и правилом исключения конъюнкта получаем

Ø находится (Чудовище, 1,1),

Ø находится (Чудовище,1,2),

Ø находится (Чудовище, 2,1).

Шаг 4.В соответствии с правилом исключения квантора общности и формулой (10.15) получаем

Ø находится (Сквозняк, 1,1)É

ÉØ находится (Яма,1,2)Ù

Ù Ø находится (Яма, 2,1).

Шаг 5.В соответствии с формулами (10.4), (10.39) и правилом модус поненс получаем

Ø находится (Яма, 1,2) Ø находится (Яма, 2,1).

Шаг 6.По (10.40) и правилу исключения конъюнкта получаем

Ø находится (Яма, 1,2),

Ø находится (Яма, 2,1).

Заметим, что так как ячеек хотя бы с одной нулевой координатой не существует, то соответствующие им предикаты не включены в формулы (10.39) и (10.40).

Шаг 7.В соответствии с формулами (10.1), (10.2), (10.37), (10.41) и правилом введения конъюнкции

находится (Агент, 1,1)Ù ориентация (1,2)Ù

Ù Ø находится (Чудовище, 1,2) Ù

Ù Ø находится (Яма, 1,2).

Шаг 8.В соответствии с формулой (10.21) и правилом исключения квантора общности получаем

находится (Агент, 1,1)Ù ориентация (1,2)Ù

Ù Ø находится (Чудовище, 1,2) Ù

Ù Ø находится (Яма, 1,2)É перейти (1,2) Ù

Ù находится (Агент, 1,2)Ù ориентация (1,3).

Шаг 9.В соответствии с формулами (10.43), (10.44) и правилом модус поненс получаем

перейти (1,2) Ù находится (Агент, 1,2)Ù

Ù ориентация (1,3).

Шаг 10.В соответствии с формулой (10.45) и правилом исключения конъюнкта получаем

перейти (1,2)

находится (Агент, 1,2)

ориентация (1,3).

Шаг 11.В соответствии с формулами (10.47), (10.8) и правилом модус поненс получаем

находится (Зловоние,1,2).

Шаг 12.В соответствии с формулами (10.47), (10.11) и правилом модус поненс получаем

Ø находится (Сквозняк,1,2).

Шаг 13.В соответствии с формулой (10.48) и правилом исключения квантора общности получаем

находится (Зловоние,1,2)É

É находится (Чудовище,1,1)Ú

Ú находится (Чудовище,1,2)Ú

Ú находится (Чудовище,1,3)Ú

Ú находится (Чудовище,2,2).

Шаг 14.В соответствии с формулами (10.49), (10,51) и правилом модус поненс получаем

находится (Чудовище,1,1)Ú

Ú находится (Чудовище,1,2)Ú

Ú находится (Чудовище,1,3)Ú

Ú находится (Чудовище,2,2).

Шаг 15.В соответствии с формулой (10.52) и правилом резолюции (согласно (10.36) истинен предикат Ø находится (Чудовище,1,1), а по (10.37) - истинен предикат Ø находится (Чудовище,1,2); следовательно, находится (Чудовище,1,1) и находится (Чудовище,1,2)ложны) получаем

находится (Чудовище,1,3)Ú

Ú находится (Чудовище,2,2).

Чудовище только одно и поэтому только один из предикатов в формуле (4.53) должен быть истинным. Определить, однако, какой из них истинен, агент не может. Поэтому попытаемся сформулировать действия, которые, находясь в ячейке (1,2), агент может совершать в предположении, что чудовище может быть в любой из двух ячеек (1,3) или (2,2).

Шаг 16.В соответствии с формулой (10.27) и правилом исключения квантора общности получаем

находится (Агент,1,2)Ù ориентация (1,3) Ù

Ú находится (Чудовище,1,3)É

É повернуться_направо (1,2)Ù

Ù находится (Агент,1,2)Ù ориентация (2,2).

Шаг 17.В соответствии с формулами (10.47), (10.48), (10.53) правилом введения конъюнкции получаем

находится (Агент,1,2)Ù ориентация (1,3) Ù

Ú находится (Чудовище,1,3).

Шаг 18.В соответствии с формулами (10.54), (10.55), (10.53) и правилом модус поненс получаем

повернуться (1,2) Ù находится (Агент,1,2)Ù

Ù ориентация (2,2).

Шаг 19.В соответствии с формулой (10.56), (10.55), (10.53) и правилом исключения конъюнкции получаем

повернуться (1,2),

находится (Агент,1,2),

ориентация (2,2).

Шаг 20.В соответствии с формулой (10.28) и правилом исключения квантора общности получаем

находится (Агент,1,2)Ù ориентация (2,2)Ù

Ù (находится (Чудовище, 2,2)Ú

Ú находится (Яма,2,2))É повернуться (1,2)Ù

Ù находится (Агент,1,2)Ù ориентация (1,1).

Шаг 21.В соответствии с формулой (10.53), (10.58), (10.59) и правилом введения конъюнкции получаем

находится (Агент,1,2)Ù ориентация (2,2)Ù

Ù (находится (Чудовище, 2,2).

Шаг 22.В соответствии с формулами (10.60), (10.61) и правилом модус поненс получаем

повернуться (1,2) Ù находится (Агент,1,2)Ù

Ù ориентация (1,1).

Шаг 23.В соответствии с формулой (10.62) и правилом исключения конъюнкта получаем

повернуться (1,2),

находится (Агент,1,2),

ориентация (1,1).

Шаг 24.В соответствии с формулой (10.20) и правилом исключения квантора общности получаем

находится (Агент,1,2) Ù ориентация (1,1) Ù

Ù Ø находится (Чудовище, 1,1) Ù

Ù Ø находится (Яма, 1,1) É

É перейти (1,1) Ù находится (Агент,1,1)Ù

Ù ориентация (1,0).

Шаг 25.В соответствии с формулами (10.5), (10.36), (10.64), (10.65) и правилом введения конъюнкции получаем

находится (Агент,1,2) Ù ориентация (1,1) Ù

Ù Ø находится (Чудовище, 1,1) Ù

Ù Ø находится (Яма, 1,1).

Шаг 26.В соответствии с формулами (10.67), (10.66) и правилом модус поненс получаем

перейти (1,1) Ù находится (Агент,1,1) Ù

ориентация (1,0).

Шаг 27.В соответствии с формулой (10.68) и правилом исключения конъюнкта получаем

перейти (1,1),

находится (Агент,1,1),

ориентация (1,0).

Таким образом, агент вернулся в ячейку (1,1), но ориентация его изменилась. Теперь он стоит лицом к несуществующей ячейке (1,0).

Шаг 28.В соответствии с формулой (10.6) и правилом исключения квантора общности получаем

находится (Препятствие,1,0).

Шаг 29.В соответствии с формулой (10.29) и правилом исключения квантора общности получаем

находится (Агент,1,0) Ù ориентация (1,0) Ù

Ù (находится (Препятствие, 1,0) Ú

Ú находится (Чудовище, 1,0) Ú

Ú находится (Яма, 1,0))É

É повернуться_налево (1,1) Ù.

Ù находится (Агент,1,1) Ù ориентация (2,1).

Шаг 30.В соответствии с формулами (10.70), (10.71), (10.72) и правилом введения конъюнкции получаем

находится (Агент,1,1) Ù ориентация (1,0) Ù

Ù (находится (Препятствие, 1,0).

Шаг 31.В соответствии с формулами (10.73), (10.74) и правилом модус поненс получаем

повернуться_налево (1,1) Ù

Ù находится (Агент,1,1) Ù ориентация (2,1).

Шаг 32.В соответствии с формулой (10.75) и правилом исключения конъюнкта получаем

повернуться_налево (1,1),

находится (Агент,1,1)

ориентация (2,1).

Шаг 33.В соответствии с формулой (10.23) и правилом исключения квантора общности получаем

находится (Агент,1,1) Ù ориентация (2,1) Ù

Ù Ø находится (Чудовище, 2,1) Ù

Ù Ø находится (Яма, 2,1)É перейти (2,1) Ù

Ù находится (Агент,2,1) Ù ориентация (3,1).

Шаг 34.В соответствии с формулами (10.77), (10.78), (10.38), (10.42) и правилом введения конъюнкции

находится (Агент,1,1) Ù ориентация (2,1) Ù

Ù Ø находится (Чудовище, 2,1) Ù

Ù Ø находится (Яма, 2,1).

Шаг 35.В соответствии с формулами (10.80), (10.79) и правилом модус поненс

перейти (2,1) Ù находится (Агент,2,1) Ù

Ù ориентация (3,1).

Шаг 36.В соответствии с формулой (10.81) и правилом исключения конъюнкта получаем

перейти (2,1),

находится (Агент,2,1),

ориентация (3,1).

Шаг 37.В соответствии с формулами (10.83), (10.9) и правилом модус поненс получаем

находится (Сквозняк 2,1).

Шаг 38.В соответствии с формулой (10.19) и правилом исключения квантора общности получаем

находится (Сквозняк 2,1)É находится (Яма, 2,2)Ú

Ú находится (Яма, 1,1) Ú находится (Яма, 3,1).

Шаг 39.В соответствии с формулами (10.85), (10.86) и правилом модус поненс получаем

находится (Яма,2,2) Ú находится (Яма, 1,1) Ú

Ú находится (Яма, 3,1).

Шаг 40.В соответствии с формулой (10.15) и правилом исключения квантора общности получаем

Ø находится (Сквозняк 1,2)É

É Ø находится (Яма,1,1) Ù

Ù Ø находится (Яма, 2,2) Ù

Ù Ø находится (Яма, 1,3).

Шаг 41.В соответствии с формулами (10.58), (10.11), (10.88) и правилами модус поненс и исключения конъюнкта получаем

Ø находится (Яма,1,1),

Ø находится (Яма, 2,2),

Ø находится (Яма, 1,3).

Шаг 42.В соответствии с формулами (10.87), (10.5), (10.90) и правилом резолюции получаем

находится (Яма,3,1).

Шаг 43.В соответствии с формулой (10.30) и правилом исключения квантора общности получаем

находится (Агент,2,1) Ù ориентация (3,1) Ù

Ù находится (Яма,3,1)É повернуться_налево (2,2) Ù

находится (Агент,2,1) Ù ориентация (2,2).

Шаг 44.В соответствии с формулами (10.92), (10.83), (10.84) и правилом введения конъюнкции общности получаем

находится (Яма,3,1) Ù

Ù находится (Агент,2,1) Ù ориентация (3,1).

Шаг 45.В соответствии с формулами (10.94), (10,93) и правилом модус поненс общности получаем

повернуться_налево (2,2) Ù

Ù находится (Агент,2,1) Ù ориентация (2,2).

Шаг 46.В соответствии с формулой (10.95) и правилом исключения конъюнкта получаем

повернуться_налево (2,2),

находится (Агент,2,1),

ориентация (2,2).

Шаг 47.В соответствии с формулой (10.21) и правилом исключения квантора общности получаем

находится (Агент,2,1) Ù ориентация (2,2) Ù

Ù Ø находится (Чудовище,2,2) Ù

Ù Ø находится (Яма,2,2)É перейти (2,2) Ù

Ù находится (Агент,2,2) Ù ориентация (2,3).

Шаг 48. В соответствии с формулами (10.9), (10.14), (10.97), (10.98), (10.90) и правилами исключения квантора общности, модус поненс и введения конъюнкции получаем

находится (Агент,2,1) Ù ориентация (2,2) Ù

Ù Ø находится (Чудовище,2,2) Ù

Ù Ø находится (Яма,2,2).

Заметим, что шаг 48 не является таким простым, как все остальныею Его детализацию предлагается выполнить самостоятельно.

Шаг 49. В соответствии с формулами (10.100), (10.99) правилом модус поненс получаем

перейти (2,2) Ù находится (Агент,2,2) Ù

Ù ориентация (2,3).

Шаг 50.В соответствии с формулой (10.101) и правилом исключения конъюнкта получаем

перейти (2,2),

находится (Агент,2,2),

ориентация (2,3).

Шаг 51.В соответствии с формулами (10.103), (10.12) и правилом модус поненс получаем

Ø находится (Зловоние,2,2).

Шаг 52.В соответствии с формулами (10.103), (10.13) и правилом модус поненс получаем

Ø находится (Сквозняк,2,2).

Шаг 53.В соответствии с формулой (10.14) и правилом исключения квантора общности получаем

Ø находится (Зловоние,2,2) É

É Ø находится (Чудовище,2,2) Ù

Ù Ø находится (Чудовище,2,1) Ù

Ù Ø находится (Чудовище,2,3) Ù

Ù Ø находится (Чудовище,1,2) Ù

Ù Ø находится (Чудовище,3,2).

Шаг 54.В соответствии с формулами (10.105), (10.107) и правилом модус поненс получаем

Ø находится (Чудовище,2,2) Ù

Ù Ø находится (Чудовище,2,1) Ù

Ù Ø находится (Чудовище,2,3) Ù

Ù Ø находится (Чудовище,1,2) Ù

Ù Ø находится (Чудовище,3,2).

Шаг 55.В соответствии с формулой (10.108) и правилом исключения конъюнкта получаем

Ø находится (Чудовище,2,2),

Ø находится (Чудовище,2,1),

Ø находится (Чудовище,2,3),

Ø находится (Чудовище,1,2),

Ø находится (Чудовище,3,2).

Шаг 56.В соответствии с формулой (10.15) и правилом исключения квантора общности получаем

Ø находится (Сквозняк,2,2) É

É Ø находится (Яма,2,2) Ù

Ù Ø находится (Яма,2,1) Ù

Ù Ø находится (Яма,2,3) Ù

Ù Ø находится (Яма,1,2) Ù

Ù Ø находится (Яма,3,2).

Шаг 57.В соответствии с формулой (10.114) и правилом исключения конъюнкта получаем

Ø находится (Яма,2,1),

Ø находится (Яма,2,3),

Ø находится (Яма,1,2),

Ø находится (Яма,3,2).

Шаг 58.В соответствии с формулой (10.21) и правилом исключения квантора общности получаем

находится (Агент, 2,2) Ù ориентация (2,3) Ù

Ù Ø находится (Чудовище,2,3) Ù

Ù Ø находится (Яма,2,3) É

É перейти (2,3) Ù находится (Агент, 2,3) Ù

Ù ориентация (2,4).

Шаг 59.В соответствии с формулами (10.103), (10.104), (10.11), (10.116) и правилом введения конъюнкции получаем

находится (Агент, 2,2) Ù ориентация (2,3) Ù

Ù Ø находится (Чудовище,2,3) Ù

Ù Ø находится (Яма,2,3).

Шаг 60.В соответствии с формулами (10.120), (10.119) и правилом модус поненс получаем

перейти (2,3) Ù находится (Агент, 2,3) Ù

Ù ориентация (2,4).

Шаг 61.В соответствии с формулой (10.121) и правилом исключения конъюнкта получаем

перейти (2,3)