Пролог к ​​соединительной нормальной форме

Question

У меня есть этот код, который мне нужно перевести в CNF (это подготовка к экзамену, поэтому не домашняя работа!):

p,q
r :- q
false :- p , s 
s :- t
t

Вот что я сделал:

p ^ q ^ (r V ~q) ^ (~p V ~s) ^ (s V ~t) ^ t

=  r

Правильно ли мое рассуждение?

Здесь есть еще один вопрос:

Вы хотите запросить базу данных с помощью r. Какой пункт, вы должны добавить в свою базу данных?

Я вообще этого не понимаю. После упрощения база данных в основном р. Это правда, не правда ли?

Answer 1

Вопрос "Вы хотите запросить базу данных с помощью r. Какое предложение вы должны добавить в свою базу данных?" относится к так называемым опровержениям. В доказательстве опровержения никто не доказывает:

 Database |- Query

Вместо одного доказательства:

 Database, ~Query |- f

В классической логике два одинаковы. Таким образом, в вашем примере вам нужно показать, что p ^ q ^ (r V ~q) ^ (~p V ~s) ^ (s V ~t) ^ t ^ ~r приводит к противоречию.

до свидания