Что означают 1 ‹0 и 1 = -1 в clingo / ASP?

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

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

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


answer-set-programming clingo gringo
person user2954167    schedule 21.11.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

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

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

В этой строке говорится

атом истинен, если: «1> 0» И «1‹ 0 »И« 1 = -1 ».

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

Запуск этой строки дает нам результат:

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 противоречат друг другу, поэтому ответ неудовлетворительный.

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

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

person tpreston_it    schedule 10.04.2019