Prolog：正确初始化与运算符连接的谓词变量答案

【问题标题】：Prolog: Initialize predicate variables connected with operators correctlyProlog：正确初始化与运算符连接的谓词变量
【发布时间】：2022-01-21 04:40:40
【问题描述】：

我创建了一些谓词，类似于我想在下面给您的（希望是）最小示例中的谓词。有了这个，我希望通过以下逻辑方式获得集合Z：

给定一些全集 {peter, sandra} 和一些二元运算符 l 和 x（l 代表是爱，x 代表等价）和一些基本公理（以变量的形式），比如说

A l A
(B l A) x (A l B)

我现在想列出所有公理，这些公理完全解释了我们的集合所说明的某些特定公理，并将它们的列表保存在某个变量中。为此，我生成了谓词

find_axioms(Specific, BaseSet, Fullfill)

目标：

BaseSet 是我们可能的公理列表[A l A, (B l A) x (A l B)] 变量 Fullfill 应该是一些返回码，比如 Z 而具体是一组由公理检查的爱情关系，例如[彼得 l 安娜，彼得 l 彼得]。

现在如果我这三个参数，说我打电话

find_axioms([(peter l anna), (peter l peter)], [(A l A), (B l A) x (A l B)], Z).

我的预期输出应该是：

A = peter
Z = peter l peter

axiom (B l A) x (A l B) 不应该是其中的一部分，因为此模板不在我们的变量 Specific 中，因此可以在 Z 中忽略它。

现在我试图用以下逻辑陈述来解释这一点：

∀ x in Specific: x in BaseSet → x in Fullfill

我现在预计，代码应该是这样的：

:-op(900, xfy, l).
:-op(900, xfy, x).


find_axioms(Specific, BaseSet, Fullfill) :-
    forall(member(X, Specific), 
        (member(X, BaseSet) -> member(X, Fullfill))).

但出于某种原因

find_axioms([(peter l anna), (peter l peter)], [(A l A), (B l A) x (A l B)], Z).

只给出输出 false 并且没有以我期望的方式定义变量。一些语法，如

(A l A) = (peter l peter)

反而给了我我期望的正确输出：

A = peter

【问题讨论】：

标签： prolog predicate

【解决方案1】：

谓词forall/2 可以很好地证明关系或产生一些副作用（例如，与write/1 或assertz/1 一起使用时）。如果您打算创建变量绑定，则此谓词是不够的（因为它不会更改任何变量绑定）。相反，您应该使用谓词findall/3（另请参阅bagof/3 和setof/3）。

因此，我认为您可以尝试以下方法：

find_axioms(Specific, BaseSet, Fullfill) :-
    findall(X, 
            ( member(X, Specific), 
              member(X, BaseSet) ), 
            Fullfill).

【讨论】：