logic - 公理化编程论文中可证明性符号⊢的含义

Question

我正在阅读“计算机编程的公理基础”。他们在公理中使用可证明符号⊢，例如

⊢P {Q} R

维基百科将该符号的使用描述为“x ⊢ y 表示 y 可以从 x 证明（在某些指定的形式系统中）”，但这似乎不适合这里。符号是什么意思？

score 6 · Accepted Answer

6

于 2012-02-10T22:03:40.587 回答

score 0 · Accepted Answer

0

⊢P {Q} R

是说“P是程序Q产生结果R的先决条件”

于 2012-02-10T21:35:52.440 回答

2 回答 2