Суперпозиционное исчисление - это метод доказательства теорем, который делает парамодуляцию менее плодотворной, вводя порядок уменьшения вместо применения каждого уравнения в обоих направлениях.
Для очень простого тестового примера рассмотрите следующие пункты (используя нотацию, где строчные буквы обозначают константы, а не переменные):
a=b
a=c
b!=c
Очевидно, из этих положений можно вывести противоречие.
В этом случае у нас есть только единичные предложения основных атомарных терминов, поэтому правила суперпозиции могут быть сформулированы в очень упрощенной форме.
Суперпозиция слева:
s=t, s!=v => t!=v
где s > t, t >= v в выбранном порядке уменьшения. (Полная версия суперпозиции должна иметь дело с предложениями как с мультимножествами литералов, с заменами переменных и с упорядочением сокращения, которое будет итоговым только в основных терминах, но это не относится к простому контрольному примеру, обсуждаемому здесь.)
Сходным образом,
Суперпозиция справа:
s=t, s=v => t=v
где s > t, t >= v в выбранном порядке уменьшения.
Предположим, мы используем порядок уменьшения a > b > c. Потом:
a=b, a=c => b=c
b=c, b!=c => false
Однако расчет должен быть полным для любого выбора порядка редукции. Предположим вместо этого c > b > a, тогда первый вывод выше запрещен.
Возможный альтернативный вывод:
c=a, c!=b => a=b
Также запрещено, поскольку b > a.
Альтернативная версия:
c=a, c!=b => b=a
Это влечет за собой проверку входных уравнений в направлении, разрешенном упорядочением сокращения, а затем перевертывание выходного уравнения, чтобы оно также соответствовало порядку сокращения. Когда вы это сделаете, это сработает.
Это разрешено? Другими словами, есть ли смысл определения исчисления суперпозиции в том, что уравнения неупорядочены, поэтому каждое уравнение должно быть как сгенерировано, так и использовано в любом порядке, соответствующем порядку сокращения?
