Что означают уравнения с 1 и 0 в клинго?

Question

Я никогда не использовал clingo раньше, и я нахожу онлайн-документацию неполной (я также не могу публиковать сообщения на форумах Potassco). У меня есть кусок кода клинго со строками правил формата

foo(L1, L2, L3):- isa(вещь, объект), isa(вещь, объект)...

Эта часть кода имеет смысл, но в конце строки перед последним правилом у меня есть условия: 1>0, 1<0 или 1==-1. Я не уверен, что они имеют в виду, потому что они не следуют нормальным логическим правилам. Кто-нибудь знает, что это значит конкретно в клинго?

Answer 1

Предполагая, что вы используете Clingo 5, условия должны разрешаться так же, как и обычные логические условия.

Поскольку вы не указали точную строку, я могу только предположить, что это строка вида:

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

Эта строка говорит

атом истина, если: "1 > 0" И "1 < 0" И "1 = -1".

У меня есть ощущение, что источником путаницы является то, как эта линия интерпретируется. Только первое логическое условие является истинным, а остальные 2 ложными. Это не означает, что атом является ложным: это просто означает, что нет никаких доказательств того, что атом является истинным.

Запуск этой строки дает нам вывод:

Answer: 1

SATISFIABLE

Потому что нет никаких доказательств того, что атом истинен.

Это означает, что у нас может быть такая программа:

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

И это будет иметь ответ:

Answer: 1
atom
SATISFIABLE

Вторая строка обеспечивает доказательство того, что атом является истинным, а первая строка не предоставляет никаких доказательств того, что атом является истинным. Следовательно, атом верен и ответ удовлетворителен. Здесь нет противоречий.

В этой программе:

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

Мы получаем ответ:

Answer: 1

SATISFIABLE

Потому что ни одна из линий не дает доказательств того, что атом верен. Противоречий нет, поэтому ответ удовлетворен, но атом подтверждается только тогда, когда есть доказательства, что это правда.

В этой программе:

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

Мы получаем ответ:

Answer: 1

SATISFIABLE

Первая строка до сих пор не дает никаких доказательств того, что атом истинен, но вторая строка доказывает, что он ложен. Поскольку строки не противоречат, у нас снова есть пустой, но удовлетворенный ответ.

И наконец, у нас есть программа:

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

Который имеет ответ:

UNSATISFIABLE

Строка 1 не дает доказательств того, что атом истинен, строка 2 доказывает, что атом истинен, а строка 3 доказывает, что атом ложен. Строки 2 и 3 противоречат, поэтому ответ неудовлетворен.

Очевидно, что я не могу рассказать вам какие-либо подробности без указания фактической строки, но логические значения разрешаются так же, как и в обычных языках программирования.

Надеюсь, это поможет!