clojure.core.logic 中是否有逻辑的 for-all ？

Question

我正在尝试使用 clojure.core.logic 解决 Smullyan 的 To Mock a Mockingbird 中的第一个难题，不是因为它特别难，而是作为一种练习。谜题说有一个花园，有三种颜色的花：红色、黄色和蓝色。每种颜色至少出现一次，无论您采摘哪三朵花，其中都会有一朵红色和一朵黄色。问题：第三个一定是蓝色的吗？
逻辑代码的基本骨架非常简单：

(run 5 [flowers]
   (counto flowers 3)
   (containso flowers [:red :yellow])
   (fresh [garden]
          (containso garden [:red :yellow :blue])
          (containso garden flowers)
          (forall [flower-selection] (...))))

counto 和 containso 是手动实现的，并且做显而易见的事情。我是新手，所以我可能缺少现有的库支持。重要的一行是以forall 开头的那一行。 forall 基本上是我希望存在的，但似乎找不到。我知道的唯一可以在这个地方使用的构造是fresh。但fresh 本质上执行存在量化∃。我这里要的是全称量化∀。
我对一个可以可能选择包含红色和黄色花朵的三朵花的花园不感兴趣。我对一个必然导致这种选择的花园感兴趣。

Answer 1

即使有一个 forall，这种方法也行不通，因为花园可以任意大，并且测试无限花园中三朵花的所有组合将花费无限的时间。

即使你做了那个，你仍然不会完成，因为你只证明了存在一个满足这个属性的花园：你还没有证明所有 满足初始条件的花园也满足属性。

core.logic“只是”一种建模搜索问题的方法，可以轻松修剪搜索空间中无趣的子树。如果您试图证明关于无限搜索空间的通用陈述，则需要以某种方式进行修剪以限制搜索空间的最大大小。对于这个问题，我在 core.logic 中没有看到任何明显的方法，没有对原始问题进行更多思考，这当然会直接导致解决方案，根本不需要 core.logic。