問題タブ [first-order-logic]

Coq のチュートリアルを読んでいます。次のように型を構築boolします。

次に、これらのそれぞれが「チェック」を使用しているものを示します。

わかりbool_indました。何かが成り立ち、 がtrue成り立つ場合false、オールbインも成り立つboolということです (これらは 2 つしかないため)。

bool_recしかし、表現やbool_rect意味がわかりません。P true( Setforbool_recとTypefor bool_rect) が命題値として扱われているようです。ここで何が欠けていますか？

Starcraft で情報を表すオントロジーに取り組んでいますが、次の一般的なクラス公理を DL で表すことができるかどうかを判断するのに苦労しています。そうでない場合は、それを表現するために必要な最小の論理セット (FOL、2 次など) を知りたいです。

この公理で、(1) その地域にユニットが存在し、(2) その地域のすべてのユニットがプレイヤーによって所有されている場合、プレイヤーがその地域を支配していることを表現したいと思います。

私には 3 つの役割があります。

A. controlsRegion(p,r) ここで、p はプレーヤー、r はリージョンです

B. isOwnedBy(u,p) u はユニット、p はプレイヤー

C. isInRegion(u,r) ここで、u はユニット、r はリージョンです

画像を投稿するのに十分な担当者がいません。ここで式を参照してください: http://postimg.org/image/wve0h9m1z/

u、p、r は変数です (これが DL で表現できるとは思えない理由です)

また、使用している構文が正しいかどうかもわかりません。適切に表現する方法を教えてください。

ありがとう、どんなフィードバックでも大歓迎です！

タイトルが示すように、たとえば解析しようとしています

のようなLuaテーブルで

これは私が構築した文法です:

次の問題があります。

• ネストされた用語を解析できません。上記の例では、 のみを返します{term, {} }(ただし、 で問題ありませんterm(A, b, c))。
• 使用した文字列から引用符を取り除く{~ ~}ために、そのため、すべてのキャプチャを下の行から移動する必要がargumentありました。termこれを回避する方法はありますか？
• Aたとえば、のようなものの代わりに、各要素にキーを関連付けてそのタイプを指定したいと思います{value = "A", type = "variable"}。これを行う方法を見つけました{:name: :}が、テーブル内の要素の順序が失われます (新しいテーブルを作成するのではなく、単にキーを追加するためです。この場合variable="A"、この要素の順序は固定されていません)。注文を維持するアイテムにタグを付けるにはどうすればよいですか?

LOADキーワードは、どのような関係代数演算子にマップされますか? それが論理演算子ではなく物理演算子のみである場合、データベース クエリ プロセッサによる論理演算子から物理演算子への変換プロセス中にどのように処理されるのでしょうか? または、関係代数プリミティブにマップされていない場合、実装固有の関係代数演算子の拡張ですか?

次の考えを一次論理で表現するのに苦労しています。

すべてのエージェントには最初の位置があると言いたいのですが、これを (言葉を使って) 次のように表現します。

エージェント タイプのすべてのエージェントの場合、I_Position(agent,x,y) AND Tile(x,y) となる xCoordinate タイプの x と yCoordinate タイプの y が存在します。

またはidpで：

tile は有効なタイル、有効な位置の式です。

For Allこの式の問題は、式には常に含意 ( =>) があり、There Exists式には常に And ( )があることを学んだこと&です。

明らかに、私には意味がありません。この文は、私が思っていることをしていますか?

FOL文を取り、同等のものを節形式で返す関数を実装しようとしています。これまでのところ何も見つからないため、リンク、サンプルのアイデア。

それは常に真実だと思う

と同等です

もしそうなら、その法律は何と呼ばれていますか？そのためにGoogleをどのように使用するかさえわかりません。

命題論理と一次論理の違いを教えてください。これは AI の私の試験問題の 1 つです。

Mercury 言語を調べ始めましたが、これは非常に興味深いと思われます。私はロジック プログラミングは初めてですが、Scala と Haskell での関数型プログラミングにはかなりの経験があります。私が考えていることの 1 つは、少なくとも型と同じくらい表現力のある述語が既にあるのに、なぜ論理プログラミングで型が必要なのかということです。

たとえば、次のスニペットで型を使用する利点は何ですか (Mercury チュートリアルから抜粋)。

述語のみを使用して記述する場合と比較して:

このトピックを扱っている紹介資料を自由に参照してください。

編集：おそらく質問の定式化が少し不明確でした。Idris のような依存型型付け言語を調べた後、私は実際に Mercury に注目し始めました。依存型型付けの型で値を使用できるのと同じ方法で、論理プログラムの正確性を検証するためにコンパイル時に述語を使用できるのと同じ方法です。プログラムの評価に長い時間がかかる場合、コンパイル時のパフォーマンス上の理由から型を使用する利点が見られます (ただし、依存型の型付けについて話すときは必ずしもそうではない「実装」よりも型が複雑でない場合のみ)。私の質問は、コンパイル時のパフォーマンス以外に型を使用する利点があるかどうかです。