Исчисление суперпозиции - это метод доказательства теорем, который делает парамодуляцию менее плодотворной за счет наложения упорядочивающего сокращения вместо применения каждого уравнения в обоих направлениях.
Для очень простого тестового случая рассмотрим следующие пункты (используяобозначения, где строчные буквы обозначают константы, а не переменные):
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
Это влечет за собой попытку ввода входных уравнений в направлении, разрешенном упорядочением редукции, затем переворачивание выходного уравнения, чтобы аналогично согласовать упорядочение редукции.Когда вы делаете это, это работает.
Это разрешено?Другими словами, является ли целью определения исчисления суперпозиции, что уравнения неупорядочены, поэтому каждое уравнение должно быть сгенерировано и использовано в любом порядке, соответствующем порядку редукции?