Thm
p-Formに対しては \(\downarrow\) の結果は一階言語になる必要があります。
「推論可能かどうか」は \(\downarrow\) をした上で一階論理により判定されます。
なお、一階論理の（等号公理を含めた）公理・推論規則は仮定されます。
例 【\(x \neq y\)】\(\blacktriangleright\)【\({\perp}\)】
ここでは、空の列を\(\text{O}\)、列の要素の区切りは太コンマ \({\bf ,}\) にします。
例 \(\text{O}\;\blacktriangleright\)【\(x = x\)】
Thmの証明探索
私たちはThmの証明を機械に探索させます。それはいくつかのsoftwareを組み合わせて遂行されます。
主要なものはphpとProverで、補助的にいくつかの計算softwareが使用されます？
最終段階はProverに任され、Proverに渡す文字列はphpで作成されます。
機械は証明があったときにのみ「あった」と答えてくれます。「そのThmは正しい」と言ってもらえると、安心します。
Proverによって出力された証明の中身はまだ利用できていません。
証明探索の効率を上げることが私たちにとって最重要の課題であります。
Proverをいじるのは難しそうなので、phpを洗練していくべきです。人間にとって簡単でもProverには難しいことがあるので、まずはそこをphpで補助します。現状ではphpでは一定の規則に従った計算をするだけで探索と呼べる事はしていません。Proverとやりとりをしながら探索をする？
論理同値
Assumptions無しで \(\text{O}\blacktriangleright{\tt P}\Leftrightarrow{\tt Q}\) となるとき \({\tt P}\) ≡ \({\tt Q}\) とされます。例 【\(x \neq x\)】≡【\({\perp}\)】\(\top,{\tt P}\) ≡ \({\tt P}\) というような演算も行われます。
\({\tt P} \stackrel{\rm v}= {\tt Q}\) なら \({\tt P}\) ≡ \({\tt Q}\) です。
p-Form/≡ の列 \(\mathcal{A}\) と元 \({\tt P}\) に対しても \(\mathcal{A}\blacktriangleright{\tt P}\) が自然に定義されます。
FormをProverに渡すとき等では、\({\tt P}\) ≡ \({\tt Q}\) なる \({\tt P}\)と\({\tt Q}\) は同一視されます。