Пролог булево уравнение решить

Question

Я получил эту программу для работы до сих пор в пролог GNU

not(X) :- \+ X.  
and(X, Y):-  X , Y.  
or(X, Y):-   X ; Y. 
implies(X, Y):- \+ X ; Y.  

p.
q.

:- initialization(main).

main :- 
    write('Program start'), nl.

Вы можете ввести и (p, q), и получить да, а также и (p, не (q)) и получить нет. Теперь я хотел бы сделать что-то вроде этого:

Я установил p в true, (инициализируя его с помощью p.) И (и (p, q)) в true (но без инициализации q), и я хочу, чтобы пролог сказал: существует одно решение: "q" должно быть истинным

Если я установил p и (или (p, q)) в true, я хочу, чтобы пролог сказал: существует два решения, "q" может быть истинным или ложным. Какой лучший способ сделать это?

Answer 1

Рассмотрите возможность использования системы Prolog с булевым решателем ограничений. Например, в SICStus и SWI-Prolog:

?- use_module(library(clpb)).
true.

?- P = 1, sat(P * Q).
P = Q, Q = 1.

?- P = 1, sat_count(P + Q, Count).
Count = 2,
P = 1.

?- P = 1, sat(P + Q), labeling([P,Q]).
P = 1,
Q = 0 ;
P = Q, Q = 1.

Вы также можете использовать конечный доменный ограничитель GNU Prolog, поскольку логические значения являются частным случаем целых чисел.

Answer 2

Я предлагаю вам использовать переменные вместо p а также q и обернуть его в некоторый термин, например

and(prop(P),prop(Q))

Кроме того, я бы реализовал два предиката, один для решения истинных утверждений, один для решения ложных утверждений. С помощью \+ это неправильный подход, так как он не позволяет связывать переменные. Вот немного примера кода:

formula_true(prop(true)).
formula_true(and(A,B)) :- formula_true(A),formula_true(B).
formula_true(not(A)) :- formula_false(A).
...

formula_false(prop(false)).
formula_false(and(A,B)) :- formula_false(A);formula_false(B).
...

Ваш пример запроса будет тогда:

P=true,formula_true(and(prop(P),prop(Q))).

И, может быть, у вас есть лучшее имя, чем formula_true соответственно formula_false,:)

Если у вас есть логический решатель ограничений, это, конечно, будет более эффективным.