在clojure.core.logic中是否有一个合乎逻辑的for-all？

Question

我试图解决Smullyan的第一个难题，用clojure.core.logic模拟一只知更鸟，不是因为它特别困难，而是因为它是一个练习。这个难题表明，有一个花园有三种颜色的花朵：红色，黄色和蓝色。每种颜色至少出现一次，无论你选择哪种花，都会出现红色和黄色。问题：第三是必然的蓝色？
的逻辑代码的基本骨架是相当简单：

(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开头的那一行。基本上我希望会存在，但似乎无法找到。我知道的唯一结构可以在这个地方去fresh。但是fresh本质上执行存在量化∃。我想要的是普遍量化∀。
我对花园不感兴趣，它是可能选择包含红色和黄色的三朵花。我对花园感兴趣，必然导致这样的选择。

Answer 1

即使存在一个问题，这种方法并不真正起作用，因为花园可以是任意大的，并且测试无限花园中的三朵花的所有组合将需要无限的时间。

而且即使你没有是，你仍然无法做到的，因为你只证明了存在着一个花园，满足这个属性：你有没有证明其满足初始所有花园条件也满足财产。

core.logic“只是”一种建模搜索问题的方法，可以轻松修剪搜索空间中不感兴趣的子树。如果您试图证明一个关于无限搜索空间的普遍陈述，那么您将需要以某种方式修剪，以限制搜索空间的最大大小。在core.logic中，我看不出有什么明显的方式来解决这个问题，而不是更多地考虑原始问题，这当然会直接导致解决方案，根本不需要core.logic。