Я должен сказать, что это крутая проблема.
Я вижу два фундаментальных подхода, в которых вы используете пролог read_term/2, чтобы получить термин вместе с именами переменных, использованными в этом термине, который будет выглядеть примерно так:
?- read_term(T, [variable_names(Names)]).
|: X and Y or Z and Q.
T = _5700 and _5702 or _5706 and _5708,
Names = ['X'=_5700, 'Y'=_5702, 'Z'=_5706, 'Q'=_5708].
Думая об этом, казалось, что это будет больше проблем, чем это стоило бы для меня, поэтому я подумал, что проиллюстрирую "более простую" версию, где у нас на самом деле нет переменных, только атомы и отдельный список значений переменных. Вы, вероятно, могли бы адаптировать тот, что ниже, к тому, что выше, без огромного количества работы, хотя это просто не казалось необходимым для решения проблемы.
Сначала нам нужно поддержать этих операторов:
:- op(500, yfx, or).
:- op(400, yfx, and).
Я пошел дальше и дал им тот же приоритет, что и + и * соответственно, что мне показалось интуитивно понятным.
У меня будет список переменных и присваиваний, например [x=true, y=false]. Я создал предикат, чтобы справиться с этим, но в конце концов подумал, что лучше, и удалил его, но отметим, что мы приняли это решение здесь.
Теперь я планирую создать оценочный предикат, который будет принимать выражение и присваивание значения переменной. Это собирается произвести логическое значение для предоставленного выражения и «причины». Я собираюсь обмануть здесь и использовать оператор «is», но я делаю это только потому, что он мне приятен. Самый основной вид термина
evaluate(X, Assignments, Value, X is Value) :-
atom(X), memberchk(X=Value, Assignments).
Так что теперь мы можем поддерживать выражения типа x:
?- evaluate(x, [x=true], V, R).
V = true,
R = (x is true).
?- evaluate(x, [x=false], V, R).
V = false,
R = (x is false).
Это что-то вроде тавтологии; если x = true, то выражение «x» является истинным, потому что x = true. Аналогично для ложного. Но у нас есть причина, к которой вы стремитесь. Так что давайте разберемся "или" дальше:
evaluate(X or _, Assignments, true, Reason) :-
evaluate(X, Assignments, true, Reason).
evaluate(_ or Y, Assignments, true, Reason) :-
evaluate(Y, Assignments, true, Reason).
Итак, теперь мы должны обработать случай, когда одно из двух истинно:
?- evaluate(x or y, [x=true,y=false], V, R).
V = true,
R = (x is true) ;
false.
?- evaluate(x or y, [x=false,y=true], V, R).
V = true,
R = (y is true) ;
false.
Если мы дадим ему x = true и y = true, мы получим два решения: одно для x и одно для y. Но нам нужно еще одно правило для ложного случая:
evaluate(X or Y, Assignments, false, R1 and R2) :-
evaluate(X, Assignments, false, R1),
evaluate(Y, Assignments, false, R2).
Таким образом, идея состоит в том, чтобы заметить, что обе стороны "или" ложны, а затем объединить причины с "и". Таким образом, мы получаем это:
?- evaluate(x or y, [x=false,y=false], V, R).
V = false,
R = (x is false)and(y is false).
Поскольку мы делегируем стороны, теперь мы можем видеть, что большие и сложные последовательности "или" должны работать:
?- evaluate(a or b or c or d or e, [a=false,b=false,c=false,d=true,e=false], V, R).
V = true,
R = (d is true) ;
false.
Вы можете экстраполировать то, что мы сделали для "или" для "и", где у нас в основном два ложных случая и один истинный случай вместо двух истинных случаев и один ложный случай:
evaluate(X and Y, Assignments, true, R1 and R2) :-
evaluate(X, Assignments, true, R1),
evaluate(Y, Assignments, true, R2).
evaluate(X and _, Assignments, false, Reason) :-
evaluate(X, Assignments, false, Reason).
evaluate(_ and Y, Assignments, false, Reason) :-
evaluate(Y, Assignments, false, Reason).
Это работает для некоторых интересных случаев, которые вы можете ожидать:
?- evaluate(x and y or z, [x=true, y=true, z=false], V, R).
V = true,
R = (x is true)and(y is true) ;
false.
?- evaluate(x and y or z, [x=false, y=false, z=true], V, R).
V = true,
R = (z is true) ;
false.
В некоторых ситуациях это бесполезно, например:
?- evaluate((a or b) and (a or c), [a=true,b=false,c=false], V, R).
V = true,
R = (a is true)and(a is true) ;
false.
Как видите, первое решение не суперинформативно, потому что мы уже говорили что-то о a; возможно, мы могли бы найти способ упростить ответ, комбинируя ответы детей более разумно. С другой стороны, это несколько более полезно в этом случае:
?- evaluate((a or b) and (a or c), [a=false,b=false,c=false], V, R).
V = false,
R = (a is false)and(b is false) ;
V = false,
R = (a is false)and(c is false).
?- evaluate((a or b) and (a or c), [a=false,b=true,c=true], V, R).
V = true,
R = (b is true)and(c is true) ;
false.
Редактировать: обработка неопределенных значений
Единственный элемент, который действительно необходимо изменить для обработки неопределенных значений, - это ветвь atom(X), которая должна быть заменена на эту:
evaluate(X, Assignments, Value, X is Value) :-
atom(X),
( memberchk(X=V, Assignments) ->
Value = V
; member(Value, [true,false])
).
Когда в списке привязок появится a=false, он будет использован; если он не появляется, то будут сгенерированы и a=false, и a=true. Это, кажется, покрывает другие ваши случаи использования, начиная с полностью общего:
?- evaluate((a or b) and (a or c), [a=false], V, Reason).
V = true,
Reason = (b is true)and(c is true) ;
V = false,
Reason = (a is false)and(b is false) ;
V = false,
Reason = (a is false)and(c is false).
И вы можете ограничить поиск случаями, которые дают интересующее вас значение:
?- evaluate((a or b) and (a or c), [a=false], false, Reason).
Reason = (a is false)and(b is false) ;
Reason = (a is false)and(c is false).
Конечно, Пролог здесь не делает ничего особенно умного; он не пытается работать в обратном направлении, чтобы выяснить, какие значения b и c приведут к ложному, он просто генерирует все возможности и пытается объединить их оценку с false. Таким образом, каждая неопределенная переменная, которую вы добавляете в выражение, удваивает пространство поиска. Если это неэффективность, о которой вы беспокоитесь, возможно, это не идеальное решение для вас (или, может быть, вам стоит попробовать и посмотреть, терпимо ли это).
Я думаю, что вы, возможно, захотите заглянуть в SAT-решатели, если ваша главная задача - производительность, хотя я не знаю, насколько они способны дать вам «причины» для своих выводов.