Здравствуйте. Ищу исполнителя.

Задача следующая:


Написать программу доказательства логических предложений в виде (предикат аргумент_1
… аргумент_N) на основе хорновских предложений.
- каждое хорновское предложение записывается в форме (p q1 … qN), которую следует
интерпретировать как “если предикаты q1 … qN истинны, то и предикат p истенен”;
- хорновское предложение, в котором условие пусто, а правило, отвечающее предикату
p, всегда истинно, является фактом и обозначается как (p);
- если заключение пусто или ложно (nil), то это всегда ложный предикат: (nil (p q1 …
qN));
- Пролог-программа строится из множества хорновских предложений:
(setq program ‘(<правила><факты>))

Пример правила:
((parent (? x)(? y))
(father (? x)(? y)))
Читается как: “x – родитель для y, если x – отец y”.

Пример факта:
(father “Пётр” “Иван”)
Читается как “Пётр – отец Ивана”.
- программа запускается путём передачи ей в качестве вопроса и для принятия решения
некоторого предиката, например,
(mother “Мария” “Иван”)
либо
(parent “Мария” (? x))
В первом случае ответом будет логическое значение, а во втором – связь (конкретизация) переменной заданного вопроса, при которой предикат будет истинен.

Интерпретатор работает в режиме командной строки. После запуска он выводит знак вопроса и ожидает ввода пользователем доказываемых предикатов.

Рекомендуемый язык для реализации – Лисп (любые диалекты).