π-演算中无卫递归的消除

本文提出消除π－演算中无卫递归的公理，证明了将该公理加入到正则π－演算受卫递归子集上的证明系统后，所得到的证明系统在π－演算全体正则子集上关于互模拟等价的可靠性和完备性.