查找逻辑公式的一致分配

Question

我即将在Prolog中实现逻辑术语的证明者.我当前的代码并不是真的可以呈现,因此,我只是说,我想要我的程序做什么,希望你可以给我一些很好的建议:)

它应该采用变量列表(也就是说逻辑参数),其次是包含这些参数的逻辑公式(例如'not'(A 'and' B) 'or' 'not'(B 'and' C) 'or' ...,依此类推).

作为输出,我希望我的程序能够以可能的一致性分配进行响应.单个参数可以是true(1)或false(0).

所以我的目标是回归A=0, B=0, C=0 ; A=1等等.

我很高兴有关我的计划的每一个帮助:)

Answer 1

有几种方法可以解决这个问题.在语法方面很方便的一种方法是定义运算符,如下所示:

:- op(500, fx, not).
:- op(600, xfx, and).
:- op(700, xfx, or).

(我只是在这里猜测合理的优先级设置,但仅用于说明.有关详细信息,请参阅op文档.)

完成后,您可以编写一个表达式,例如:A and B和Prolog会"看到"它and(A, B):

| ?- write_canonical(A and B).
and(_23,_24)

从那里,您需要有一种方法来评估表达式.在这方面有很多关于SO的问题(在这个网站上搜索[prolog] boolean expression evaluation),但我会提供一个简单的例子.现在,所有这些都是关于如何表示结果和递归的.

在表示结果时,您可以使用Prolog的成功/失败机制,因为您正在处理布尔结果.或者,您可以有一个明确的结果,例如0和1.让我们尝试0和1,因为那是你的真假表示.

% Describe a valid boolean
bool(0).
bool(1).

% The evaluation of a valid boolean is itself
exp_eval(X, X) :- bool(X).

% Evaluation of an 'and' expression
exp_eval(and(A, B), Result) :-
    exp_eval(A, ResultA),
    exp_eval(B, ResultB),
    Result #= ResultA * ResultB.

% Evaluation of an 'or' expression
exp_eval(or(A, B), Result) :-
    exp_eval(A, ResultA),
    exp_eval(B, ResultB),
    % Just a little trick to get 1 if either ResultA or ResultB or both are 1
    Result #= (ResultA + ResultB + 1) // 2.

% Evaluation of a 'not' expression
exp_eval(not(A), Result) :-
    exp_eval(A, ResultNot),
    Result #= 1 - ResultNot.  % 0 ---> 1, and 1 ---> 0

我不是像上面那样计算"布尔"1/0结果,而是可以将它们断言为如下事实:

bool_not(0, 1).
bool_not(1, 0).

bool_and(0, 0, 0).
bool_and(0, 1, 0).
bool_and(1, 0, 0).
bool_and(1, 1, 1).

bool_or(0, 0, 0).
bool_or(0, 1, 1).
bool_or(1, 0, 1).
bool_or(1, 1, 1).

然后,例如,而不是Result #= (ResultA + ResultB + 1) // 2你可以拥有,bool_or(ResultA, ResultB, Result).

既然我们可以评估表达式,我们需要一个求解器:

solve(Exp) :-
    term_variables(Exp, Variables),
    maplist(bool, Variables),  % Variables should be valid booleans
    exp_eval(Exp, 1).          % We only want true results for the expression

请注意,在原始问题陈述中,表示变量列表将作为参数给出,但您可以使用term_variables/2从表达式中获取变量.

然后你可以运行求解器:

| ?- solve(not(A and B) or not(B and C)).

A = 0
B = 0
C = 0 ? a

A = 0
B = 0
C = 1

A = 0
B = 1
C = 0

A = 0
B = 1
C = 1

A = 1
B = 0
C = 0

A = 1
B = 0
C = 1

A = 1
B = 1
C = 0

no
| ?-

我不知道你的表达是什么.但无论如何,您都可以将其映射到上述解决方案.我所展示的内容简单明了.您可以跳过这些op/3内容并使用标准术语表达式,例如,or(not(and(A,B)), not(and(B,C)))使用上面的代码.如果您将输入作为某种令牌序列,[not, (, A, and, B, ...]那么您将需要进行一些列表处理.