4. ВЫВОД В ЛОГИКЕ ПРЕДИКАТОВ

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

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

4.1. Исчисление предикатов

В главе 2 было определено понятие логического исчисления. Одним из таких исчйслений является классическое исчисление предикатов. Как и любое другое исчисление, оно построено на использовании: алфавита (совокупности используемых символов);

синтаксических правил построения формул в алфавите;

аксиом (общезначимых исходных формул);

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

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

К этому множеству аксиом, являющихся аналогом аксиом классического исчисления высказываний, добавляются две следующие аксиомы:

Общезначимость этих аксиом легко проверить с помощью таблиц истинности.

Множеством правил классического исчисления предикатов является модус поненс а, а в котором являются формулами логики предикатов первого порядка, и два правила введения кванторов:

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

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

При использовании классического исчисления предикатов для описания свойств какой-либо конкретной среды абстрактные предикатные символы

заменяют конкретными, называемыми также индивидуальными тредикатными символами. Кроме того, вводят факты, аксиомы и правила, не являющиеся аксиомами классического исчисления предикатов и зависящие от той среды, для которой осуществляется формализация постановки задачи. В результате получается некоторое новое логическое исчисление. Формулы этого исчисления по-прежнему строят по тем же правилам, показанным на рис. 3.1. С его помощью можно выводить формулы, которые нельзя получить в классическом исчислении высказываний. С практической точки зрения нас интересуют именно такие исчисления, учитывающие особенности конкретных сред. В дальнейшем ряд таких исчислений и будет рассмотрен. Чтобы отличать такие исчисления от классического исчисления логики предикатов первого порядка, назовем их неклассическими исчислениями. К их числу относятся также исчисления, которые строятся не на основе логики предикатов первого порядка. В настоящей главе продолжим изучение неклассических исчислений, построенных на основе логики предикатов первого порядка.

Пусть, среди аксиом в неклассическом исчислении для какой-либо среды имеется две аксиомы где — переменная; А, В — константы; — предикатные символы. Спрашивается, можно ли на основании этих аксиом, используя правило модус поненс , заключить, что формула истинна. Если принять то такое заключение можно было бы сделать, если бы среди исходных аксиом имелась аксиома а Ее у нас нет. Имеется только аксиома Эта аксиома гласит: «Для всех х имеет место истинность формулы а Когда речь идет о всех х формулы а то имеются в виду, естественно, только те х, областью значений которых являются заранее оговоренные константы, среди которых есть константа А хотя бы потому, что она встречается в предикате а формулы а т.е. в предикате, предикатный символ а которого совпадает с предикатным символом предиката в аксиоме Это означает, что предикат а истинен. Следовательно, можно воспользоваться правилом модус поненс И заключить, что формула истинна. Таким образом, чтобы воспользоваться правилом модус поненс

пришлось по аксиоме получить аксиому а Это равносильно использованию правила вывода, означающего, что при наличии, аксиомы вместо переменной х в предикат а можно подставить константу А (эта подстановка обозначается и в результате получить аксиому а Это правило называют правилом исключения квантора общности. Кроме этого правила могут потребоваться также правила исключения квантора существования, которые записывают в общем виде следующим образом:

исключения квантора общности

исключения квантора существования

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

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

4.1.1. Снова пример со средой чудовища

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

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

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

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

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

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

(см. скан)

(кликните для просмотра скана)

(кликните для просмотра скана)

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

4.1.2. Вывод

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Шаг 23. В соответствии с формулой (4.62) и    правилом

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.1.4. Обобщенное правило модус поненс

Обозначим некоторый атом, имеющий предикатный символ и множество вхождений переменных и констант 5. Тогда обобщенное правило модус поненс принимает вид

Смысл этого правила состоит в следующем. Формулы являются атомами и каждый из них имеет множество вхождений констант и переменных В формуле а представленной импликацией, являются атомами, каждый из которых имеет множество вхождений констант и переменных Если существуют подстановки такие, что а то будет истинным атом Напомним, что означает, что вместо аргументов 6 атома подставляются аргументы 0. При этом необходимо соблюдать следующие требования:

Вместо переменной в 5 можно подставлять переменную из 0. Такую подстановку называют переименованием переменной.

Вместо переменной в 5 можно подставлять константу из 0. Такую подстановку называют конкретизацией переменной.

Вместо переменной в 6 можно подставлять функцию из 0. Такую подстановку называют заменой переменной.

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

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

Формулы в постановке задачи не должны содержать кванторов существования.

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

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

Такие формулы называют хорновскими формулами.

Преобразование произвольных формул логики предикатов в хорновские формулы непростая задача, причем не любую формулу можно преобразовать к такому виду. В нашем примере со средой чудовища кванторов существования, не считая формулы цели, вообще нет, тем не менее, подобное преобразование всех формул невозможно. Например, это нельзя сделать для формул (4.18), (4.19). Рассмотрим, как выполняется указанное преобразование для формул (4.1) — (4.32). Для того чтобы можно было легко сопоставить эти формулы с их преобразованиями, будем последние нумеровать теми же числами, но со звездочкой, комментируя производимые преобразования (если в преобразованиях нет необходимости, то соответствующая формула переписывается без комментариев):

Выполняя преобразования на основе закона Ложь Ложь, получаем

Простым удалением квантора общности (если он есть) или на основе закона получаем следующие формулы:

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

Вторая формула в (4.9) может быть преобразована аналогично.

С помошью преобразования за), удаления квантора существования и правила исключения конъюнкта, получаем следующие формулы:

(кликните для просмотра скана)

(кликните для просмотра скана)

Подформулы системы формул (4.25) — (4.32) получаются аналогично, но их еще больше. Выпишем, как и в предыдущем случае, только по одной (первой) подформуле:

(см. скан)

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

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