R-演算:一个修正程序规约的演算系统

在一个软件规约（Program specification）的形成过程中,规约总是不断被修改,要么增加新的功能,要么由于出现事实反驳,而改正规约中的错误.规约的新功能是与其逻辑无关的新规则,而它的事实反驳则是其反例.新规则和事实反驳都是由研究者或用户提出来的.极大缩减是在规约出现事实反驳的情况下,对规约的理想修正.这里在一阶逻辑的框架下给出规约的新规则、事实反驳和极大缩减的模型论定义.构建了R-演算.该演算由一组变换规则组成,用以删除规约中与事实反驳矛盾的规则,并最终得到规约的极大缩减.同时证明了R-演算的可达性和完全性.

科学发现的逻辑验证

R演算是一个关于逻辑连接词符号和量词符号的演算系统.它是一个根据事实反驳对科学理论进行修正的符号演算系统.文中以狭义相对论和生物进化论为例,使用R演算,对这两个科学理论的发现过程,在数理逻辑层面进行了验证.验证的结果表明:对Einstein时代的物理学而言,狭义相对论是唯一而且正确的选择.对Darwin时代的生物学而言,在接受自然选择原理等前提下,R演算可以推导出3种不同的,但逻辑上合理的进化论方案.Darwin提出的进化论是其中一种.有趣的是三者中的另一种,现在看来它具有一定的包容性.