Что означают 1 <0 и 1 = -1 в клинго / ASP? - PullRequest
Новая
       24

Что означают 1 <0 и 1 = -1 в клинго / ASP?

0 голосов
/ 21 ноября 2018

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

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

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

1 Ответ

0 голосов
/ 10 апреля 2019

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

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

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

В этой строке указано, что

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

У меня такое ощущение, что источником путаницы является то, как эта линия интерпретируется.Только первое логическое условие является истинным, а остальные 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 противоречат друг другу, поэтому ответ неудовлетворителен.

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

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

...