logic-programming - 为什么析取 ASP 程序不能在答案中返回两个析取谓词实例？

Question

我是 ASP（答案集编程）的新手。

我在cligo在线版中尝试了以下程序（推理模式=枚举全部）

% instance
member(dave).

% encoding
edu(X);rich(X) :- member(X).

它返回：

Answer: 1
member(dave) rich(dave)
Answer: 2
member(dave) edu(dave)
SATISFIABLE

但是为什么没有“答案：3”？就像是：

Answer: 3
member(dave) edu(dave) rich(dave)

这个答案也满足规则edu(X);rich(X) :- member(X).。

从逻辑的角度来看，

edu(X);rich(X) :- member(X).

方法

member(X) -> edu(X) ∨ rich(X)

所以应该有另一个答案，edu(X)和 rich(X) 都是真的。

顺便说一句，如果我手动添加关于查理的两个事实：

% instance
member(charlie).
rich(charlie).
edu(charlie).

% encoding
edu(X);rich(X) :- member(X).

然后它按预期返回正确答案：

Answer: 1
member(charlie) edu(charlie) rich(charlie)
SATISFIABLE

很感谢！

---

一些背景资料：

我有这个问题，因为我正在比较传统的逻辑编程（例如 Prolog）与答案集编程（例如 cligo），尽管它们使用不同的理论框架。

clgo 中形式的析取程序：

a_1 ∨ a_2 ... ∨ a_n <- body

无法在 Prolog 中表示。

一个相关问题，请参阅在序言语句的 HEAD 中使用 And 子句

标签： logic-programminganswer-set-programmingclingo

Answer 1

看来我们可以用Choice Rule的形式来表示clgo中的逻辑析取语义。

示例 1：

% instance
member(dave).

% encoding
1 {edu(X);rich(X)} :- member(X).

返回

Answer: 1
member(dave) edu(dave)
Answer: 2
member(dave) rich(dave)
Answer: 3
member(dave) rich(dave) edu(dave)
SATISFIABLE

示例 2：

% instance
member(dave).
member(charlie).
rich(charlie).
edu(charlie).

% encoding
1 {edu(X);rich(X)} :- member(X).

返回

Answer: 1
edu(charlie) rich(charlie) member(dave) member(charlie) edu(dave)
Answer: 2
edu(charlie) rich(charlie) member(dave) member(charlie) rich(dave)
Answer: 3
edu(charlie) rich(charlie) member(dave) member(charlie) rich(dave) edu(dave)
SATISFIABLE

它按预期工作，尽管我不知道它在语义上是否正确。