What do 1<0 and 1=-1 mean in clingo/ASP?

Question

I have never used clingo before, and I find the online documentation incomplete (I also can't post to the Potassco forums). I have a piece of clingo code with lines of rules of the format

foo(L1, L2, L3) :- isa(thing,object), isa(thing, object)...

That part of the code makes sense, but at the end of the line before the final rule, I have the conditions either 1>0, 1<0, or 1==-1. I'm not sure what they mean, because they don't seem to follow normal boolean rules. Does anyone know what this means specifically in clingo?

Answer 1

Assuming that you're using Clingo 5, the conditions should resolve just like normal boolean conditions.

As you've not posted the exact line, I can only assume it's a line of the form:

atom :- 1 > 0, 1 < 0, 1 = -1. 

This line says

atom is true if: "1 > 0" AND "1 < 0" AND "1 = -1".

I have a feeling that the source of the confusion is the way this line is interpreted. Only the first boolean condition is true, and the other 2 are false. This does not mean that atom is false though: it just means that there is no evidence that atom is true.

Running this line gives us the output:

Answer: 1

SATISFIABLE

Because there is no evidence proving that atom is true.

This means we could have a program like this:

atom :- 1 > 0, 1 < 0, 1 = -1.
atom :- 1 = 1.

And it will have the answer:

Answer: 1
atom
SATISFIABLE

The second line provides evidence that atom is true, and the first line provides no evidence that atom is true. Therefore, atom is true and the answer is satisfiable. There are no contradictions.

In this program:

atom :- 1 > 0, 1 < 0, 1 = -1.
atom :- 1 = 0.

We get the answer:

Answer: 1

SATISFIABLE

Because neither line provides evidence that atom is true. There are no contradictions, so the answer is satisfied, but an atom is only proven true when there is evidence that it is true.

In this program:

atom :- 1 > 0, 1 < 0, 1 = -1.
:- atom.

We get the answer:

Answer: 1

SATISFIABLE

The first line still provides no evidence that atom is true, but the second line proves that it is false. As the lines don't contradict, we once again have an empty but satisfied answer.

And finally, we have the program:

atom :- 1 > 0, 1 < 0, 1 = -1.
atom :- 1 = 1.
:- atom.

Which has the answer:

UNSATISFIABLE

Line 1 gives no evidence that atom is true, line 2 proves that atom is true, and line 3 proves that atom is false. Lines 2 and 3 contradict, so the answer is unsatisfied.

Obviously I can't tell you any specifics without being given the actual line, but booleans do resolve in the same way that they do in conventional programming languages.

I hope this helps!