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

Question

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

本質的には、モデルが反例として機能しないことを示すことによって定理を証明しようとしています。私の最初の難しさは、次の論理プログラムが充足できるとは思わなかったということでした。

fof(all_foo, axiom, ![X] : (pred(X) => (X = foo))). 
fof(exists_bar, axiom, pred(bar)). 

何もfooに等しいからbarを防止していないので、それは確かに充足可能。したがって、最初の解決策は、これらの2つの用語が異なることを主張し、次の満たされないプログラムを取得することです。

fof(all_foo, axiom, ![X] : pred(X) => (X = foo)). 
fof(exists_bar, axiom, pred(bar)). 
fof(foo_not_bar, axiom, foo != bar). 

Techinal報告書は、異なる二重引用符で囲まれた文字列が実際に異なるオブジェクトであることを明確にしているので、他のソリューションには、次の充足不能のプログラムを得られるように、あちこちで引用符を置くことです。

fof(all_foo, axiom, ![X] : (pred(X) => (X = "foo"))). 
fof(exists_bar, axiom, pred("bar")). 

私はそれは明らかに、より現実的なシナリオに拡張しませんように手動不平等を指定していないようにうれしいです。私の実際の状況に近づくにつれて、実際には構成された用語を処理しなければならず、次のプログラムは残念ながら満足できるものです。

fof(all_foo, axiom, ![X] : (pred(X) => (X = f("foo")))). 
fof(exists_bar, axiom, pred(g("bar"))). 

私はf("foo")という言葉が、オブジェクト"foo"に適用される関数fではないと思います。したがって、機能gと潜在的に一致する可能性があります。 fとgが決して一致しないマニュアル仕様は、このトリックはありませんが、次のプログラムは満足できません。私は間違っているように感じています。そして、文法的に異なっているときには、多くの用語を区別して解釈することは、おそらく私の実際の設定には適用されません。

私は周りに一重引用符を投げてみましたが、それを行う適切な方法が見つかりませんでした。

構文的に異なる（構成された）用語を作り、構文的平等をテストするにはどうすればよいですか？

副次的な質問：自動化定理の証明者が未解釈のファンクタではなく関数としてfを理解しているので、次のプログラムは充足可能です。

私は手動でfを注入するように指定する必要があります。プログラムで発生するすべてのファンクタの注入性を指定せずにこの動作を取得する自然な方法は何ですか？

fof(exists_f_g, axiom, (?[I] : ((f(foo) = f(I)) & pred(g(I))))). 
fof(not_g_foo, axiom, ~pred(g(foo))). 
fof(f_injective, axiom, ![X,Y] : (f(X) = f(Y) => (X = Y))). 

Answer 1

最初に、TPTPのSyntax BNFに指摘してください。原則として、適切な優先順位の事前定義済みの接尾辞/接頭辞演算子を持つPrologの用語を使用します。つまり、変数は大文字で書かれ、定数は小文字で書かれています。また、Prologのように、一重引用符でエスケープすると、大文字の 'X'で始まる定数を書くことができます。これまで二重引用符で囲まれた原子は見たことがないので、それらを解釈する方法について証明者の指示を調べるとよいでしょう。

しかし、構文がProlog-ishであっても、自動定理証明は異なる種類の獣です。あなたは構文DISを持つようにしたいのであれば

fof(c1, conjecture, ~(a=b)). 

：

fof(c1, conjecture, a=b). 

とのためでもない：あなたがのための証拠を見つけることができない理由です - そこには閉世界仮説があることも、異なる定数が異なることが想定されています-equality、あなたはそれを公理化する必要があります。ここで、bとは異なると仮定すると、それらが異なっていることが分かります。したがって、私は少なくとも「aとbの2つの異なる定数があると仮定して、bでない変数が存在します。

fof(a1, axiom, ~(a=b)). 
fof(c1, conjecture, ?[X]: ~(X=b)). 

一次論理の関数は必ずしも注入型ではないので、そこにあなたの前提を追加することもできません。

入力式のさまざまな役割にも注意してください。これまでのところ、公理と推測は記述されていませんでした。つまり、証明者にあなたの公理が矛盾していると表示するよう依頼します。いくつかの証明者は、公理間の解決を制限するいくつかの解決策の細分化（例えば、サポートのセット）を使用するので、あきらめるかもしれない[1]。いずれにしても、あなたが証明しようとしている数式は、A1 ∧ ... ∧ An → C1 ∨ ... Cmの形であり、Aは公理であり、Cは推測であることに注意する必要があります。[2]

少なくとも構文が少しはっきりしていることを願っています。残念なことに、疑問の答えは、より多くの霧化された定理証明者があなたが期待しているのと同じ仮定をしないためです。これらの公理化はしばしば効果がなく、特殊なツールからより良い性能を得るかもしれません。

[1]既に気付いているように、VampireやE Proverのような高度な証明者は、代わりに（カウンター）満足度を教えてくれます。

[2]解決策ベースの定理証明者は、最初にその式を否定してCNF変換を行いますが、ほとんどのTPTP受理証明者は解決基準に基づいていますが、これは必須条件ではありません。