问题标签 [propositional-calculus]

我正在尝试为 R 中的逻辑变量创建一个“暗示”运算符，以使命题演算更容易。然而，它似乎并不适合否定运算符。正如这里的最后 4 行所示，我必须将否定变量括在括号中，以使蕴含运算符正常工作。

我怀疑运算符优先级是问题，但我不确定。从我读到的内容来看，没有办法改变中缀运算符的优先级。有没有一种方法可以重新定义，这样就不需要implies()括号了？(!q) %->% (!p)

主要问题：如何更新我的命题逻辑的递归下降解析器（用 JavaScript 编写），以便像“p~”和“pp”这样的字符串将返回“无效”消息？

我对 HTML、JavaScript 和解析非常陌生。我想看看我是否能够制作一个简单的网页，可以从命题逻辑中解析简单的公式。这是语法：

我是这样写语法的新手，所以希望这种语法有意义。据我了解维基百科对左递归语法的了解，我不相信这种语法是左递归的，也不显得模棱两可。

然后我尝试创建一个简单的网页，允许某人在文本框中输入公式，单击“验证”按钮，并返回一条简单的消息，说明公式是否有效。我试图编写一个可以进行解析的递归下降解析器。以下是我根据 Wikipedia、Stack Overflow 和我发现的关于该主题的其他资源 ( jsfiddle ) 得出的结论：

解析器似乎主要工作。它正确地将以下字符串解析为有效公式：

但是，当它应该返回“无效”时，它错误地为这些字符串返回“有效”：

在这些情况下，解析器似乎没有检查整个字符串，只检查第一个字母之前的字符和字母本身，因此认为它很好。我尝试在“else if (proposition(sym)”部分的 formula() 中添加某种验证，以确保字母后面的字符是有效的，但这不起作用，因为有效字符会根据什么而改变出现在它之前。更改我的语法可能会有所帮助。我真的不明白在创建这些语法时应该考虑什么，除了左递归会给递归下降解析器带来麻烦。我在 Stack Overflow 上查看了关于递归下降的几个问题解析器，但似乎没有一个可以帮助我解决我的问题。

如何更新我的解析器，以便此类字符串返回“无效”作为结果？我不一定要寻找完整的答案，只是一些关于要考虑的事情或要查看的资源的指示。如果您还知道构建语法（尤其是参考解析器）时要考虑的内容的好资源，那将是非常棒的。

注意：我的解析器目前不处理空格。我现在对此很好，因为我最关心的是在更新事物以处理空白之前让其他解析正确。

在我的理论 CS 作业中，我偶然发现了布尔函数的外观问题，即测试 n 个给定的布尔变量、x1 到 xn、k 或更少的变量是否为真。

在 Java 中，这将相当简单：

现在的问题是通过依赖于 n 和 k 的命题演算找到一个公式，该公式仅在给定的 n 中的 k 或更少为真时才返回真。

举个例子，如果我们让 k = 1，则公式对应于 NAND 函数：

(x1 , x2) ^<=1 = NOT(x1 AND x2)

(x1 , x2 , x3) ^<=1 = NOT( (NOT(x1 AND x2)) AND x3)
。
.
.

到目前为止的问题是，如果 k 增加，公式将如何变化......

还有一个非常明显的联系是：

(x1, x2, ..., xn) ^<=k = (x1, ..., xn) ^=k OR (x1, ..., xn) ^=k-1 OR ... OR (x1, ... ., xn) ^<=1

我是精益证明的新手，我正在尝试解决在线教程中的示例。

我被这个例子困住了，我需要证明“假暗示q”或类似的东西。我的代码是：

我不认为定义 hnpq 会有所帮助，因为这个证明是 (¬ p ∨ q) → (p → q) 的一部分。在集合论中，我认为 false 意味着一切。

有什么建议或想法吗？

我正在尝试扩展 Miles Sabin 的这篇优秀文章中描述的功能：Unboxed Union Types以支持n元类型联合，例如：

我修改了 Sabin 的代码并编写了我自己的<:<操作符版本，如下所示。

根本问题是每个额外的逻辑析取 ( OR) 将生成的证据子类包装在一个新的双重否定中，即

从理论上讲，我希望双重否定身份的定义与传递性的定义相结合，以允许它起作用，但是我无法编译它。有谁知道这是否可能，或者递归链接的泛型是否超出了 Scala 编译器的能力？

在研究命题逻辑时，我提出了以下问题：

软件错误总是程序和规范之间的逻辑矛盾吗？

考虑以下示例：我们的规范告诉我们“如果前提 A 和 B 为真，我们会执行动作 C ”。

其实现如下：

很明显，可以看到规范不适合实现，因为（考虑上面的程序）“如果前提 A 或前提 B 为真，我们会做 C ”。

将我们的规范和程序表达为命题公式，我们得到以下等式：

我们将规范转换为 CNF 并应用解析演算，现在我们可以很容易地看到第一个子句与最后一个子句相矛盾。因此这个公式是不可满足的，因此我们的规范与我们的实现相矛盾。

我现在的问题是（因为上面只是一个例子）：

假设一个完整的文档，对于每个软件错误都是如此吗？

如果是这样：

如果我们将完整的规范转换为命题公式，我们是否可以自动化软件错误发现的过程？

我试图证明

在此处输入链接描述

我只能使用介词逻辑。我尝试使用 not+/- 规则，但它们要求我同时假设 P 而不是 P。在这一点上我真的迷路了

我目前正在尝试将上下文无关语法用于命题逻辑。

我想象这组终端将如下所示：

现在我需要定义一组产品，这可以帮助我实现所有合法的复合命题。谁能帮我？我真的不知道从哪里开始，大量的终端有点让我失望

对于一项作业，我们必须编写 Python 代码来对命题逻辑 KB 执行解析。

所有代码似乎都可以正常工作，除了recursive_print_proof. 运行程序时，它将一直运行，直到您告诉它停止。

它应该做的是根据分辨率输出一个证明。但是，它似乎陷入了一个循环。

希望任何人都可以帮助我。

recursive_print_proof几乎可以在最后找到。我的代码是：

I know only one prover that translates the algorithm that Quine gave for classical propositional logic in his book Methods of Logic (Harvard University Press, 1982, ch. 1 sec. 5, pp. 33-40), this prover is in Haskell and it is here: Quine's algorithm in Haskell

I tried to translate Quine's algorithm in Prolog, but until now I have not succeeded. It is a pity because it is an efficient algorithm and a Prolog translation would be interesting. I am going to describe this algorithm. The only Prolog code that I give at the start is the list of operators that would be useful to test the prover:

Truth constants are top and bot for, respectively, true and false. The algorithm starts as follows: For any propositional formula F, make two copies of it and replace the atom which has the highest occurrence in F by top in the first copy, and by bot in the second copy, and then apply the following ten reduction rules one rule at a time for as many times as possible, for each of the copies:

Of course, we have also the following rules for negation and double negation:

When there is neither top nor bot in the formula so none of the rules apply, split it again and pick one atom to replace it by top and by bot in yet another two sided table. The formula F is proved if and only if the algorithm ends with top in all copies, and fails to be proved, otherwise.

Example:

It is clear that Quine's algorithm is an optimization of the truth tables method, but starting from codes of program of truth tables generator, I did not succeed to get it in Prolog code.

A help at least to start would be welcome. In advance, many thanks.

EDIT by Guy Coder

This is double posted at SWI-Prolog forum which has a lively discussion and where provers Prolog are published but not reproduced in this page.