anldp - онлайн у хмарі

ПРОГРАМА:

ІМ'Я

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

СИНТАКСИС

anldp [опції] вхідний файл > вихідний файл

ОПИС

На цій сторінці посібника коротко описано anldp команда

anldp є реалізацією процедури Девіса-Патнема для пропозиції
проблема задовільності. anldp розкриває процедуру, яку використовує mace2(1) визначити
задовільність. anldp може також приймати твердження в логіці першого порядку з рівністю та a
розмір домену 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