能否让clingo输出生成解决方案所用的事实与规则？

针对提取生成"Yes"（即证明mortal(socrates)成立）所依赖的核心事实与规则、排除无关内容的需求，可通过以下两种方式实现：

方法1：使用Clingo内置的理由提取参数 #

Clingo的--explain与--text参数组合，可直接输出推导特定结论的依赖链，自动过滤无关内容。

操作步骤： #

1. 保留原代码不变：

man(socrates).       % socrates is a man
mortal(X) :- man(X). % all men are mortal

greek(socrates).     % other info not needed for question

% is socrates mortal?
#show.
#show "Yes" : mortal(socrates).

2. 执行命令：

clingo your_file.lp --explain --text

3. 输出结果中会明确展示推导mortal(socrates)的必要依赖：

• 事实：man(socrates).
• 规则：mortal(X) :- man(X).
  无关的greek(socrates).不会出现在推导链中。

方法2：自定义规则标记依赖（更可控） #

通过添加规则显式标记推导目标的依赖，可精准控制输出内容：

修改后的代码： #

man(socrates).       % socrates is a man
mortal(X) :- man(X). % all men are mortal

greek(socrates).     % other info not needed for question

% 标记推导mortal(socrates)所需的事实与规则
depends_on(man(socrates)) :- mortal(socrates).
depends_on(mortal(X) :- man(X)) :- mortal(socrates).

% 展示结果及依赖
#show "Yes" : mortal(socrates).
#show depends_on/1.

运行命令： #

clingo modified_file.lp

输出结果： #

"Yes" depends_on(man(socrates)) depends_on(mortal(_):-man(_))

该结果直接呈现了生成结论的必要事实与规则，自动排除无关内容。

内容的提问来源于stack exchange，提问作者Andy T