The homogeneous model provides a nice symbolic and geometric computing environment for classical geometries. A Clifford bracket algebra is the quotient of the polynomial algebra generated by all nonzero inner products of vectors and all nonzero brackets modulo the two-sided ideal generated by the generalized Grassmann-Pucker relations. The present work on automated geometric theorem proving in the homogeneous model with Clifford bracket algebra further extends our previous work on theorem proving in projective geometry with bracket algebra. Two prominent features of the proofs produced by the method are geometric interpretability and simplicity, compared with proofs produced by other algebraic methods.

hli@mmrc.iss.ac.cn