答案集编程中的混合量化答案

【问题标题】：Mixed quantification in Answer Set Programming答案集编程中的混合量化
【发布时间】：2017-10-16 09:25:20
【问题描述】：

我希望能够在 ASP/cligo 中制定以下 FOL 语句：

∀ X. prop(X) ⇐ (∃ Y. ∀ V. ∃ A. 
                 (p(Y, V, A) ∧ q(X, V, A))
               )

X 和Y 的域由dom/1 给出。 A 的域由 domA/1 给出。 V 的域是 1..n。

对我来说，问题是混合量化。现在，当然，我可以扩展 ∀ V 并得到如下内容：

prop(X) :- p(Y, 1, A_1), q(X, 1, A_1), domA(A_1),
           p(Y, 2, A_2), q(X, 1, A_2), domA(A_2),
           ...,
           p(Y, n, A_n), q(X, n, A_n), domA(A_n)

           dom(X), dom(Y).

但是当我直到运行时才知道n（我将它作为参数传递给 cligo）时，这并不适用。

有没有办法用 cligo 方便又干净地做到这一点？还是应该改用 Python/Lua 脚本功能？如果有，怎么做？

【问题讨论】：

标签： logic-programming quantifiers first-order-logic answer-set-programming clingo

【解决方案1】：

迟到总比没有好...我可能完全错了，但也许数数可以解决问题：

pq(X,Y,V) :- p(Y, V, A), q(X, V, A), dom(X), dom(Y), V=1..n, domA(A).
allpq(X,Y) :- {pq(X,Y,V):V=1..n} == n, dom(X), dom(Y).
prop(X) :- allpq(X,Y), dom(X), dom(Y).

【讨论】：