ViewProver(20190825)

1. vcirc003.cnf このcnfでは、VPOW()とVWIRE()のテストが必須になっている。

[x,y,z,w].[+DC(x,y,z,w),-VPOW(z),-VWIRE(w),-KC(x,y,z,w)]

たとえばバッテリが空なら、ランプがつかない理由はそれだと結論づけそうだが 両方確認することは論理的に正しい。

しかし、これはswitchとlampの関係が決まった時のテストしかできない。 もっと柔軟にできないか?