Категоризация решетка представляет собой математическую структуру, используемую в теоретических основ автоматизированного доказательства теорем и других символических вычислений приложений.
Термин т 1 называется подводить слагаемое т 2, если подстановка σ такая, что σ применяется к т 1 урожайности т 2. В этом случае t 1 также называется более общим, чем t 2, а t 2 называется более конкретным, чем t 1 или экземпляром t 1.
Множество всех членов (первого порядка) данной сигнатуры можно сделать решеткой над отношением частичного порядка «. .. более конкретно, чем... » следующим образом:
Эта решетка называется решеткой включения. Два члена называются объединяемыми, если их пересечение отличается от Ω.
Присоединиться и операция встречается в этой решетке называется антиунификациями и унификация, соответственно. Переменная x и искусственный элемент Ω - это верхний и нижний элементы решетки соответственно. Каждый основной член, то есть каждый член без переменных, является атомом решетки. Решетка имеет бесконечные нисходящие цепи, например x, g ( x), g ( g ( x)), g ( g ( g ( x))),..., но не бесконечные восходящие.
Если f - двоичный функциональный символ, g - унарный функциональный символ, а x и y обозначают переменные, то термины f ( x, y), f ( g ( x), y), f ( g ( x), g ( y)), f ( x, x) и f ( g ( x), g ( x)) образуют минимальную немодулярную решетку N 5 (см. рис. 1); его внешний вид препятствует тому, чтобы решетка подчинения была модульной, а следовательно, и распределительной.
Совокупность сроков, унифицированных с данным термином, не обязательно должна быть закрыта в отношении соответствия; Рис. 2 показан контрпример.
Обозначая Gnd ( t) множество всех основных экземпляров терма t, выполняются следующие свойства:
Рис. 5. Дистрибутивная подрешетка линейных членов |
Рис. 4: M 3 построен из линейных членов |
Рис. 3: N 5 построен из линейных членов |
Набор линейных членов, то есть терминов без нескольких вхождений переменной, является подмножеством решетки включения и сам по себе является решеткой. Эта решетка также включает N 5 и минимальную недистрибутивную решетку M 3 в качестве подрешеток (см. Рис. 3 и рис. 4) и, следовательно, не является модулярной, не говоря уже о дистрибутивной.
Операция meet всегда дает тот же результат в решетке всех членов, что и в решетке линейных членов. Операция соединения в решетке всех членов всегда дает экземпляр соединения в решетке линейных членов; например, (основные) члены f ( a, a) и f ( b, b) имеют соединение f ( x, x) и f ( x, y) в решетке всех терминов и в решетке линейных членов, соответственно. Поскольку операции соединения в общем не согласуются, решетка линейных членов не является собственно подрешеткой решетки всех терминов.
Соединение и встреча двух собственных линейных членов, т. Е. Их анти-объединение и объединение, соответствует пересечению и объединению их множеств путей, соответственно. Следовательно, любая подрешетка решетки линейных термов, не содержащая Ω, изоморфна решетке множеств и, следовательно, дистрибутивна (см. Рис. 5).
По-видимому, решетка подчинения была впервые исследована Гордоном Д. Плоткиным в 1970 году.