问脱节推理
EN

Stack Overflow用户

提问于 2022-09-11 13:42:31

回答 1查看 29关注 0票数 0

达夫尼没有证实这一点：

assert forall p,q,p',q' :: (p==>p' && q==>q') ==> (p||q ==> p'||q') ;

而且，更广泛地说，我很难验证与分离有关的计算。

发布于 2022-09-13 15:34:19

assert forall p,q,p',q' :: ((p==>p') && (q==>q')) ==> (p||q ==> p'||q') ;

不要忘记==>周围的括号，否则您的第二个条件将被视为p ==> ((p' && q) ==> q')

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/73679743

复制

相似问题

问脱节推理EN