first-order-logic

1熱

2答えて

私が流れるの文が有効/偶発/充足不能であるかどうかを尋ねる質問が発生しました： p(x)⇒∀x.p(x) 私は答えは文が有効であると思います。ここhttp://logic.stanford.edu/intrologic/secondary/notes/chapter_06.htmlsays 教科書のセクション6.10の下で自由変数を持つ文は自由変数のすべてが普遍的に定量化された文と等価です。

0熱

1答えて

誰でも∀x。（px => q）が∃x.px=> qを満たすことができる人間言語の例を与えることができますか

私は次の文の等価性を理解するのに問題があります。直感的に。 ∀x（PX => Q） ∃x.px=> Q 私は以下の真理値表がない理解は、彼らが等価であると言う： p(a) p(B) q p(a)=>q p(b)=>q (p(a)=>q)&(p(b)=>q) p(a)|p(b) p(a)|p(b) =>q T F T T T T T T F T T T T T

0熱

1答えて

∃x.px=> qは∃x（px => q）と等しいか？

Iは、IF文 ∃x.px=> Q ∃x。（PX => Q）に等しいを疑問。私は、彼らがために、次の例で同じであると思う：最初の文の例：牛が存在する場合、それは哺乳動物です。第二文の例：それは牛である場合牛が存在し、それは哺乳動物です。等しくない場合は、私の例で何が問題になりますか？

1熱

3答えて

正規表現一致する2文字の文字数

正規表現を使用して任意の関数のパラメータを文字列として照合したいと思います。例は次の文字列とさせて頂きますよう： predicate(foo(x.bar, predicate(foo(...), bar)), bar) これは、より長い配列の一部であってもよい predicate(foo(x.bar, predicate(foo(...), bar)), bar)predicate(foo(x

0熱

1答えて

Z3での記録

私はドキュメントとガイドをよく見て、公正ないくつかのものを自分で試しました。しかし、私の問題に対する解決策は、私を避けています。これは、チュートリアルでは、レコードに関して言うが、それは私のニーズに合わせ持っているか私には不明であるものです： (declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) (decla

2熱

1答えて

EPR断片のプレノックス定量の順序は重要ですか？

1次論理の効果的命題（EPR）フラグメントは、しばしば∃X.∀Y.Φ(X,Y)という形式のプレノックスで数量化された式のセットとして定義されます。XとYは（おそらくは空の）可変シーケンスです。定量化の順序、つまり∃*∀*はEPRの決定可能性に関係しますか？定量化の順序が入れ替わった場合、決定性を失うか？特に、私は決定可能なロジックで集合モナドのバインド操作のセマンティクスをキャプチャすることに興

1熱

1答えて

TPTPの文法的に異なる用語を表現する

私はVampireやE-Proverのような一次論理定理証明者を見ています.TPTP構文は今後の道のりです。 Answer Set ProgrammingとPrologのようなLogic Programmingの構文にはよく慣れていますが、TPTP syntaxの詳細な説明を参照しようとしていますが、解釈されたファンクタと解釈されないファンクタを正しく区別する方法はまだ分かりません。間違った用語を

3熱

1答えて

ファーストオーダーロジックプロローグ匿名変数

以下のPrologのルール：我々はPrologのルールで何かを匿名変数を持っている場合理論的には ∀x ∀y ∀z ((P (x, y) ∧ P (y, z)) → G(x, z)) ：一階述語論理で grandparent(X,Z) :- parent(X,Y) , parent(Y,Z) があることを行っていますlike： grandparent(X,Z) :- parent(X,Y,

0熱

2答えて

ユニバーサル定量器を使用したこの式は何を意味しますか？

私はこの式に遭遇しました。私はこれまで普遍的な量量子を学んだことがないので、何を意味するのか分かりません。 ∀α.α → α は、私はそれが普遍数量詞である知っているが、私はそれが

0熱

1答えて

∀x。（p（x）⇒∀y.p（y））を読むには？

私はここで質問しました：p(x)⇒∀x.p(x) is contingent? p（x）⇒∀xp（x）は∀x。（p（x）⇒∀yp（y））と同じ傾向にあるようですが、 xに対してp（x）が真であるかのように、∀x。（p（x）⇒∀yp（y））が読み取られると、すべてのxについて真です。がですそこには数量詞 '∃' の '∀x。（P（x）は⇒∀yp（Y））' 以来、SOMEがどこから来た数量詞だところ