Теорема графства Ковальского, доказывающая

Question

Я пытаюсь использовать алгоритм графа Ковальского для теоремы разрешения доказательство. Описание алгоритма в http://www.doc.ic.ac.uk/~rak/ умалчивает о том, что делать с большим количеством дублирующих предложений, которые он генерирует. Мне интересно, есть ли известная техника для общения с ними ?

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

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

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

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

Answer 1

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

Answer 2

Это в основном выглядит совершенно правдоподобным; некоторые Googling не представляют каких-либо очевидных реализаций. Я согласен, вы хотите посмотреть на равенство между представлениями, а не на идентичность.