我正在阅读“计算机编程的公理基础”。他们在公理中使用可证明符号⊢,例如
⊢P {Q} R
维基百科将该符号的使用描述为“x ⊢ y 表示 y 可以从 x 证明(在某些指定的形式系统中)”,但这似乎不适合这里。符号是什么意思?
该论文可以在这里找到:http ://www.cs.ucsb.edu/~kemm/courses/cs266/acmhoare69.pdf
我正在阅读“计算机编程的公理基础”。他们在公理中使用可证明符号⊢,例如
⊢P {Q} R
维基百科将该符号的使用描述为“x ⊢ y 表示 y 可以从 x 证明(在某些指定的形式系统中)”,但这似乎不适合这里。符号是什么意思?
该论文可以在这里找到:http ://www.cs.ucsb.edu/~kemm/courses/cs266/acmhoare69.pdf