Competitive Semantic Tree Theorem Prover with Resolutions. - Choon Kyu Kim; Monty Newborn (PVM/MPI, 2003)

Exploiting parallelism: highly competitive semantic tree theorem prover. - Choon Kyu Kim (Int. J. Comput. Math., 2004)