prolog - 序言和翻译命题逻辑

Question

我的最终目标是将一组命题公式从文件加载到 Prolog 中，以推断出一些事实。假设我有命题公式：

p implies not(q).

在 Prolog 中，这将是：

not(q) :- p

Prolog 似乎不喜欢not规则头部的运算符。我收到以下错误：

 '$record_clause'/2: No permission to redefine built-in predicate `not/1'
        Use :- redefine_system_predicate(+Head) if redefinition is intended

我知道重写通用公式的两种方法p implies q。首先，利用对立式在逻辑上等价的事实。

p implies q当且当not(q) implies not(p)

其次，使用p implies q逻辑上等价not(p) or q的事实（真值表相同）。

第一种方法导致我当前的问题。第二种方法只是合取或析取。你不能在 Prolog 中只写连词和析取词，因为它们不是事实或规则。

1. 解决我的问题的最佳方法是什么，以便我可以表达p implies not(q)？
2. 是否可以在 Prolog 中编写所有命题公式？

编辑：现在我希望将我的结果与其他命题公式联系起来。假设我有以下规则：

something :- formula(P, Q).

这是如何连接的？如果我formula(false, true)在解释器中输入（计算结果为真），这不会自动变为something真。这就是我想要的。

Answer 1

p => ~q  ===  ~p \/ ~q  === ~( p /\ q )

所以我们可以尝试用 Prolog 程序对此进行建模，

formula(P,Q) :- P, Q, !, fail.
formula(_,_).

或者您可以使用内置的\+ie“not”，将其定义为formula(P,Q) :- \+( (P, Q) ).

这只是检查传递的值是否符合公式。如果我们首先将其与域生成结合起来，我们可以“推断”，即生成符合要求的值：

13 ?- member(Q,[true, false]), formula(true, Q).  %// true => ~Q, what is Q?
Q = false.

14 ?- member(Q,[true, false]), formula(false, Q). %// false => ~Q, what is Q?
Q = true ;
Q = false.

Answer 2

您使用了错误的工具。尝试答案集编程。