问题标签 [verifiable-c]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

32 问题
Newest
Active
Bountied
318
Unanswered
0 投票
0 回答
10 浏览

verifiable-c - 存在主义魔杖的意义何在？

我试图理解“存在魔杖”运算符的意义。我看到(P * Q) -o R = P -o (Q -o R)，这显然是一种柯里化形式，|> (P -o Q) = |> P -o |> Q只是一个分配公理。

公理ewand_TT_sepcon( (P * Q) && (R -o TT) |-- (P && (R -o TT)) * (Q && (R -o TT)))、exclude_elsewhere( P * Q |-- (P && (Q -o TT)) * Q))
和ewand_conflict( P * Q |-- FF -> P && (Q -o R) |-- FF) 让我感到困惑。

存在魔杖的预期语义是什么？

0 投票
0 回答
18 浏览

verifiable-c - 蕴涵谓词

我们确定不可能以天真的方式将序列嵌入到分离逻辑中吗？

在 PLCC 的第 100 页上，它指出 ifP [|-] Q意味着“适用于所有世界w，如果w |= P那么w |= Q，那是行不通的，因为它无法证明(P [|-] Q) |-- |> (P [|-] Q)。

我不明白为什么嵌入它!!(P |-- Q)不起作用，特别是因为证明这一点很简单，而且证明起来也
!!(P |-- Q) |-- |> !!(P |-- Q)没有那么难
!!(P |-- Q) |-- !!(|> P |-- |> Q)。


12345678910