anldp - Интернет в облаке

ПРОГРАММА:

ИМЯ

anldp - реализация процедуры пропозициональной выполнимости Дэвиса-Патнэма

СИНТАКСИС

илдп [кредита] входной файл > выходной файл

ОПИСАНИЕ

Эта страница руководства кратко документирует илдп команда.

илдп является реализацией процедуры Дэвиса-Патнэма для пропозициональной
проблема выполнимости. илдп раскрывает процедуру, используемую mace2(1) определить
выполнимость. илдп может также принимать операторы в логике первого порядка с равенством и
размер домена n затем ищите модели размера n. Код поиска модели первого порядка
преобразует утверждения в набор пропозициональных предложений, так что первый порядок
у заявлений есть модель размера n тогда и только тогда, когда пропозициональные предложения
удовлетворительно. Затем пропозициональный набор передается коду Дэвиса-Патнэма; любой
найденные пропозициональные модели могут быть переведены на модели первого порядка
заявления. Программа поиска модели первого порядка принимает операторы только в сглаженном виде.
форма реляционного предложения без функциональных символов.

ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ

-s Выполните отнесение. (Принятие всегда выполняется во время предварительной обработки модуля.)

-p Распечатайте модели по мере их нахождения.

-m n Остановитесь, когда n-я модель найдена.

-t n Остановить после n секунд.

-k n Выделить не более n килобайты для хранения статей.

-x n Квазигрупповой эксперимент n.

-B файл
Резервное копирование назначений в файл.

-b n Резервные задания каждые n секунд.

-R файл
Восстановить задания из файла. Файл обычно содержит только последнюю строку
файл резервной копии. Остальные входные данные, в частности предложения, должны быть даны точно так же, как в
оригинальный поиск.

-n n Эта опция используется для поиска моделей первого порядка. Параметр n указывает на
размер домена, и его наличие указывает программе читать сглаженный
реляционные предложения ввода вместо пропозициональных предложений.

Используйте anldp в Интернете с помощью сервисов onworks.net