問題タブ [first-order-logic]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
logic - 不動点と証明理論
任意の論理プログラムについて、その証明理論は SLD (Selective Linear Definite) 解決を使用してクエリの充足可能性を見つけます。同じ論理プログラムに対して、不動点定理を適用してモデルを見つけることができます。
私の質問は、
論理プログラムの不動点を証明理論やモデル理論として考えるべきか、それともどちらでもないのか?
logic - 人工知能と一次論理
全称量指定子または存在量指定子をいつ使用するか決めかねています。これが私の例です。歴史の試験に合格し、宝くじに当選した人は誰でも幸せです。一次論理: ∀x Pass(x,history) ^ win(x,lottery) -> happy(x) or ∃x Pass(x, history) ^ win(x,lottery) -> happy(x)ロジックが正しいかどうかを知りたい。
coq - Coqの「elim」は存在量指定子でどのように機能しますか?
Coq が存在量化を扱う途中で混乱しています。
述語 P と仮定 H があります
現在の目標は（何でも）
H で n をインスタンス化したい場合は、そうします
ただし、削除後、現在の目標は
Coq が存在量指定子を普遍的な量指定子に変換しているようです。(forall a, P a -> Q a) -> ((exists a, P a) -> Q a)ということは、一階論理に関する限られた知識から知っています。しかし、逆の命題は正しくないようです。「forall」と「exists」が同等でない場合、なぜ Coq はそのような変換を行うのでしょうか?
Coqの「elim」は、目標を証明するのが難しいものに置き換えますか? または、((exists a, P a) -> Q a) -> (forall a, P a -> Q a)が一階論理で成立する理由を誰かが示してくれませんか?
z3 - SMT2 でのビット ベクトルのルールの定義
SMT で Int から Bit Vector を使用するように切り替えました。ただし、ロジック QF_BV では、スクリプトで量指定子を使用できないため、FOL ルールを定義する必要があります。存在量指定子を削除する方法は知っていますが、普遍的な量指定子は? どうやってするか？
次のようなコードを想像してください。