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