問題タブ [first-order-logic]

次回の試験について、次のレビュー用の質問があります。サポートが必要です。「メアリーは青リンゴだけを使ってパイを作る」という質問に、解像度を使って答える必要があります。私の現在の知識ベースと言語は次の文章です。

最新の更新：

一般的にはもっと具体的にしようと思います。私が証明したいのは、「メアリーはパイを作るのに青リンゴだけを使う」ということです。このロジックを書くと、次のようになります。

メアリーは、青リンゴのみを使用してパイを作成します。π、aPie（π）A Make（M、π、a）=> Green（a）

そして、それをCNF形式（http://en.wikipedia.org/wiki/Conjunctive_normal_form）に変換する手順：

CNF形式でのこのステートメントの否定（証明の解決に使用します）：

Pie（π）A Make（M、π、a）A⌐Green（a）

一階述語論理に解決を使用する場合：（http://en.wikipedia.org/wiki/Resolution_(logic））

これは正しいですか！？それとも私はそれを間違えていますか？

2 つの 1 次式 F と G が等しいことを自動的に証明する最良の方法は何ですか?

式には、「完全な」一次式と比較していくつかの制限があります。

1. 量指定子なし
2. 機能フリー
3. 暗黙的に普遍的に量化された

これらの式を句の標準形に変換でき、リテラルの統一のためのルーチンがあります。ただし、続行する方法と、この問題が決定可能かどうかはわかりません。

Prologではどんな文章が表現できないのかしら？私は一般的な論理プログラミングを研究してきましたが、一階述語論理は、Prologが基づいている明確な論理（ホーン節）と比較してより表現力があることを学びました。頭を動かすのは難しいテーマです。

したがって、たとえば、次の文を表現できます。

もしそうなら、表現できない他の文章はありますか？そうでない場合、なぜですか？

わかりました、与えられた関係があります: F(x) が真でない場合、G(x) と H(y,x) を満たすケースはありません。((∀x ¬F(x)) ⇒¬(∀y G(y) ˄ H(y,x)))

さて、これを次のように変換できますか: (∀y G(y) ˄ H(y,x))) ⇒ ((∀x F(x)) ????

そうでない場合、左辺は本質的に次のことを暗示する必要があります。F(x) が true でない場合.... For All または Existential 数量詞については何も言及していません。量指定子の外で否定を取ることはできますか、つまり (¬(∀x F(x)) のように置きますか?

Microsoft が開発した SMT ソルバーである Z3 に 1 次理論を入れたいと考えています。この理論には、オブジェクトobj1とobj2の 2 つのオブジェクトがあり、オブジェクトを受け取りアクションを返す関数moveと、アクションを引数として取る1 位の述語が発生します。理論には数式occurs(move(obj1)) が含まれており、これが発生述語が真になる唯一の方法であることを確認したいと思います。私は発生の定義を与えることによってこれを行います:

これは、ocens(move(obj1))は理論から推論できますが、ocens(move(obj2))は推論できないことを意味します。これを証明するために、私はこれを次のように Z3 に翻訳しました。

問題は、これにより次の出力が得られることです。

私には理解できません。発生の定義は、述語が真になるための必要かつ十分な条件をすべて提供するため、どのモデルでも発生(move(obj2))が真になることはできないと思います。私は何を間違っていますか？

更新 de Moura のおかげで、問題の解決策を見つけることができました。私がする必要があるのは、アクション (私の場合は関数) に固有の名前の公理を提供することです。2 つの異なる引数がある場合、 sort の同じ要素を決して返さないことmoveを述べる必要があります。これはいくつかの方法で実行できますが、これが最も簡潔なバージョンであることがわかりました。moveAction

私は最近AIコースでKRL（知識表現言語）を学び、記述論理がセマンティックWebの正式な知識表現言語のファミリーであることを魅力的に感じました。さらに、記述論理では、一階述語論理よりも知識を表現する方が簡単で扱いやすいです。

その記述論理または一階述語論理を処理するために利用できるJavaライブラリについて誰か知っていますか？

ドメイン分類と用語に関する情報を推測するためにオントロジーを構築しようとしていますが、概念的な問題が発生しています。

問題を説明しましょう。Protègè 4.1 では、Thing の 6 つのサブクラス、Concept、conceptTitle、ConceptSynonym (分類用) および Term、TermTitle、TermSynonym (用語用) を作成しました。また、hasConceptTitle、hasConceptSynonym、hasTermTitle、および hasTermSynonym オブジェクトの関係を作成し (いくつかの制約付きで)、すべてのコンセプトには 1 つ (1 つだけ) のタイトルがあり、いくつかのシノニムを持つことができ、すべての用語には 1 つ (1 つだけ) のタイトルがあり、いくつかの同義語。Concept と Term には別の関係 isA があり、分類に DAG/ツリー構造を与えますが、Terminology には格子構造があります (つまり、用語は複数の用語のサブクラスである可能性があります)。

ここで問題が発生します: 概念のサブクラスを作成したいと思います (たとえば、「MappedConcept」としましょう)。これは、マップされた概念のセットである必要があります。これは、用語のタイトルに等しいタイトルを持つ概念のセットです。シノニムが用語のタイトルと等しいか、用語のシノニムと等しいシノニムを持っています。一次論理では、このセットは次のように表現できます。

どうすればこれを入手できますか? 「ConceptTitle」、「ConceptSynonym」、「TermTitle」、および「TermSynonym」のデータ プロパティを定義していますか? そして、文字列の一致をどのように説明しますか? たぶん、これらの 4 つのクラスは、Concept クラスと Term クラスの単なるデータ プロパティである必要がありますか? マシュー・ホリッジの実践ガイドを何度か読みましたが、頭に浮かんだ実践的なアイデアを Protègè の腫瘍学にまとめることはできませんでした。

前もって感謝します。

解釈されていない並べ替えと関数で遊んでいて、定量化された数式が空のモデルとどのように相互作用するかを完全に理解できません。ここ（ここでもhttp://rise4fun.com/Z3Py/6ets）は、私をやや混乱させるいくつかの簡単な例です：

1. [∀v : False]は未飽和ですが、「直感的に」空のモデルに当てはまります。
2. チェック[∃v : v = v]すると空のモデルが生成されますが、それには満足のいく割り当てがありません。
3. と一見同等のいくつかの式は[∃v : v = v]、どういうわけか z3 が空のモデルを生成するのを防ぎます。[∃v, v1 : v = v1]はその一例です。たとえば、そのような式をソルバーに追加してから、allsat プロシージャに似たものを作成しようとすると (より多くのモデルを除外するために、より多くの制約を追加する)、空のモデルを取得する前に unsat に遭遇します。

では、z3 が量指定子と空のモデルをどのように処理するかを説明しているドキュメント/論文を参照していただけますか? また、空でないモデルのみに注意を向けることを選択した場合、z3 にそれを求める正しい方法は何ですか? のような[∃v, v1 : v = v1]ことがうまくいくように見えますが、より良い方法はありますか?

古典的なアインシュタイン/ゼブラ パズルは次の形式で与えられます。

同じ道に色の違う家が5軒並んでいるとします。各家には異なる国籍の男性が住んでいます。人は皆、好きな飲み物、好きなタバコのブランドを持ち、特定の種類のペットを飼っています。

タスクは、パズル内の 5 人の人物がイギリス人、スウェーデン人、デンマーク人、ノルウェー人、ドイツ人、およびキープであると仮定して、これらのステートメントを一次論理の一連の閉じた式として表現することです。 (X,Y) は、X がペット Y を飼っていることを意味します。これらは後でプロローグに変換されます。

私の質問は、ステートメントを正しい方法で変換しようとしているかどうかです。今、私は次のようなものを持っています：

これは正しいですか、それとも私が試した他の方法に似ているはずです:

私も次のようなことを試みました：

最初のものが最も正しいと思いますが、よくわかりません。また、一次論理でセンターやネイバーなどを表現する方法もわかりません。これらのどれかが正しいに近いですか？

編集:おそらく正しいと思われる解決策を思いつきました。CLOSED式と書かれていることに気づいたので、次のようにしました。

これは正しい方法ですか？どんな助けでも大歓迎です。

したがって、Z3py で次のコードを単純化する方法を探しています。このアサーションを確認するたびに (自分のコンピューターまたはhttp://rise4fun.com/z3py/で) タイムアウトになったので、そこにあると思います最速の方法かもしれません。

ご覧のとおり、これは非常に大きな式ですが、それを小さくする方法は見つかりませんでした...目的は、タスクのすべての部分が異なるプロセッサによって処理されている場合でも、順序どおりであることを確認することです (p1または p2)

あなたが私を助けることができれば、前もって感謝します（その式を変更するのに役立つヒントだけでも素晴らしいでしょう）

編集：その制約を単独でテストしたところ、機能します。奇妙な結果が得られますが、それでも機能しますが、他の制約と連携する必要があるため、最適化を手伝っていただければ大歓迎です。