Getting full Herbrand model of a program

[LukasZahradnik]

Hello,

I would like to ask if it is possible to obtain a full Herbrand Model for my program.

Let's say my program has the following facts:

b(0). d(0). c(1). c(2).

And two simple rules:

a(X) :- b(X).
a(X) :- c(Y), d(X).

From this program (with the keep-facts flag), I'm able to obtain the following grounding:

b(0).
d(0).
c(1).
c(2).
a(0) :- d(0), c(1).

But I would want to get all possible substitutions, i.e.:

b(0).
d(0).
c(1).
c(2).

a(0) :- b(0).
a(0) :- d(0), c(1).
a(0) :- d(0), c(2).

Is there a way to somehow achieve this? I couldn't find anything in the documentation.

Thank you, Lukáš

[rkaminsk]

It's not possible via an option.

You could augment your program a bit by adding additional rules:

{ dom(0..2) }.

a(X) :- dom(X).
b(X) :- dom(X).
c(X) :- dom(X).
d(X) :- dom(X).

{ b(0) }.
{ c(1..2) }.
{ d(0) }.

{ a(X) } :- b(X).
{ a(X) } :- c(Y), d(X).

Note that I also made all heads choices so that gringo does not apply simplifications. Filtering the rules containing dom and stripping the curly braces, we obtain:

➜ gringo test.lp --text | grep -v dom | sed 's/[{}]//g'
d(0).
c(1).
c(2).
a(0):-d(0),c(0).
a(0):-d(0),c(1).
a(0):-d(0),c(2).
a(1):-d(1),c(0).
a(1):-d(1),c(1).
a(1):-d(1),c(2).
a(2):-d(2),c(0).
a(2):-d(2),c(1).
a(2):-d(2),c(2).
b(0).
a(0):-b(0).
a(1):-b(1).
a(2):-b(2).

[LukasZahradnik]

Thank you. Making all heads choices seems to be working.

I didn't understand the reason behind introducing the dom and additional rules. In your example, after the filtering, you will get groundings that shouldn't hold, such as a(1):-d(1),c(0). (there is no d(1)).

[rkaminsk]

I didn't understand the reason behind introducing the dom and additional rules. In your example, after the filtering, you will get groundings that shouldn't hold, such as a(1):-d(1),c(0). (there is no d(1)).

I don't know what a full Herbrand model is. Glad you could get it working for your case.