Подскажите библиотеку (C)
а зачем тут С?
Затем, что требуется для решения другой задачи.
Подскажи хотя бы ссылки на алгоритмы, если знаешь.
Подскажи хотя бы ссылки на алгоритмы, если знаешь.
может что-нибудь вроде такого(только там C++)?
http://www.amzi.com/articles/prolog_cpp.htm
я не читал что там конкретно, но идея - поискать C-шные backend-ы к прологу.
http://www.amzi.com/articles/prolog_cpp.htm
я не читал что там конкретно, но идея - поискать C-шные backend-ы к прологу.
Идея понятна, спасибо. Но в реальности все немного сложнее — реализовать надо не просто вывод формул в булевой логике, а скорее в логике первого порядка. У меня в качестве булевых переменных выступают предикаты — линейные уравнения и неравенства. И как минимум надо замещать симплекс-методом, где это возможно, тупой логический вывод.
В основе пролога и так лежит логика первого порядка.
С помощью него скорее всего можно решить твою задачу "проверки истинности и определения наборов значений переменных, на которых формула истинна".
Хотя реально я им не пользовался, так что могу и ошибаться.
А вот на счет преобразования формул - совсем х.з.
С помощью него скорее всего можно решить твою задачу "проверки истинности и определения наборов значений переменных, на которых формула истинна".
Хотя реально я им не пользовался, так что могу и ошибаться.
А вот на счет преобразования формул - совсем х.з.
Если у тебя есть предикаты - то какая для них интерпретация используется ?
Если интерпретация любая - то тебе нужно пролог реализовать
Если интерпретация любая - то тебе нужно пролог реализовать
Если у тебя есть предикаты - то какая для них интерпретация используется ?Я вроде написал про предикаты: это линейные уравнения и неравенства. В том-то и дело, что надо учитывать их семантику, причем умным споcобом, например, если формула имеет вид
x <= 9 && y <= 9 && 10*x + y >= 100
надо пользоваться соображениями линейной алгебры.
С другой стороны, формула может выглядеть как-то так:
y == 0 && x <= 9) || (y == 1 && x >= 10 && z + x == 100 && y >= 1) || y == 1)
Тогда надо как-то еще упрощать, например, получить, что y == 1 и отбросить тождественно ложный кусок первой конъюнкции.
Это называется linear arithmetic. Ищи запросами типа "linear arithmetic solver".
О, клева 
Спасибо, кажись че-то интересное нашел.
Спасибо, кажись че-то интересное нашел.
Блин у тебя предикатов то всего три: <, <=, = и то они бинарные. А если совсем точно - то два: < и = 
писал бы подробнее
писал бы подробнее
Ну и что ? Думаешь от этого легче ?
Вот подробнее:
Рассматривается следующий класс формул от вещественных (для простоты) переменных x, y, z, ...
Термами являются линейные комбинации переменных с вещественными коэффициентами со свободным членом.
Атомарные предикаты: >=, <=, ==, !=
Булевы связки: конъюнкция и дизъюнкция.
Нужно придумать (эффективный) алгоритм определения выполнимости формулы.
Неэффективный алгоритм: это преобразовывать все формулы к виду ДНФ, то есть к набору систем линейных неравенств. Каждую систему исследовать симплекс-методом на предмет наличия решения.
Вот подробнее:
Рассматривается следующий класс формул от вещественных (для простоты) переменных x, y, z, ...
Термами являются линейные комбинации переменных с вещественными коэффициентами со свободным членом.
Атомарные предикаты: >=, <=, ==, !=
Булевы связки: конъюнкция и дизъюнкция.
Нужно придумать (эффективный) алгоритм определения выполнимости формулы.
Неэффективный алгоритм: это преобразовывать все формулы к виду ДНФ, то есть к набору систем линейных неравенств. Каждую систему исследовать симплекс-методом на предмет наличия решения.
Оставить комментарий
Oper
для работы с булевыми формулами, если такая имеется.Что мне требуется:
* преобразование булевых формул из одного вида в другой;
* проверка истинности и определение наборов значений переменных, на которых формула истинна.
Или надо писать свою ?