問題タブ [first-order-logic]

これは私のPythonコードです:

このコードでは、Z3Py 構文で次の式を記述しました。

このスクリプトを実行すると、モデルが見つかりますが、unsat. どうしてそれが可能でしょうか？何か不足していますか？

私はこの表現に遭遇したばかりで、これまで普遍的な量指定子を学んだことがないので、これが何を意味するのかわかりません。

私はそれが普遍的な量指定子であることを知っていますが、それがどのように機能するのかわかりません

流れている文が有効か、偶発的か、満足できないかを尋ねる質問に遭遇しました。

答えは文が有効だと思います。ここの教科書のセクション6.10の下でhttp://logic.stanford.edu/intrologic/secondary/notes/chapter_06.htmlsays

自由変数を含む文は、すべての自由変数が普遍的に量化されている文と同等です。

したがって、最初の関係文 p(x) は ∀xp(x) に等しく、したがって文は有効であると思います。それは常に真実です。

ただし、正解は文が偶発的であるということです。ある真理割り当ての下ではそれは真であり、他のいくつかの他の真理割り当ての下ではそれは偽です。

では、なぜ文は条件付きなのですか?答えは間違っていますか?

私は長い間、次の文の同等性を直感的に理解するのに問題があります

∀x.(px=>q)

∃x.px=>q

以下の真理値表は、それらが同等であると述べていることを理解しています。

しかし、私が探しているのは 、等価性の有効性を検証するための人間の言語の例です。そのため、より直感的に理解できます。誰か例を挙げてもらえますか?

私は文章かどうか疑問に思った

∃x.px=>q

に等しい

∃x.(px=>q).

次の例から、それらは等しいと思います。

最初の文のインスタンス:

牛がいれば哺乳類です。

2 番目の文のインスタンス:

牛がいる、牛なら哺乳類。

それらが等しくない場合、私の例の何が問題になっていますか?

量指定子、自由変数、束縛変数の範囲に関するいくつかの質問に対する適切な説明が見つかりませんでした。

1) ∃X(p(X,Y) & ∃Y(X,Y)) - 2 番目の X について疑問に思っています。実際には ∃Y の下にネストされているため、まだ ∃X 量指定子の範囲内ですか? ∃X のスコープ内にない場合、それは自由変数ですか? ∃X にバインドする必要があると考えています。
2) ∃X(p(Y,Z) & ∃X(q(Y,Z)) - 2 番目の ∃X が必要ですか? 自由変数 Y と Z に対して何か変更がありますか?

このタイプの質問は他にもありますが、これらの 2 つが現在最も気になっています。それらに答えると、一般的なアイデアが得られ、次の質問に答えることができます。

また、このタイプのものが詳細に説明されているリソースがあれば、私は感謝します!

前もって感謝します！

正規表現を使用して、任意の関数のパラメーターを文字列として一致させたいと思います。例として、次の文字列を想定します。

これは、より長いシーケンスの一部である可能性があります

ここで、関数/述語とそのパラメーターを表すすべての部分文字列を検索したいと考えています (つまり、最初の例では、文字列全体とネストされたpredicate(foo(...), bar))。問題は、このように単純に一致できないことです

*貪欲な場合は述語のパラメーターよりも多く一致する可能性があり、怠惰な場合はより少ない可能性があるためです。これは、そのような predicates() をネストできるためです。

と が同量含まれる任意の文字列に一致する文字列predicate(...)を見つける正規表現が必要です(遅延)。...()

問題がある場合: Python の re モジュールで正規表現を使用しています。