connjectureの意味

公理の集合Aと、証明したい式Cの関係を考えたい。 Wikiで書くのは面倒だ。

conjectureの否定をP(x)とかですませていたのは、いろいろわけがあった。 programの仕様としては、E.x.P(x) になるので、否定して、A.x.P(x) だったから、clause P(x)だった。 Resolution 適用して問題起こらない。

Aは、factであるground unit clauseと、法則を示す公理からなる。

+P(a)v +P(b)はもはやfactではない。

conjは、公理集合が満たす性質を示すのか。

E.x.φ(x)なのかA.x.φなのか。

conjectures の否定が複数のとき、全clauseから各□を証明できないとダメ。 E.x.φ(x)は、エルブラン宇宙のすべての項についてφ(x)が真である。