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

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

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

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

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

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

12.12.2008 21:07:58
2 ОТВЕТА

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

0
12.12.2008 21:56:27
РЕШЕНИЕ

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

1
2.02.2009 14:53:22