Описание тега horn

Вопросы с тегом
2 ответа

Что такое реальное приложение для HORN?

В последнее время я немного слышал о HORN и удивляюсь, какие проблемы он может решить или насколько это полезно в реальной жизни. http://code.google.com/p/hornget/
12 авг '09 в 12:20
2 ответа

Является ли "~A=>B" клаузулой для рога?

Я просто запутался в определении клаузулы о роге. Является ли "~A=>B" клаузулой для рога? Если мы преобразуем его в дизъюнктивные формы, это будет "AvB", который не является клаузулой рога. Поэтому мне интересно, является ли это клаузулой с рогом. Б…
10 дек '13 в 20:35
2 ответа

Проблемы, возникающие при использовании простого скрипта jQuery для захвата одной высоты div и создания другого div такого же размера

В основном я хочу получить высоту .r-side и применить его к высоте .l-side так что эти два элемента всегда имеют одинаковую высоту, даже если размер окна изменен и расположен друг над другом. Я не уверен, что не так с моим JQuery. Вот что я получил:…
08 май '17 в 09:20
1 ответ

CNF против рога удовлетворенности

Я знаю, что легче доказать, выполнима ли формула рога. Мой вопрос: почему с формулой рога легче, чем с обычным CNF?
16 мар '15 в 16:06
4 ответа

Подписание неподписанного собрания

Недавнее обновление NHibernate 2.1 вывело ситуацию с головной болью на поверхность. Похоже, что большинство проектов создаются по умолчанию как подписанные сборки. Например, fluentnhibernate ссылается на ключевой файл fluent.snk. Nhibernate.search с…
03 ноя '09 в 18:12
1 ответ

SVG с прозрачностью

Я стремлюсь создать эффект, подобный тому, который есть в этом коде. Есть SVG с прозрачностью поверх фонового видео. Пока у меня есть документ AI с выбранной формой пути, который я экспортировал из фотошопа. В идеале я хочу, чтобы внутренняя часть п…
22 апр '17 в 23:32
1 ответ

Какие придирки эквивалентны этим положениям?

Я использую Z3 и расширенный синтаксис SMT-LIB2 для решения моих предложений рог. Я знаю, что заголовок предложения рог должен быть неинтерпретируемым предикатом; но мне интересно, как мне переписать следующие пункты, чтобы они были набором предложе…
14 окт '19 в 15:15
0 ответов

Как написать предложение рог с ложным головой в Z3?

Я использую Z3 и расширенный синтаксис SMT-LIB2 для решения моих предложений рог. Заголовок предложения рог должен быть неинтерпретируемым предикатом; но мне интересно, как я могу переписать следующий пункт как пункт рог. (declare-rel p(Int)) (decla…
15 окт '19 в 13:06
1 ответ

Алгоритм Horn SAT с использованием графиков

Для некоторых ограниченных классов логических формул проблема выполнимости может быть эффективно решена за полиномиальное время или даже линейно. Одним из таких классов является класс формул Хорна, которые состоят только из предложений Хорна с не бо…
22 ноя '20 в 15:08
1 ответ

что означает ключевое слово "максимум" в языке SMT-LIB (расширенная версия Z3 FixedPoint)

Как в этом файле ключевое слово "не больше" в правиле: horn1.smt2(из репозитория Z3 github examples/python/data) (declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool)) (declare-rel Invariant (Bool Bool Bool Bool Bool Bool B…
15 ноя '20 в 08:57
1 ответ

Использование Array в логике HORN в Spacer/Z3

Есть ли какой-нибудь способ использовать «неинтерпретируемые функции» (UIF) внутри запросов Horn? Я думаю, вы используете UIF для представления «переменных Хорна», поэтому, возможно, я подумал, что могу подделать то, что хочу, с помощью массивов. Од…
30 мар '23 в 16:16