如何解决可以通过收集子公式的有效性来决定公式的有效性吗？
问题
正式来说，我想知道两者之间的关系
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 举报，一经查实，本站将立刻删除。
