Soundness and completeness of Kung’s reasoning procedure
Soundness and Completeness of Kung s Reasoning Procedure

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 completeness of the reasoning procedure based on Herbrand’s theorem.