Где найти ресурсы / информацию о контрольном контроле в Прологе - PullRequest
Новая
       19

Где найти ресурсы / информацию о контрольном контроле в Прологе

0 голосов
/ 20 ноября 2018

В рамках задания меня попросили проверить правильность или неправильность доказательств естественного вывода с использованием Пролога.Пример текстового файла с именем «valid.txt», содержащего доказательство, выглядит следующим образом: 

[imp(p, q), p].
q.
[
[1, imp(p,q), premise],
[2, p, premise],
[3, q, impel(2,1)]
].```

Это будет входная информация для моей программы, которая должна ответить «да» или «истина» на правильное доказательство (что выше), и «нет» или «ложь» для неправильного доказательства.

Понятия не имею, с чего начать.Итак, , мой вопрос, есть ли какие-нибудь ресурсы, где я мог бы узнать о проверке / контроле доказательств в прологе .У меня есть небольшой опыт программирования на прологе, но я чувствую, что мне нужны конкретные инструкции о том, как создать программу, которая может проверять доказательства.Я искал учебники и сайты, но не смог найти ничего, что могло бы мне помочь.

В конце моя программа, вероятно, должна выглядеть примерно так: Проверка правильности логической последовательности, в которой есть предположения

Так как это мой первый раззадавая вопрос здесь я прошу прощения, если я что-то пропустил.

1 Ответ

0 голосов
/ 20 ноября 2018

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

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

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

«Справочник по практической логике и автоматическому рассуждению» ДжонХаррисон ( WorldCat ) ( Amazon ) ( Веб-страница )

Примечание: книга использует язык программирования OCaml, но реализуетподмножество Пролог .Также в книге используется язык, специфичный для предметной области, и реализован синтаксический анализатор .

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

Вам может понадобиться только то, что находится в prop.ml 

let rec eval fm v =
  match fm with
    False -> false
  | True -> true
  | Atom(x) -> v(x)
  | Not(p) -> not(eval p v)
  | And(p,q) -> (eval p v) & (eval q v)
  | Or(p,q) -> (eval p v) or (eval q v)
  | Imp(p,q) -> not(eval p v) or (eval q v)
  | Iff(p,q) -> (eval p v) = (eval q v);;

Пример запроса 

tautology <<p \/ q ==> q \/ (p <=> q)>>;;

Книга является более подробным введениемк исходному коду более функциональной версии HOL-Light , которая является более простой версией HOL .

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

...