1

チェックした後に論理コンテキストを表示すると、特に次のようになります。

inconsistent():1
m_asserted_formulas.inconsistent():1
#1 := true
#2 := false
... (follows around 40 of theses assertions)
#144 := (not #143)
asserted formulas:
#23 #125 .... #2

主張された公式のリストには、いくつかの矛盾があることを理解しています。私が最初に目にするのはアサーション番号2です。

#2 := false

私は正しいですか、それとも「偽」が真の主張である可能性がありますか？

前もって感謝します、

AG。

4

1 に答える 1

2

はい、falseあなたの文脈では真実であると主張されました。コンテキストは不整合としてタグ付けされていることに注意してください：inconsistent():1。ここでは、Cでは通常どおりを1意味trueします。論理コンテキストのこの低レベルの表現は、デバッグ目的でのみ使用する必要があることに注意してください。それは実際には「外部」消費を意図したものではありません。最後にfalse、ユーザーによって明示的にアサーションされていない可能性がありますが、代わりにユーザーによって実行されたアサーションによって暗示されます。

于 2012-09-07T19:07:54.413 に答える