Алгоритм подпункта - PullRequest
Новая
       28

Алгоритм подпункта

0 голосов
/ 04 января 2019

Важной частью автоматического доказательства теорем является сокращение избыточности путем выяснения, когда одно предложение включает другое.

Интуитивно понятно, что предложение (логическая формула первого порядка в CNF) C включает в себя другое предложение D, когда оно хотя бы является общим. Конкретное определение состоит в том, что необходимо заменить переменные на термины, которые превращают C в подмножество D. (Не подмножество; это позволило бы предложению включать в себя его собственные факторы, что нарушило бы полноту некоторых из лучших исчислений насыщения такие как суперпозиция.)

Существуют методы индексации, которые значительно сокращают количество попыток включения, но даже в этом случае потребление может занимать много процессорного времени, поэтому важно его оптимизировать. Очевидно, в общем случае известно, что он NP-сложный, но все же возможно и необходимо, чтобы большинство частных случаев работало быстро.

Следующий псевдокод правильный, но неэффективный. (На практике отрицательные и положительные литералы должны обрабатываться отдельно, а затем возникают проблемы, такие как попытка уравнений, ориентированных в обе стороны, но здесь я просто рассматриваю основной алгоритм для сопоставления двух пакетов литералов.) 

def match_clauses(c, d, map):
    if c == {}:
        return true
    for ci in c:
        for di in d:
            if match_terms(ci, di, map):
                if match_clauses(c - ci, d - di, map):
                    return true
    return false

Почему это неэффективно? Рассмотрим два пункта p(x) | q(y) | r(42) и p(x) | q(y) | r(54). Приведенный выше алгоритм сначала будет успешно совпадать с p(x), затем успешно совпадать с q(y), затем уведомление r(42) не будет совпадать с r(54). Хорошо, но тогда он попробует это с другой стороны: сначала успешно сопоставить q(y), затем успешно сопоставить p(x), затем снова заметить, что r(42) не соответствует r(54). Если есть N литералов, которые действительно совпадают, потраченная впустую работа будет N факториальной, что в некоторых практических случаях наносит серьезный ущерб.

Я, без сомнения, мог бы найти лучший алгоритм, если бы уделил достаточно времени, но другие люди, должно быть, сделали это до меня, поэтому, кажется, стоит спросить: Какой алгоритм для этого известен лучше всего?

...