Is it possible for clingo to output which facts/rules are used in generating a solution?

Question

Is it possible for clingo to output which facts/rules are used in generating a solution?

As an simple example, the following code can be used to show that Socrates is mortal:

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

Which produces:

clingo version 5.6.2 (d469780)
Reading from test.cl
Solving...
Answer: 1
"Yes"
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

Is it possible to also get access to the facts/rules which were used in finding the "Yes" solution e.g. mortal(X) :- man(X). and man(socrates). (but not greek(socrates). and any other facts/rules which may have been specified but not needed for the found solution).

EDIT: I know if I omit the #show and add is_socrates_mortal :- mortal(socrates). It produces the whole answer set e.g. man(socrates) mortal(socrates) is_socrates_mortal greek(socrates). But in that case it also gives greek(socrates) which isn't needed for the ordinal question "is socrates mortal?".

I'd like to get access to specifically the facts/rules needed in producing a given solution.

Answer 1

If anyone else comes across this.

There is a project called xclingo2 which does what I was after:

https://github.com/bramucas/xclingo2

For the input:

%!trace_rule {"socrates is a man"}
man(socrates).

%!trace_rule {"All men are mortal"}
mortal(X) :- man(X). 

%!trace_rule {"socrates is greek"}
greek(socrates).


%!show_trace mortal(socrates).

I get:

Answer 1
  *
  |__All men are mortal
  |  |__socrates is a man

Answer 2

Clingo, which is part of the ASP (Answer Set Programming) system, typically provides the set of rules and facts that are used in generating a solution. In ASP, a solution corresponds to an answer set, which is a consistent set of literals that satisfies the rules and constraints specified in the program.

When you run Clingo, it usually outputs the answer sets along with the rules