Р.У. Себеста - Основные копцепции языков программирования (2001) (1160794), страница 159
Текст из файла (страница 159)
Например, рассмотрим следующие выражения: Первое из этих высказываний означает, что для любого значения переменной Х, если Х вЂ” женшина, то Х вЂ” человек. Второе высказывание означает, что существует такое значение переменной Х, прн котором Мери является матерьюХ и Х вЂ” мужчина; другими словами, у Мери есть сын. Область видимости кванторов всеобщности и существования распространяется на атомарное высказывание, к которому они приписаны.
Эта область видимости может быть расширена с помощью скобок, как зто сделано в двух только что описанных составных высказываниях. Таким образом, кванторы всеобщности и существования имеют более высокий приоритет, чем любой другой оператор. 616 Глава 15. Языки логического программирования а агзЬ абаз Ь аиЬ аэЬ асЬ Ниже приведены примеры составных высказываний: Ъ'Х.(женшина(Х) э человек(Х)) Л Х.(мать(Мери, Х) л мужчина(Х)) а не а иЬ а или Ь а тождественно Ь а влечет Ь Ь влечет а 1$.2.2.
Дизъюнктивные формы Мы обсуждаем исчисление предикатов, поскольку оно является основой языков логического программирования. Как и в других языках, оптимальными являются простейшие формы логических языков, т.е. избыточность языка следует минимизировать.
Одна из проблем, связанных с исчислением преднкатов в том виде, как мы его до сих пор описывали, состоит в том, что существует слишком много способов формулирования высказываний, имеющих одинаковый смысл, т.е. возникает большая проблема избыточности. Для логиков этой проблемы не существует, но, если исчисление предикатов должно быть использовано в автоматической (компьютеризованной) системе, это становится серьезной проблемой. Чтобы упростить ситуацию, нужно иметь стандартную форму высказываниЯ. Дизъюнктивная форма (с)ацьа! )опп), представляющая собой относительно простую форму высказываний, является одной из таких стандартных форм. Без потери общности все высказывания могут быть выражены в дизъюнктивной форме.
Высказывание в дизъюнктивной форме имеет следующий синтаксис: В1 Н Вз Н ... Н Вр С й1 Г1 йз Г1 ... Г1 йн Здесь А, и В, — это термы. Смысл этой дизъюнктивной формы высказывания заключается в следующем: если все термы А, истинны, то по крайней мере один терм В истинен. Основное свойство днзъюнктивной формы высказываний состоит в следующем: не нужны кванторы существования; кванторы всеобщности присутствуют неявно при использовании переменных в атомарных высказываниях; не требуется никаких операторов, кроме конъюнкции и дизьюнкции. Кроме того, коньюнкцня и дизъюнкция должны появляться только в порядке, указанном в общей дизъюиктивной форме: дизъюнкция в левой части, а конъюнкция — в правой. Все высказывания в исчислении предикатов можно преобразовать в дизъюнктивную форму с помощью соответствующего алгоритма.
Нильсон ()ч!!эзоп (1971)) привел доказательство того, что это действительно можно сделать, и описал простой алгоритм, реализующий такое преобразование. Правая часть в днзъюнктивной форме высказывания называется антецедентом (апгеседеп!). Левая часть называется консеквентом (сопзеццеп(), поскольку она является следствием истинности антецедента. Рассмотрим следующие дизъюнктивные формы высказываний: любит(Боб, форель) С любит(Боб, рыба] Г1 рыба(форель) отец(Луис, Эл) н отец(Луис, Вайолет) с отец(Эл, Боб) Г1 мать(Вайолет, Боб) Г1 Лед(Луис, Боб) На русском языке первое высказывание означает, что если Боб любит рыбу и форель является рыбой, то Боб любит форель.
Второе высказывание означает. что если Эл— отец Боба, а Вайолет — мать Боба и Луис — дед Боба, то Луис — либо отец Эла, либо отец Вайолет. 15.3. Исчисление предикатов и доказательство теорем Исчисление преликатов дает метод для выражения совокупностей высказываний.
Использовать совокупности высказываний — значит определять, можно лн вывести из них 619 15.3. Исчисление предикптов и доказательство теорем какие-нибудь интересные или полезные факты. Это аналогично работе математиков, старающихся открыть новые теоремы, которые можно вывести из известных аксиом и теорем. На заре компьютерных наук (в 1950-х и в начале 1960-х годов) процессу автоматического доказательства теорем уделялось большое внимание.
Одним из самых крупных научных достижений в области автоматического доказательства теорем было открытие принципа резолюции (гезо!цбоп) Аланом Робинсоном (А!ап КоЬ!пзоп) из Сиракузского университета (Б!гасцзе Оп!уегз!(у). Резолюция (гезо!цйоп) — это правило логического вывода, позволяющее вычислять выводимые высказывания по заданным высказываниям, обеспечивая, таким образом, метод, имеющий потенциальные приложения в области автоматического доказательства теорем. Резолюция была изобретена для применения к высказываниям в дизъюнктивной форме. Концепция резолюции заключается в следующем: допустим, что нам даны два высказывания в следующих формах: ',ср: О с (?г Их смысл состоит в том, что Р, следует из Р, а Д, следует из Дь Предположим, что высказывание Р, тождественно высказыванию Дь так что мы можем переобозначить их через Т.
Перепишем два наших высказывания в следующем виде: Тс Р- (2; с Т Поскольку Т следует из Р,. а Д~ следует из Т, логически очевидно, что Д, следует из Р, Запишем это в виде следующего высказывания: О- с Рг Процесс вывода этого высказывания из исходных двух высказываний является резолюцией. Рассмотрим два высказывания: старше(Джоанна, Джек) с мать(Джоанна, Джек) мудрее(Джоанна, Джек) С старке(Джоанна, Джек) По этим высказываниям, используя резолюцию, можно построить новое высказывание: мудрее (Джоанна» Джек) с мать (Джоанна, Джек) Механизм этой резолюции прост: термы в левых частях этих двух высказываний объединяются вместе с помощью логической операции "И", образуя левую часть нового высказывания. Затем точно также формируется правая часть нового высказывания.
Далее, терм, появляющийся в обеих частях нового высказывания, удаляется из них. Этот процесс применим и тогда, когда высказывания содержат составные термы в одной или обеих частях. Левая часть нового выведенного высказывания вначале содержит все термы левых частей двух заданных высказываний. Новая правая часть конструируется аналогично.
Затем термы, появляющиеся в обеих частях нового высказывания, удаляются. Резолюция следующих высказываний отец(Боб, Джек) и мать(Боб, Джек) ~ родители(Боб, Джек) дед(Боб, Фред) с отец(Боб, Джек) гз отец(Джек, Фред) 620 Глава 15. Языки логического программировония приведет к такому выражению: мать(Боб, Лжек) н дед('Боб, Фред) л родители(Боб, Лжек) гз отец(Лжек, Фред) Это выражение содержит все.
кроме одного, атомарные высказывания из обоих заданных высказываний. Атомарное высказывание. позволявшее операцию отец (Боб, Лжек) в левой части первого и правой части второго высказывания, удалено. По-русски мы могли бы записать эти высказывания следующим образом: если: из того. что Боб — родитель Джека, следует что Боб — или отец. или мать Джека и: из того, что Боб — отец Джека и Джек — отец Фреда, слелует что Боб— дед Фреда, лго,"да если: Боб — ролитель Джека и Джек — отец Фреда, ео: либо Боб — мать Джека, либо Боб — дед Джека.
В действительности резолюция представляет собой более сложный процесс, чем показано в этом простом примере. В частности, наличие переменных в высказываниях требует выполнять в процессе резолюции поиск значений этих переменных, что приводит к процессу поиска соответствий. Этот процесс определения полезных значений переменных называется унификацией (вп)бсайоп), Временное присваиванне значений переменным с целью унификации называется конкретизацией ()пыапйайоп).
Обычно во время резолюции переменная конкретизируется неким значением, не полностью удовлетворяющим требуемому соответствию, затем следует отменить последнее действие (Ьасрцгас)г) и конкретизировать зту переменную новым значением. Мы будем изучать унификацию и бектрекинг (Ьаск)гаек)пй) более подробно в контексте языка Рго)оя. Крайне важное свойство резолюции — ее способность обнаруживать любое противоречие в заданной совокупности высказываний. Это свойство позволяет использовать резолюцию для доказательства теорем следующим образом: в терминах исчисления высказываний мы можем представизь себе доказательство теоремы как заданную совокупность соответствующих высказываний, в которых отрицание теоремы само по себе формулируется в виде новою высказывания.
Теорема отрицается, так что можно использовать резолюцию для доказательства теоремы, обнаружив противоречие. Это — доказательство от противного. Обычно исходные высказывания называются гипотезами (Ьуро(йезйез), а отрицание теоремы — целью (йоа)). Теоретически. это обоснованный и полезный процесс. Однако количество времени, требуемое для выполнения резолюции, может стать проблемой.
Несмотря на то что резолюция — конечный процесс. если совокупность высказываний конечна, время, необходимое для обнаружения противоречия в большой базе данных высказываний, может быть огромным. Доказательство теорем представляет собой основу логического программирования. Многое из того, что может быть вычислено, можно сформулировать в виде списка заданных фактов и отношений в качестве гипотез, а цель должна быть выведена из гипотез с помощью резолюции.
При использовании высказываний для резолюции используется только ограниченный вид дизъюнктных форм. которые еше более упрощают процесс резолюции. Специальные формы высказываний. называемые хорновскими днзъюнктами (Ноги с)ацзез), могут иметь либо единственное атомарное высказывание в левой части либо пустую левую 15.3. Исчисление предикатов и доказательство теорем 621 часть. (Хорновские дизъюнкты названы в честь Альфреда Хорна (А1(гег) Ноги), изучавшего дизъюнкгы такого вида (Ноги, 1951).) Левая часть дизъюнктивной формы высказываний иногда называется головой, и поэтому хорновские дизъюнкты с левой частью называются хорновскими дизъюнктами с головой. Хорновскне дизъюнкты с головой используются для формулирования таких отношений, как любит(Боб, форель) С любит(Боб, рыбу) Г~ рыба(форель) Хорновские дизъюнкты с пустой левой частью, часто используемые для формулирования фактов, называются хорновскими дизъюнктами без головы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
