Пролог: показать таблицу истинности для произвольного выражения, используя is / 2 для некоторых подвыражений

Question

Предположим, у меня есть выражения, которые выглядят как a /\ b \/ c. Я хотел бы создать таблицу истинности для этого, что-то вроде:

 a |  b |  c | a /\ b \/ c
---+----+----+-------------+-
 F |  F |  F | F
 F |  F |  T | T
 F |  T |  F | F
 F |  T |  T | T
 T |  F |  F | F
 T |  F |  T | T
 T |  T |  F | T
 T |  T |  T | T

Ключевой идеей здесь является обработка операторов, которые еще не обработаны is/2, таких как логическое значение ->. Кстати, этот вопрос выводится из сообщения пользователя reddit u / emergenviousts .

Код, который у меня есть для этого, следующий:

bool(0).
bool(1).

negate(1, 0).
negate(0, 1).

eval(Assignments, A, V) :- atom(A), memberchk(A=V, Assignments).
eval(Assignments, \+ E, V) :- eval(Assignments, E, NotV), negate(NotV, V).
eval(Assignments, E1 /\ E2, V) :-
    eval(Assignments, E1, V1),
    eval(Assignments, E2, V2),
    V is V1 /\ V2.
eval(Assignments, E1 \/ E2, V) :-
    eval(Assignments, E1, V1),
    eval(Assignments, E2, V2),
    V is V1 \/ V2.
eval(Assignments, E1 -> E2, V) :-
    eval(Assignments, E1, V1),
    V1 = 1 -> eval(Assignments, E2, V) ; V = 1.

generate_assignment(Variable, Variable=B) :- bool(B).
generate_assignments(Variables, Assignments) :-
    maplist(generate_assignment, Variables, Assignments).

atoms_of_expr(A, A) :- atom(A).
atoms_of_expr(\+ E, A) :- atoms_of_expr(E, A).
atoms_of_expr(E1 /\ E2, A) :- atoms_of_expr(E1, A) ; atoms_of_expr(E2, A).
atoms_of_expr(E1 \/ E2, A) :- atoms_of_expr(E1, A) ; atoms_of_expr(E2, A).
atoms_of_expr(E1 -> E2, A) :- atoms_of_expr(E1, A) ; atoms_of_expr(E2, A).

table_for(E) :-
    setof(A, atoms_of_expr(E, A), Variables),
    write_header(Variables, E),
    write_separator(Variables, E),
    table_rest(Variables, E).

table_rest(Variables, E) :-    
    generate_assignments(Variables, Assignments),
    eval(Assignments, E, Value),
    write_assignments(Assignments, Value),
    fail.
table_rest(_, _) :- true.

write_header([Var|Rest], E) :- 
    write(' '), write(Var), write(' | '), write_header(Rest, E).
write_header([], E) :- writeln(E).

write_separator([_|R], E) :- write('---+-'), write_separator(R, E).
write_separator([], _) :- write('-+-'), nl.

write_assignments([_=Var|Rest], Value) :-
    write(' '), write(Var), write(' | '), write_assignments(Rest, Value).
write_assignments([], Value) :- writeln(Value).

Этот код выводит немного хуже, чем хотелось бы, но я не хотел утомлять вас большим количеством форматирования:

?- table_for(a/\b\/c).
 a |  b |  c | a/\b\/c
---+----+----+--+-
 0 |  0 |  0 | 0
 0 |  0 |  1 | 1
 0 |  1 |  0 | 0
 0 |  1 |  1 | 1
 1 |  0 |  0 | 0
 1 |  0 |  1 | 1
 1 |  1 |  0 | 1
 1 |  1 |  1 | 1
true.    

Я полагаю, что это решение довольно простое, и мне оно нравится, но я часто удивляюсь в Прологе тем, что могут сделать настоящие волшебники, поэтому я подумал, что мне нужно будет внести существенные улучшения. atoms_of_expr/2 немного похоже на шаблон, поскольку дублирует обход в eval/3. Я не видел способа использовать term_variables/2 вместо этого, потому что тогда я не думаю, что смог бы на самом деле предоставить имена переменных или правильно связать их с memberchk/2. Я ошибаюсь?

Answer 1

Следующее не совсем то, что буквально требуется в этой задаче. Тем не менее, я хочу показать, как выгодно оставаться в подмножестве pure при рассуждении о таких задачах, и поэтому я сосредоточен на этом аспекте.

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

eval(v(V), V)       :- V in 0..1.
eval(\+ E0, V)      :- eval(E0, V0), V #= 1 - V0.
eval(E1 /\ E2, V)   :- eval(E1, V1), eval(E2, V2), V #<==> V1 #/\ V2.
eval(E1 \/ E2, V)   :- eval(E1, V1), eval(E2, V2), V #<==> V1 #\/ V2.
eval((E1 -> E2), V) :- eval(E1, V1), eval(E2, V2), V #<==> (V1 #==> V2).

При этом используются целочисленные ограничения для максимально возможного делегирования движку Prolog. См. clpfd для получения дополнительной информации. Если ваша система Prolog поддерживает их, вы также можете использовать ограничения clpb в качестве альтернативы. Обратите внимание, что мы работаем над фактическими переменными Prolog вместо , преобразуя переменные и их связывающую среду в Prolog.

Обратите внимание, что я использую так называемое чистое представление, различая переменные по уникальному (произвольному) главному функтору v/1. Это делает предикат пригодным для индексации аргументов и в то же время сохраняет его общность. Это не совсем (но почти!) Предполагаемый формат ввода. Тем не менее, легко преобразовать предполагаемый формат ввода в такое чистое представление, и я оставляю эту часть как вызов.

В качестве небольшой дополнительной отметки обратите внимание на квадратные скобки в (E1->E2). Причина для них:

<b>6.3.3.1 Arguments</b>

An argument (represented by arg in the syntax rules)
occurs as the argument of a compound term or element of
a list. It can be an atom which is an operator, <b>or a term
with priority not greater than 999</b>. ...

Таким образом, исключение скобок не соответствует синтаксису и не будет работать, например, в GNU Prolog.

И теперь мы уже почти уже закончили, потому что теперь мы можем использовать встроенные механизмы Пролога для рассуждения о таких формулах и включенных в них переменных. Особенно полезны term_variables/2 и опции variable_names/1 для чтения и записи.

Ниже приведена нечистая часть, которая выполняет чтение и печать:

run :-
        read_term(Formula, [variable_names(VNs)]),
        term_variables(Formula, Vs),
        maplist(write_variable(VNs), Vs),
        write_term(Formula, [variable_names(VNs)]),
        nl,
        eval(Formula, Value),
        label(Vs),
        maplist(write_variable(VNs), Vs),
        format("~w\n", [Value]),
        false.

write_variable(VNs, V) :-
        write_term(V, [variable_names(VNs)]),
        format(" |  ", []).

Пример использования:

?- run.
<b>|: v(A)/\v(B)\/v(C).</b>
A |  B |  C |  v(A)/\v(B)\/v(C)
0 |  0 |  0 |  0
0 |  0 |  1 |  1
0 |  1 |  0 |  0
0 |  1 |  1 |  1
1 |  0 |  0 |  0
1 |  0 |  1 |  1
1 |  1 |  0 |  1
1 |  1 |  1 |  1
false.

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

Например:

<b>?- eval(Formula, 0).</b>
Formula = v(0) ;
Formula =  (\+v(1)) ;
Formula =  (\+ \+v(0)) ;
Formula =  (\+ \+ \+v(1)) ;
Formula =  (\+ \+ \+ \+v(0)) ;
etc.

Это может быть не особенно полезным, но это лучше, чем ничего вообще. В частности, он иллюстрирует, что «eval» является , а не хорошим названием для этого отношения, потому что «eval» является императивом и предлагает только один возможный режим использования, тогда как на самом деле это отношение можно использовать и в других направлениях! Я оставляю в поисках лучшего, более декларативного имени.

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

Answer 2

Хм. Я не уверен, что понимаю вопрос и комментарии, но, возможно, у меня есть, чем поделиться. Мне очень очень жаль: это не тот код, который я написал, но я помню, что нашел его, когда впервые где-то занимался логикой в ​​школе, и мне очень жаль, но я не помню, где я его нашел. Я также немного изменил это, потому что это было не очень хорошо, прежде чем я нашел это. Но если кто-то узнает этот код , пожалуйста, , скажите мне, и я снимаю его или приписываю реальному автору кода.

Итак, вот код, который у меня был. Я назвал это загадочно lc.pl, потому что 2 буквы - только больше чем одна буква, но меньше, чем любое другое число. Я не знаю, что означает «с». «Я» означает логику, я надеюсь.

:- module(lc, [
        bl/2,
        valid/1,
        contradiction/1,
        lequiv/2,
        truth_table/2,
        op(100, fy, ?),
        op(200, fy, ~),
        op(500, yfx, and),
        op(500, yfx, or),
        op(690, yfx, =>),
        op(700, yfx, <=>)]).

truth_table(F, T) :-
        term_variables(F, Vs),
        bagof(R-Vs, bl(F, R), T).

valid(F) :-
        forall(bl(F, R), R == t).

contradiction(F) :-
        forall(bl(F, R), R == f).

lequiv(F, G) :-
        forall(( bl(F, X), bl(G, Y) ), X == Y).

bl(?X, R) :-
        v(X, R).
bl(~X, R) :-
        bl(X, R0),
        not(R0, R).
bl(X and Y, R) :-
        bl(X, R0),
        and_bl(R0, Y, R).
bl(X or Y, R) :-
        bl(X, R0),
        or_bl(R0, Y, R).
bl(X => Y, R) :-
        bl(X, R0),
        impl_bl(R0, Y, R).
bl(X <=> Y, R) :-
        bl(X, R0),
        bl(Y, R1),
        eq(R0, R1, R).
bl(X xor Y, R) :-
        bl(X, R0),
        bl(Y, R1),
        xor(R0, R1, R).

v(f, f).
v(t, t).

not(t, f).
not(f, t).

and_bl(f, _, f).
and_bl(t, Y, R) :- bl(Y, R).

or_bl(f, Y, R) :- bl(Y, R).
or_bl(t, _, t).

impl_bl(t, Y, R) :- bl(Y, R).
impl_bl(f, _, t).

eq(f, Y, R) :- not(Y, R).
eq(t, Y, Y).

xor(f, Y, Y).
xor(t, Y, R) :- not(Y, R).

Извините за длинный код: - (

Вы видите term_variables/2, но вы не видите atoms_of_expr, потому что он не использует атомы, потому что зачем использовать атомы, когда переменные легче использовать? Я не знаю.

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

?- truth_table(?A and ?B or ?C, Table).
Table = [f-[f, _3722, f], t-[f, _3692, t], f-[t, f, f], t-[t, f, t], t-[t, t, _3608]].

Так что, очевидно, нет README, но если вы хотите "логическую переменную", а не "логическую переменную", вам нужно написать? Infront, чтобы сделать его "логическим". Зачем ? Я не знаю. После долгих проб и ошибок я обнаружил, что должен написать? перед переменной, чтобы сделать его логическим; много кода, который не заканчивается, если вы забыли написать? перед переменной: - (

Но это имеет смысл и эквивалентность в списке операторов. Вы видите, что таблица истинности в решении сильно отличается, но на самом деле такая же.