答案集编程中的混合量化

Question

我希望能够在ASP/clingo中表述以下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时，这并不有效（我将其作为参数传递给 clingo）。

有没有办法用粘着方便干净地做到这一点？或者我应该改用 Python/Lua 脚本功能？如果是这样，如何？

Answer 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).