Abstract: This paper introduces an idea of environment of proving theorem by Boyer-Moore's method, and presents corresponding implementation KTPE system on microcomputer IBM-PC.