|
软件学报 1995
维护的证明论系统, PP. 513-524 Abstract: 给定一阶语言及该语言的一个理论,假设需要在理论中添加一个与理论不和谐的语句,并要求保持理论的扩张是和谐的,就必须删除理论内的某些语句.删除理论中尽可能少的语句,即保留理论与需要添加语句和谐的一个极大子集,是构造理论扩张的一种方法.本文构造出了针对上述理论扩张的证明论.该证明论的可靠性及完全性刻划了一般形式的理论扩张与典型的理论扩张间的联系.对于命题逻辑,本文还给出了判定理论扩张的一种方法.
|