Cтраница 1
Принцип резолюции в исчислении высказываний состоит в выборе двух дизъюнктов Dt и DJ, в один из которых входит литера L, а в другой - ее отрицание - L. Резольвентой называется новая формула R - Р / Q, получаемая из Dt Р V L и DJ - Q у 0) путем вычеркивания литер L и - L. Это соответствует применению правила модус поненс к рассматриваемым дизъюнктам. [1]
Принцип резолюции или вариации этого принципа используются во многих системах по автоматическому доказательству теорем или для нахождения доказательства или проведения вывода. Отметим только, что хотя принцип резолюции очень простой, его практическое применение во многом зависит от того, каким образом уменьшить пространство перебора, когда мы пытаемся провести сравнение. Мы также отметим, что принцип резолюции тесно связан с графическим сравнением. Фактически мы можем представить предложение ( или дизъюнкты) с помощью ( модифицированной) семантической сети и провести логические выводы путем применения принципа резолюции к семантической сети. [2]
Принцип резолюции обладает важным свойством - полнотой, которое устанавливается следующей теоремой. [3]
Принцип резолюции является более эффективной процедурой, нежели процедура вывода Эрбрана. Но и он страдает существенными недостатками, заключающимися в формировании всевозможных резольвент, большинство из которых оказывается ненужными. Многочисленные модификации принципа резолюции направлены на нахождение более эффективных стратегий поиска нужных дизъюнктов. Желающие могут обратиться к комментарию в конце книги, где перечислена литература, описывающая эти модификации. [4]
Принцип резолюции является научной базой разработки автоматизированных процедур вывода в ЭС при использовании МПЗ в виде исчисления высказываний и ИП. [5]
Принцип резолюции применим к двум дизъюнктам, один из которых содержит позитивную литеру, а второй - негативную с тем же предикатом и одинаковым количеством аргументов. Вычеркивая данную литеру, можно сформировать новый дизъюнкт, называемый резольвентой, который является логическим следствием исходных дизъюнктов. [6]
Фактически принцип резолюции распространяет общепринятое правило вывода modus ponens на дизъюнкты с произвольным числом литер. [7]
По существу принцип резолюции является расширением Modus Ponens на случай произвольных дизъюнктов с любым числом литер. Расширение состоит в том, что если любые два дизъюнкта С и С 2, имеют контрарную пару литер ( Р и - iP), то, вычеркивая ее, мы формируем новый дизъюнкт из оставшихся частей двух дизъюнктов. [8]
Рассмотрим применение принципа резолюции для решения следующей задачи. C V В и один факт - однолитерный дизъюнкт: УЗ. Необходимо доказать истинность высказывания А. [9]
При использовании принципа резолюции для логического вывода в ИП возникают следующие трудности: 1) приведение всех исходных логических формул ИП в клаузальную, или дизъюнктивную, форму с применением различного рода эквивалентных преобразований; 2) поиск контрарных пар атомов или простых предикатов. [10]
Существенный недостаток принципа резолюции заключается в формировании на каждом шаге вывода множества резольвент - новых дизъюнктов, большинство из которых оказываются лишними. В связи с этим предложены различные модификации принципа резолюции, использующие более эффективные стратегии поиска и различного рода ограничения на вид исходных дизъюнктов. [11]
В исчислении предикатов принцип резолюций усложняется. [12]
Именно на основе принципа резолюций построен один из наиболее распространенных языков логического программирования - Пролог. [13]
Машинно-ориентированная логика, основанная на принципе резолюции - Киберн сб ( нов. [14]
Арифметико-логическая машина, базирующаяся на принципе резолюций, может выполнить алгоритм, описанный набором хорновских дизъюнктов. Язык программирования Пролог пронизан этим принципом. Пролог вводится в разд. [15]