Max*_*iel 1 logic computer-science axiom
我正在读"计算机编程的公理化基础".他们在公理中使用可证明符号,,例如
?P {Q} R
维基百科描述了该符号的使用,因为"x⊢y表示y可以从x(在某些指定的正式系统中)证明,"但这似乎不适合这里.符号是什么意思？
该论文可在此处找到:http://www.cs.ucsb.edu/~kemm/courses/cs266/acmhoare69.pdf
在x⊢y中,x是一组假设,y是一个语句(在您正在讨论的逻辑系统或语言中)."x⊢y"表示,在逻辑系统中,如果从假设x开始,则可以证明语句y.
因为x是一个集合,所以它也可以是空集.通常这是用空集符号写的,如∅⊢y,但有时为了简洁,它完全被遗漏,这就是这里发生的事情.能够从空的假设中证明它意味着它只是真实的(或有效的).例如,⊢p→p.
Hoare的论文讨论了描述程序行为的语言.正如Todd所指出的那样,"P {Q} R"是(在这种语言中)如果你在P为真的初始状态下运行程序Q,那么之后R将为真(iff Q终止).这是您可能想要使用某些假设证明的那种陈述.这些假设将是比初始状态更高的事物:例如,如果您已经证明了一个更简单但相关的P'{Q'} R'语句,您可能想要假设它来证明更大的P {Q R语句.
因此,"⊢P {Q} R"表示"P {Q} R"这个陈述是正确的,你不需要假设任何东西.
我们来看一个愚蠢的例子吧.
⊢x = 3 {y:= x} x =3∧y= 3
我们证明的声明是:"如果x在开始时是3,你运行程序y:= x,那么之后x将是3而y将是3".您不需要任何假设来证明这一点,它来自语言的定义.您可以继续使用这一事实作为证明其他事物的假设.
x = 3 {y:= x} x =3∧y= 3⊢x = 3 {y:= x; z:= y} x =3∧y=3∧z= 3
在这里,我们使用左侧更简单的陈述作为假设来证明更大的陈述.这是一个非常愚蠢的例子,但我希望它能说明如何阅读这个.我已经the大胆地表明它是行中的"顶级"事物,将假设与结论分开.左手侧和右手侧都是Hoare逻辑中的语句,带有P {Q} R,其中P和R是逻辑语句,Q是程序.