Доказательство теоремы графа Ковальского

Question

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

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

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

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

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

Answer 1

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

Answer 2

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