问题标签 [implication]

Here is a little test:

When I load this into SWI-Prolog:

The -> branch doesn't have access to the (local) variables Eos and Gos? But why?

It has access to Value because that one appears in the head I suppose.

And indeed:

It don't really see why this restriction occurs, expect that maybe it's a part that hasn't been implemented in the compiler?

(Btw, we need one of those "keep the bar in the green windows" for unit testing from the Java World, like this: (stolen from here)

这个问题是关于我正在做的一个项目，即在 Coq中编写Principia Mathematica代码。Principia导出了推理规则，其中之一是 Syll：

∀ PQR : 道具, P→Q, Q→R : P→R

我正在尝试创建一个对 Syll 推理形式进行编码的 Ltac 脚本。以下来自（Chlipala 2019）的 MP 策略非常有效：

这里我认为“=>”右边的策略专门将H1应用于H2。现在相关的 Syll 策略不起作用：

我在应用它时遇到的错误（在下面的示例中）是：

没有匹配的匹配子句。

我不确定为什么这是由此产生的错误。引入经典逻辑，证明为定理Syll2_06，即(P→Q)→((Q→R)→(P→R))。事实上，基本上是 Syll Ltac 被应用于定理 Trans2_16 的证明（见下文）。所以我不确定为什么将代码转换为 Ltac 脚本不起作用。

也许我误解了 Ltac 匹配在做什么，以及“=>”右侧的策略应该是什么。但是根据查看Coq 手册，可能是策略的左侧是问题所在，可能是因为 H1 不适用于 H2。

进一步的建议，特别是解释 Ltac 和/或我的思考方式错误的建议，将不胜感激。

我遇到了一个在这里工作的示例属性：

上面没有语法错误。

然后我尝试修改为此

这给了我语法错误，只是意识到它实际上不是'|->'

这行得通，那么->属性中的实际符号是什么？我通常知道它用于触发事件。

标题。

假设您有 3 个问题：

Q1、Q2 和 Q3

每个问题有 3 个答案：

a1、a2 和 a3。

还假设您有 2 个学生，他们的结果。

S1 已回答：

Q1->a1，Q2->a3，Q3->a1，得分为2/3

S2 已回答：

Q1->a1，Q2->a1，Q3->a1，得分为1/3

从那里您应该能够确定 Q2->a3 是正确答案，Q3->a1 或 Q1->a1 也是正确的。

是否有任何有效的算法来解决这组约束？

如果可能的话，我也希望有人给我一些研究或提示。:D

有人可以帮我线性化这个含义吗？

作为 x 和 y 整数变量，含义如下

我真的很感激一些帮助。