问题标签 [propositional-calculus]

我正在尝试生成一些命题可满足性的测试问题，特别是生成一些不可满足的问题，但是根据固定模式，这样对于任何 N，都可以生成 N 个变量的不可满足问题。

一个简单的解决方案是x1, x1=>x2, x2=>x3...!xN除了这将是所有单元子句，任何 SAT 求解器都可以立即处理，所以这不是一个足够艰难的测试。

N 个变量的不可满足问题的模式是什么，这些变量不是随机的并且可以通过检查看出是不可满足的，但对于 SAT 求解器来说至少有些不重要？

我的逻辑老师顺便说，Quines算法 也可以用来计算估值。不幸的是，我无法理解在 Prolog 中这是如何完成的？

例如，该程序将使用
Quines 算法中答案的语法给出：

由于析取 X+Y 的真值表
有 3 行的值为真：

SWI-Prolog 的新版本 8.3.19 在新的 Picat 样式规则中引入了单面统一。这可能是对任何 Prolog 系统的一个受欢迎的补充。我想知道我们是否可以重写奎因算法

Quine算法的Prolog实现
https://\stackoverflow.com/q/63505466/502187

Picat 样式规则以及这是否可行？如果是，并且如果 Quine 算法的编写变得更简单，那么 SWI-Prolog 可能通过此添加对社区大有帮助。

有人接受这个挑战吗？SWI-Prolog 8.3.19 已经可以从开发中获得。

我需要将以下命题转换为序言代码，但我不明白运算符是如何工作的。我通常使用java。

“牛仔裤只是休闲，正装裤只是正式，kakis只是半正式，腰带不是休闲，黑色袜子随时都可以接受。休闲= C，半正式= SF，正式= F，牛仔裤= J，正装裤= DP, Kakis = K, 腰带 = B, 黑袜子 = BS.J -> C, DP -> F, K -> SF, B -> !C, BS -> (C v SF v F)"

这是我已经拥有的代码：

在浏览在线资源时，我注意到可满足性的不同之处。

有时资源要求显示给定的命题是否可以满足？

但是，有时他们会要求证明一组命题是否可满足？

我对可满足性到底与什么有关感到困惑。它必须与单个命题或一组命题有关吗？

a) 判断下列语句形式是否在逻辑上等价：p -> (q -> r) and (p -> q) -> r

b) 使用 (a) 部分建立的逻辑等价，以两种不同的方式重写下面的句子。（假设 n 表示一个固定整数。）如果 n 是素数，则 n 是奇数或 n 是 2。

有人可以帮我做B吗？它真的令人困惑

基于我在 mathoverflow 社区中的问题，我想再次在这里提问，以达到更大的社区：

我正在寻找一些软件或开源项目，它们能够以自然演绎的方式证明一阶谓词逻辑的命题，例如在 Lemmon （开始逻辑）一书中介绍的，并且可以将结果放入 LaTeX 代码中。

（你可以在这里找到一个简短的介绍。）

对不起，过于复杂的例子。我有

正在做

给

然后我这样做destruct H4.了，这给了

我已经不明白了：为什么有两个相同的目标？然后我做left.并获得

然后assumption.给

然后做

再次引入了两个相同的目标，并将我带到

这与以前的状态相同，只是我现在有两个相同的前提y → x ∨ z。

我被困住了。显然我做错了什么，但是什么？

我有一个说明命题的字符串列表。例如

我的目标是将每个元素与字符串“∧”和括号“()”连接起来，从而得到以下字符串：

他们是一个简单的方法吗？

我有一些字典，例如：

它们是替换出现在 form→(q, ∧(¬(p), ∨(y, z)))或→(p, q)by字典值中的所有字符串的简单方法吗(q→(¬(p)∧(y∨z)))？(p→q)