1

私はZ3の新規ユーザーであり、いくつかの公理とそれらの公理のみを使用して、式を一階述語論理の別の同等の式に変換することを望んでいます。例：使用のみ

1.（pまたはq）および（pまたはr）<=> pまたは（rおよびq）

2.not（pまたはq）<=> not（p）およびnot（q）

3.pおよびp<=>p

証明する

not（pまたは（qおよびr））<=>（not（p）およびnot（q））または（not（p）およびnot（r））

私はC＃APIを使用しています。解釈されていない関数を使用する必要があると思いますが、その方法がわかりません。

Plzzヘルプ。

4

1 に答える 1

1

そうです、アイデアは解釈されていない関数とソートを使用することです。Z3でエンコードされた問題は次のとおりです。http： //rise4fun.com/Z3/Vzns

Z3は、提供された3つの公理を使用した証明を見つけられません。実際、結論は彼らからは得られません。しかし、公理を置き換えると証拠を見つけることができます

pおよびp<=>p

と

not（not（p））<=> p

注：上記のスクリプトのエンコーディングでは、のB代わりに未解釈の並べ替えが使用されていますBool。したがって、Z3はケース分析による証明も試みず、 Bool2つの要素のみを含む事実を使用しようともしません。

備考：=の代わりに使用し<=>ます。

次の例では、Z3Pyを使用して、指定した3つの公理を満たすモデルを構築しますが、推測は成り立ちません。

http://rise4fun.com/Z3Py/7H7

于 2012-05-17T15:25:20.863 に答える