Vp таких, что р входит в дизъюнкт с [c.484]
Два различных дизъюнкта могут иметь одинаковое описание. Пусть [c.484]
Семантические шаблоны используются как в подсистеме ИСХОДНЫЙ ОТОБРАЖАТЕЛЬ (где отображаются предикаты и переменные в формулировках теоремы), так и в подсистеме РАСШИРИТЕЛЬ, которая добавляет дополнительные предикаты, необходимые для доказательств теоремы ТА, и отыскивает множество аксиом, которые следует использовать для доказательства ТА- Описание дизъюнкта используется только в подсистеме РАСШИРИТЕЛЬ. [c.485]
Отображение дизъюнктов в этой аналогии представляет собой объединение дизъюнктов, входящих в GJ и j — >- 2. [c.503]
Когда множество дизъюнктов, которые удовлетворяют ограниченному описанию, содержит только один дизъюнкт, имеется гарантия, что он является образом дизъюнкта, который мы пытаемся отыскать (конечно, если аналогия Gf не содержит никаких ошибочных ассоциаций). Далее, если С пусто, имеется основание усомниться в правильности G , и нам следует [c.503]
Распознавание лемм зависит от свойств системы, решающей задачи. Например, в логике резолюций хорошим критерием было бы 1) основные единицы используются более чем дважды (или k раз) в доказательстве 2) единица, которая соединяется 3) дизъюнкт, который является потомком ( least des endant ) более чем для двух единиц. [c.477]
Логика резолюций есть правило вывода, а ее предложения (высказывания) называются дизъюнктами2) [1, 5]. Таким образом, система, отыскивающая аналогии и ориентированная на логику резолюций, должна иметь дело с дизъюнктами и их описаниями. Поскольку другая система, GPS, для описания своих состояний использует множества объектов, следует ожидать, что система поиска аналогий в этом случае должна была бы также иметь дело со (сложными) объектами и их свойствами. [c.478]
Пары георем ) Число предикатов в теоремах предикатов, отображенных исходным ОТОБРАЖАТЕЛЕМ Число аксиом в доказательстве Т Число найденных РАСШИРИТЕЛЕМ дизъюнктов частных аналогий, выработанных ZORBA-1 [c.480]
ZORBA-1 делает это так, что каждое приращение выделяет новые дизъюнкты, которые можно использовать в доказательстве ТА. Практически, если в результате расширения аналогии GJ мы не получаем нового дизъюнкта, это может послужить поводом считать, что аналогия G/ ошибочна. В следующих разделах порождающий алгоритм будет описан более подробно. [c.481]
G — одно-многозначное отображение между дизъюнктами. Каждый дизъюнкт, использованный в доказательстве 7, ассоциируется с одним или более дизъюнктов из информационной базы D, которые ZORBA-1 будет использовать при доказательстве теоремы ТА. [c.482]
В предшествующем разделе мы ссылались на последовательность аналогий Gb. .., G/,. За один шаг ZORBA-1 обычно не получает аналогию G . Она постепенно расширяет некоторую ограниченную аналогию в другую, которая охватывает несколько большее число переменных, предикатов или дизъюнктов. Этот процесс подробно описан в следующих разделах. Здесь же мы только определим несколько терминов, относящихся к этому процессу. Когда я говорю аналогия между теоремами Т и ТА , я имею в виду отображение, которое включает каждую переменную в формулировке теоремы Т и каждый предикат и дизъюнкт, употребленный в доказательстве Т. Это полное отображение получается как последний шаг в ряде последовательных отображений, содержащих ассоциации для некоторых предикатов и некоторых дизъюнктов. Я называю последовательные и неполные отображения частными аналогиями . [c.482]
Кроме того, ZORBA-1 может составлять описание des r [с] для любого дизъюнкта с в соответствии со следующими правилами, относящимися к предикатам дизъюнкта с [c.483]
Таким образом, аксиома Всякая абелева группа есть группа (например У (х, ) abelian [х, ] =Ф group [л , ]) выражается дизъюнктом [c.484]
Каждый элемент описания, например pos [group], есть свойство ( признак , характеристика ) описания. Каждое свойство соответствует одному предикату, так что число свойств дизъюнкта равно числу предикатов в нем. [c.484]
Описание дизъюнктов используется, чтобы получить характеристики аксиом, для которых мы ищем аналоги. В качестве таких аналогов ZORBA-1 выбирает дизъюнкты, описания которых близки к аналогам описаний 4) аксиом в известном множестве аксиом. Хотя в специальных контекстах ZORBA-1 действительно использует упорядочивающее отношение на множестве описаний для отыскания наилучшего дизъюнкта , обычно используется более простой подход. Мы будем говорить, что [c.484]
Ни один из дизъюнктов не удовлетворяет pos [interse tion]. Очевидно, что, если описание содержит только несколько [c.485]
Конструкция РАСШИРИТЕЛЯ основана на нескольких простых, тесно связанных между собой идеях. Я начну с их объяснения, затем опишу MAPDES R — операцию для отображения описаний дизъюнктов — и закончу обсуждением двух простых вариантов РАСШИРИТЕЛЯ. [c.499]
Предположим далее, что нам надо отыскать возможность расширения GI путем нахождения аналогии для с7. Маловероятно, что мы найдем дизъюнкт, который удовлетворяет этому описанию (Gi [d7]), поскольку он может быть выведен только из одной (редко употребляемой) теоремы, связывающей условия в коммутативных кольцах с групповой структурой. В любом случае он не должен быть аналогом по отношению к с7. Если бы мы просмотрели все дизъюнкты, которые включают в свое описание neg [ ommutative ring], мы, конечно, включили бы s и сд, ибо они по крайней мере включают B, дизъюнкт которой для нас желателен [c.500]
Таким образом, иногда нам нужно отыскать дизъюнкты, которые имеют описание с характерным свойством, например neg ( ommutative ring], которое включает только предикаты, входящие в частную аналогию G,-. С этой целью мы используем процесс, состоящий из четырех шагов [c.500]
Отыскать в базе данных дизъюнкты, удовлетворяющие ограниченному описанию Gj [des r (с)]. [c.500]
В отдельных случаях РАСШИРИТЕЛЬ может искать дизъюнкты, которые удовлетворяют полному описанию аналогий Gj [des r] или только ограниченному описанию G, [des r]. Резюмируя, можно сказать, что основой для РАСШИРИТЕЛЯ служат следующие четыре ключевых понятия [c.500]
Поиск дизъюнктов, удовлетворяющих аналогам описаний дизъюнктов в proof [Г]. [c.500]
Теперь можно записать один из вариантов операции MAPDES R, в котором в качестве аргументов используются два описания дизъюнктов и аналогия Of. [c.502]
В выбранной нами алгебраической информационной базе описание дизъюнкта обычно состоит из двух, трех или четырех свойств. РАСШИРИТЕЛЬ предполагает, что некоторые из предикатов в каждой паре дизъюнктов, прошедших через операцию MAPDES R, входят в аналогию GJ. Таким образом, ко времени, когда мы достигаем третьего шага алгоритма, мы чаще всего имеем описания длины один , которые тривиально отображаются согласно условию несоответствия или описанию длины два с различными свойствами, например pos и neg. Таким образом, шаг 36, который требует устранения неоднозначности на основании проверки предикатных типов, редко встречается в этой области (абстрактной алгебре). [c.502]
Таким образом, когда РАСШИРИТЕЛЬ пытается расширить аналогию GJ, он создает новые аналогии Gj+ь Gj+2 и т. д. для каждой пары дизъюнктов, которую он отображает, если эти дизъюнкты были выбраны на основе информации, содержащейся в аналогии GJ. Имеется, конечно, процедура, позволяющая выяснить, не входит ли ассоциация предикатов новой аналогии в некоторую ранее полученную аналогию, и таким образом препятствующая избыточности. В этом случае два соответствующих дизъюнкта добавляются к каждой имеющейся аналогии, для которой пары предикатов, выданные подпрограммой MAPDES R, представляют собой подмножество отображений дизъюнктов, включенных в эти аналогии. [c.503]
После того как я изложу еще одну идею, я смогу описать простой вариант подсистемы РАСШИРИТЕЛЯ. Когда РАСШИРИТЕЛЬ расширяет аналогию GJ, он осуществляет поиск некоторого дизъюнкта, аналогичного аксиоме h e SOME в большой базе данных. Теперь мы можем производить поиск среди множества дизъюнктов, которые удовлетворяют G , [des r [ h]], но столкнемся при этом с трудностями, которые были описаны ранее в статье. Поэтому мы производим поиск среди дизъюнктов, [c.503]
Дизъюнкта с, то G des rf ]] будет иметь только одно свойство и многие дизъюнкты могут ему удовлетворять. Если некоторая аналогия Gk(G Gk), стоящая в последовательности расширяющихся аналогий после Of включает другой предикат из с в дополнение к первому предикату, включенному в аналогию GJ, то Gifdes rf ]] будет иметь два свойства и этому описанию будет удовлетворять меньшее число дизъюнктов, чем опи сание Gj[des r[ ]]. Таким образом, поскольку последовательность аналогий растет, каждый дизъюнкт будет иметь все уменьшающееся число образов кандидатов, удовлетворяющих его ограниченному описанию. [c.504]
Для того чтобы отыскать дизъюнкты, удовлетворяющие аналогии ограниченного (краткого) описания, РАСШИРИТЕЛЬ использует оператор shortdes r (краткое описание) [GJ. SHORTDES R зависит от аналогии GJ в трех отношениях [c.504]