3

このコードを 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 を使用してデータベースにクエリを実行します。データベースにどの句を追加する必要がありますか?

私はこれをまったく理解していません。単純化後のデータベースは基本的に r です。r は本当ですね。

4

1 に答える 1

1

「r を使用してデータベースにクエリを実行したいのですが、データベースにどの句を追加する必要がありますか?」という質問 いわゆる反駁証明のこと。反駁証明では、次のことは証明されません。

 Database |- Query

代わりに 1 つの証明:

 Database, ~Query |- f

古典論理では、この 2 つは同じです。したがって、あなたの例では、 p ^ q ^ (r V ~q) ^ (~p V ~s) ^ (s V ~t) ^ t ^ ~r が矛盾につながることを示す必要があります。

さよなら

編集 14.02.2019:
命題式を CNF に変換するための Prolog コードに興味がある場合は、こちらを参照してください https://gist.github.com/jburse/ca8d01e26c7cf176ea65eeb1bf916ea0#file-aspsat-p (43 ～ 87 行目、Prolog Commons が必要)リストと ordset)を呼び出して、式Fを CNFに変換できます。Cnorm(F,H), cnf(H,C)

取得された CNF は、自明で包含された節から既にクリーンアップされています。誰かが CNF テスト ケースにさらに興味がある場合は、ここhttp://gist.github.com/jburse/bf992​​39903847322321fabf6f49a5b84 # file-casescls-p を参照してください。Principia Mathematica からの数百のトートロジーと、別の方法で収集された 10 分の 1 の誤謬が含まれています。

于 2015-08-18T09:31:12.390 に答える