The research field of automated geometry theorem proving has developed many new methods; but, all of them have not used the rings of vector. In the paper, the authors have proposed a new approach based on vector rings, implemented a machine proving program, which emphasis loop of vectors. This program could construct most common constructive geometry drawings very quickly, do automated reasoning with various vector methods according to different types of constructions which includes equal vectors, perpendicular vectors or definite proportional division points, and the proofs are concise and readable. The prover with vectors has been used to produce short and elegant proofs for some constructive constructions. Therefore, this new approach could be used in education. With many instances test, it shows automated reasoning with vectors is available, which also enhance the efficiency and readability.
更多
查看译文
关键词
Automated reasoning,Dynamic geometry,Readable proof,Forward chaining,Vector method,Vector ring