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

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

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

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

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

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

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


prolog proof
person wesslo    schedule 20.11.2018    source источник
comment
Обратите внимание, что запросы рекомендаций о внешних ресурсах здесь не рассматриваются. Более широкий сайт, такой как Quora, может вам помочь.   -  person Carcigenicate    schedule 20.11.2018
comment
Хорошо, спасибо за информацию, я сделаю это вместо этого.   -  person wesslo    schedule 20.11.2018

Ответы (1)


arrow_upward
0
arrow_downward

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

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

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

«Справочник по практической логике и автоматизированному мышлению». Автор Джон Харрисон (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.

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

person Guy Coder    schedule 20.11.2018