问题描述
问题
正式来说，我想知道两者之间的关系
forall I. I ⊧ (f1∧f2∧f3)
和
(forall I. I ⊧ f1) and (forall I. I ⊧ f2) and (forall I. I ⊧ f3)。
如果第二个成立，第一个成立吗？反之亦然？
详情
我想检查一阶逻辑公式 (f1∧f2∧f3) 的有效性，使用 SMT 求解器，将其编码为 is ¬(f1∧f2∧f3) UNSAT?。
但是，这需要很长时间。所以我考虑检查每个公式f1、f2和f3的有效性，将其编码为(is (¬f1) UNSAT) and (is (¬f2) UNSAT) and (is (¬f3) UNSAT)?。这会调用 SMT 求解器 3 次，但如果 SMT 查询之一返回“未知”或“无效”，程序可以更早地转义。
改用这种方法是否安全（且有效）？
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）