clojure - 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。