我试图用clojure.core.logic解决Smullyan的《嘲笑一只知更鸟》中的第一个谜题，不是因为它特别难，而是一种练习。拼图指出，有一个花园，有三种颜色的花：红色、黄色和蓝色。每种颜色至少出现一次，无论您选择哪三朵花，其中都会有红色和黄色。问题：第三个一定是蓝色的吗？
逻辑代码的基本框架非常简单：
(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本质上是在执行存在量化∃。我在这里想要的是通用量化∀.
我对一个花园不感兴趣，因为它可以选择三朵包含红色和黄色的花朵。我对一个必然导致这种选择的花园感兴趣。
即使有一个forall，这种方法也不会真正奏效，因为花园可能是任意大的，并且测试来自无限花园的三朵花的所有组合将花费无限的时间。
即使你这样做了，你仍然不会完成，因为你只是证明了存在一个满足这个属性的花园：你还没有证明所有满足初始条件的花园也满足这个属性。
Core.Logic"只是"一种对搜索问题进行建模的方法，它可以很容易地修剪搜索空间中不感兴趣的子树。如果你试图证明一个关于无限搜索空间的通用陈述，你需要以某种方式修剪，以限制搜索空间的最大大小。对于这个问题，我没有看到任何明显的方法可以在core.logic中做到这一点，除了更多地考虑原始问题，这当然会直接导致解决方案，根本不需要core.logic。