This paper presents a technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic. The technique realized as a tool called APL is implemented. The APL theoremprover is fully automated with which proofs can be recorded and checked efficiently. The tool is tested on pointerprograms mainly about singly-linked lists, doubly-linked lists and binary trees.