0

ソフトウェア検証モジュールでは、真理値表から自然推論に移行しました。真理値表は非常に基本的なものに見えましたが、現在は coq の定理証明器を使用して、より複雑なステートメントを証明しています。私を混乱させているのは、「証明されているか証明されていない」タイプの答えになる方法です。真理値表を使用すると、入力に基づいて真または偽のタイプの結果が得られる場合、これは自然な演繹を使用して調べることを意味しますか?トートロジーの場合、または完全に何かが欠けていますか?

4

2 に答える 2

4

それらには異なる意味があります。真理値表は、命題のセマンティクスに対応します。自由変数 ("forall" または "exists" 内にない任意の変数、またはあなたが言うように "inputs") が真か偽かによって、命題が真か偽かを確立します。

真偽値を入力に直接割り当てないため、自然演繹は異なります。自然演繹では、命題から始め、演繹または「自然推論」を使用して命題から新しい命題を作成します。基本的に、「推論ルール」と呼ばれる、これらの命題を構築する方法を示す一連のルールがあります。

例を使ってみましょう: を証明したいです|= A->A。

真理値表 まず、の真理値表を見てみましょう|= X->Y

X | Y | X-> Y
-------------
T | T | T
T | F | F
F | T | T
F | F | T

それでは、それを適用してみましょう|= A->A

A | A | A-> A
-------------
T | T | T
T | F | F
F | T | T
F | F | T

A は常に同じ値を持っているため、そこにある 2 つの行を切り取って、次のようにすることができます。

A | A | A-> A
-------------
T | T | T
F | F | T

これは何を意味するのでしょうか？それ|= A->Aは常に真であることを意味するので、意味論的に証明しました。

自然控除

ここでは|- A->A演繹法を使って証明したいと思います。そのために、「含意」の (簡略化された) 推論規則を見てみましょう。

A |- B
--------
|- A -> B

この推論規則は次のことを教えてくれます。最初に小さな命題の証明を作成し、次にそれらを結合してより大きな命題の証明を作成します。

使用できる別の推論規則もあります。

A |- A

これはどういう意味ですか？それが起こると仮定すれば、いつでも何かを証明できることを意味します。理にかなっていますよね？

したがって、これらの新しい規則を使用して を証明できます|- A->A。どのように？簡単：

A |- A
------
|- A -> A

「含意」の推論規則を使用し、B を A に置き換えました。次に、 を証明する必要がありますがA |- A、それは私たちが知っている別の推論規則です! これで、 が真であることはすでに証明されてい|- A->Aます。ただし、真理値表を使用する必要はまったくありませんでした。

|= A->Aあなたは、それらのうちの1つがどのようであるかに気付くかもしれません|- A->A. これは、|=手段が「意味的に含意する」のに対し、|-手段が「証明する」ためです。ただし、どちらも等価です。そのうちの 1 つが真である場合、もう 1 つも真であると証明することにより、|- A->A真であることが証明されます。|= A->Aつまり、それA->Aはトートロジーです。

これは、自然演繹法を使用してトートロジーを探すということですか、それとも完全に何かが欠けているのでしょうか?

トートロジー以外にも多くのことを証明できます。トートロジーは、何があっても常に真である命題です。これは、何を仮定しても、「入力」にどの値を割り当てても、それが真であることを意味します。|= Xこれは、X がトートロジーであることを示す表記法で表されます。ただし、その左側に命題を含めることはできます。そうすると、左の命題が真であると解釈した場合にのみ、右の命題が真であるということになります。たとえばA |= A。これは、 (左) に値trueを割り当てる任意の解釈で、 (右) にも値があることを意味します。任意の命題、または命題のリストを左側に含めることができます。たとえば、それを解釈するたびにAAtrueA,B |= A /\ BA値をB持っているtrueので、そうA /\ Bです。自然演繹に戻ると、同じことができます ( に変更|=することを忘れないでください|-)。たとえばA,B |- A /\ B 、推論規則を使用して、それが真であることを証明できます。

しかし今は、より複雑なステートメントを証明するために coq Theorm Prover を使用しています。

ここで注意が必要です。Coq は自然演繹法を使用しませんが、直観論的論理と呼ばれるものを使用します。これはこの質問の範囲外かもしれませんが、詳細情報が必要な場合は、ウィキペディアのページをご覧ください。

http://en.wikipedia.org/wiki/Intuitionistic_logic

于 2013-11-30T01:12:25.227 に答える
0

自然演繹法を使用して真理値表でできることはすべて定式化できますが、それは形式が異なるだけです。P : Prop -> Prop -> Prop次のような真理値表を持つ命題があるとしましょう

 A | B | P
 ---------
 T | F | T
 T | T | T
 F | T | T
 F | F | F

これを次のように述べることができます

 Theorem or_equiv : forall A B, A \/ B -> P A B

または類似。これは、常に真であるという意味でトートロジーですが、真理値表で表現できることはすべて表現できます。

于 2013-11-15T00:38:37.887 に答える