Soundness and Completeness of Kung's Reasoning Procedure

• 作 者: 黎仁蔚
• 机 构: Institute of Software Academia Sinica,
• 出 处: Journal of Computer Science and Technology
• 发表日期: 1988年01期
• 关键词: reasoning parallelism proof inconsistent literal carry 几几 somewhat interested fa

Kung’s reasoning procedure is characterized by high parallelism in the sense that an unlimited numberof CPUs can be used to carry out the computation in parallel.This paper presents a proof of the soundness andcompleteness of the reasoning procedure based on Herbrand’s theorem.

Kung’s reasoning procedure is characterized by high parallelism in the sense that an unlimited number of CPUs can be used to carry out the computation in parallel. This paper presents a proof of the soundness and integrity of the reasoning procedure based on Herbrand’s theorem.