问题标签 [modal-logic]

我有一个谓词将模态逻辑公式与其负范式联系起来。除了模态运算符、合取和析取之外的所有连接词都被消除了，并且否定被尽可能地推到表达式的叶子中。

rewrite/2✱ 谓词有一个包罗万象的子句，rewrite(A, A).在文本上是 last。有了这个包罗万象的子句，就可以提取否定范式的公式。在这个例子中，e是一个像 Łukasiewicz 表示法一样的双条件连接词，4并且7是模态逻辑中的变量（因此是 Prolog 常量）。

Z与负范式的公式统一。

但是，rewrite(<some constant>, <some constant>)总是成功，我不希望它成功。包罗万象的条款真的应该是一个包罗万象的条款，而不是如果另一个条款适用的话可能会触发的东西。

我尝试用受rewrite(A, A).保护的版本替换：

我认为当且仅当A 不是由具有特殊含义的原子/构造函数领导时，这将阻止包罗万象的条款适用。但是，在进行更改后，rewrite如果递归调用，总是会失败。

什么是设置捕获所有子句的正确方法。

✱ 方案全文供参考：

这篇文章从某种意义上来说是我之前的一篇。HTNW在他们的回答中定义了数据类型Same和功能allEq。所以我认为通过定义数据类型AllDifferent、函数allDiff和派生的someEq和someDiff，我将获得一种Foldable结构的模态正方形。

如果我的工作结果是正确的，如何恰当地表征这组数据类型和函数？

我写了以下代码：

但是，当我执行命令“flatten_hierarchy”时，出现以下错误：“x-1”未定义

我不知道为什么 x-1 是未定义的。

对于如何解释 Kripke 模型，我将不胜感激。

我想确定在 s_1-s_6 的哪个世界中，存在对 p 的否定（$\neg p$），但不知道如何考虑一个空的世界或一个同时包含 p 和 q 的世界，其中这种情况适用于世界 s_4 和 s_6。这两个包含 $\neg p$ 是真的吗？

如果我猜测，空的世界应该包含p的否定，因为世界上根本不存在p，但在同时包含p和q的世界中，我更加分裂。如果 p 和非 p 都存在于世界中，那么对 p 的否定真的可以存在于世界中吗？