Clifford algebra formalism has been used recently in combination with standard term-rewriting techniques for proving many nontrivial geometric theorems. The key issue in this approach consists in verifying whether two Clifford expressions are equal. This paper is concerned with the generalization of the work to 3D geometric problems. A rewriting system is proposed and its theoretical properties are investigated. Some examples and potential applications are also presented.