Трудности процедуры поиска решения в среде чудовища

Вывод

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Шаг 7. В соответствии с формулами (4.1), (4.2), (4.37), (4.41) и правилом введения конъюнкции получаем

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

находится (Чудовище, 1, 3) повернуться_направо (1, 2)

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

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

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

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

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

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

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

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

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

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

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

находится (Агент, 1, 2) ориентация (2, 2) (находится (Чудовище, 2, 2) находится (Яма, 2, 2)) повернуться (1, 2) находится (Агент, 1, 2)

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

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

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

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

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

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

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

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

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

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

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

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

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

перейти (1,1) находится (Агент, 1,1) ориентация (1, 0). (4.66)

Шаг 25. В соответствии с формулами (4.5), (4.36), (4.64), (4.65) и правилом введения конъюнкции получаем

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

находится (Чудовище, 1, 1) находится (Яма, 1, 1). (4.67)

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

перейти (1, 1) находится (Агент, 1, 1) ориентация (1, 0). (4.68)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Шаг 34. В соответствии с формулами (4.77), (4.78), (4.38), (4.42) и правилом введения конъюнкции получаем

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Шаг 44. В соответствии с формулами (4.92), (4.83), (4.84) и правилом введения конъюнкции получаем

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

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

Шаг 45. В соответствии с формулами (4.94), (4.93) и правилом модус поненс получаем

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

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

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

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

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

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

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

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

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

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

Шаг 48. В соответствии с формулами (4.9), (4.14), (4.97), (4.98), (4.90) и правилами исключения квантора общности, модус поненс и введения конъюнкции получаем

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Шаг 59. В соответствии с формулами (4.103), (4.104), (4.111), (4.116) и правилом введения конъюнкции получаем

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

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

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

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

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

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

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

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

Шаг 62. В соответствии с формулами (4.123), (4.10) и правилом модус поненс получаем

находится (Блеск, 2, 3). (4.125)

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

находится (Агент, 2, 3) находится (Блеск, 2, 3) взять (2, 3). (4.126)

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

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

Шаг 65. В соответствии с формулами (4.127), (4.126) и правилом модус поненс получаем

взять (2, 3). (4.128)

Шаг 66. В соответствии с формулой (4.128) и правилом введения квантора существования получаем

взять (2, 3) (i, j) взять (i, j). (4.129)

Таким образом, была достигнута (выведена) цель (4.33).

Процедура поиска решения сравнительно простой задачи в среде чудовища потребовала 66 шагов. На каждом шаге применялось чаще всего какое-либо одно правило вывода. (Некоторые шаги, например, шаг 48 вывода формулы (4.100), были несколько укрупнены). Что можно заметить, анализируя эту процедуру?

Несмотря на простоту задачи, число шагов кажется несоразмерно большим (66 шагов).

Также кажется слишком большим количество новых истинных литералов, которые были выведены в процессе поиска решения (130 литералов).

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

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

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

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

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