Cтраница 1
Множества поддержки ( support set) литеры L, принадлежащей WFSXP программы Р с пересматриваемыми литерами Rev ( каждое из них представляется как), получаются следующим образом. [1]
Множества удаления противоречия строятся по множествам поддержки противоречия. Они представляют собой минимальные множества таких литер, выбранных из множеств поддержки, что любое множество поддержки 1 содержит, по крайней мере, одину литеру из множества удаления противоречия. [2]
Подмножество Т множества 5 дизъюнктов называется множеством поддержки для S, если 5 - Т выполнимо. [3]
Легко доказать, что OL-резолюция влечет резолюцию с множеством поддержки. Иными словами, теорема 7.2 влечет теорему 6.2. Мы оставляем это читателю в качестве упражнения. [4]
Разумеется, имеется в виду полнота на тех множествах поддержки, на которых полна последняя стратегия. [5]
Тогда следующий вывод является выводом с Т в качестве множества поддержки. [6]
С, S1 и S2 с W в качестве множества поддержки для С, где S1 - список положительных единичных дизъюнктов, S2 - список отрицательных единичных дизъюнктов, W - некоторый список единичных дизъюнктов, С-неединичный дизъюнкт, N-натуральное число. [7]
Дизъюнкты ( 2), ( 4), ( 5) и ( 6) составляют множество поддержки. Следующий вывод является выводом с поддержкой. [8]
В дополнение к полноте V-резолюции в нее могут быть включены многие уточнения резолюции, введенные в главе 6, такие, как гиперрезолюция, множество поддержки и линейная резолюция. [9]
Если S - конечное противоречивое множество дизъюнктов и Т - подмножество S такое, что S - Т выполнимо, то имеется вывод с поддержкой пустого дизъюнкта П из множества S, в котором Т является множеством поддержки. [10]
Множества удаления противоречия строятся по множествам поддержки противоречия. Они представляют собой минимальные множества таких литер, выбранных из множеств поддержки, что любое множество поддержки 1 содержит, по крайней мере, одину литеру из множества удаления противоречия. [11]
Базу данных для известных фактов (1.1) иногда называют контекстной базой данных или долговременной памятью. Базу данных для новых фактов (1.2) иногда называют активной базой данных или множеством поддержки, или кратковременной памятью. [12]
Пусть Ck-дизъюнкт, выбранный на & - м шаге. TPU пытается породить какой-либо единичный дизъюнкт из Ck, Sx и S2 с множеством Wck поддержки для Ck. Если не было порождено ни одного единичного дизъюнкта, то TPU выбирает в Sa другой дизъюнкт и повторяет процесс. Если порождены какие-то единичные дизъюнкты, то TPU применяет критерий поглощения и, если возможно, критерий функциональной глубины. TPU сохраняет только те дизъюнкты, которые выдерживают эти критерии. Если найдено противоречие, программа останавливается; в противном случае она выбирает другой дизъюнкт из S3 и повторяет процесс. На каждом шаге процесса метод выбора дизъюнкта из S3 может оказаться критическим для эффективности программы. В TPU дизъюнкты из S3 выбираются последовательно. Когда S3 исчерпано, дизъюнкты выбираются снова в том же самом порядке. В программу включена стратегия поддержки. Каждый дизъюнкт из S3 имеет свое собственное множество поддержки. Различные дизъюнкты могут иметь различные множества поддержки. Они обновляются на каждом шаге. [13]
Необходимо отметить, что среди них имеются как стратегии, ориентированные на расширение ( expansion) множества дизъюнктов, получаемого путем резолюции, так и на сокращение ( contraction) этого множества путем поглощения. Упорядочение здесь понимается как наличие обоснованного порядка среди дизъюнктов, подлежащих процедуре поиска вывода. Стратегии, основанные на упорядочении, используют поиск только наилучшего ( с применением эвристик) и, как правило, не очень восприимчивы к разрешению целей. Однако использование в них семантических ( например, семантической резолюции) или поддерживающих ( резолюция множества поддержки) требований настраивает поиск на разрешение целей. [14]
Одно из преимуществ абстракции состоит в том, что она автоматически выбирает из входных дизъюнктов те, которые представляются относящимися к данной задаче. Таким образом, мы получаем преимущества стратегий поддержки. Однако поисковые стратегии, основанные на абстракции, оказываются совместимыми с другими полными резолюционными стратегиями, такими как лок-резолюция и Р1 - вывод. Следовательно, мы можем получить преимущества стратегии поддержки в резолю-ционных стратегиях, которые непосредственно не совместимы с ограничениями множества поддержки. Эта совместимость должна быть особенно полезна, когда имеется очень большое число входных дизъюнктов, из которых не все имеют отношение к данной задаче. [15]