@inproceedings{baa7c64283384549a929f035436982c4,
title = "Proving geometric theorems using clifford algebra and rewrite rules",
abstract = "We consider geometric theorems that can be stated constructively by introducing points, while each newly introduced point may be represented in terms of the previously constructed points using Clifford algebraic operators. To prove a concrete theorem, one first substitutes the expressions of the dependent points into the conclusion Clifford polynomial to obtain an expression that involves only the free points and parameters. A term-rewriting system is developed that can simplify such an expression to 0, and thus prove the theorem. A large class of theorems can be proved effectively in this coordinate-free manner. This paper describes the method in detail and reports on our preliminary experiments.",
author = "St{\'e}phane F{\`e}vre and Dongming Wang",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1998.; 15th International Conference on Automated Deduction, CADE 1998 ; Conference date: 05-07-1998 Through 10-07-1998",
year = "1998",
doi = "10.1007/bfb0054242",
language = "英语",
isbn = "3540646752",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "17--32",
editor = "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
booktitle = "Automated Deduction - CADE-15 - 15th International Conference on Automated Deduction, 1998, Proceedings",
address = "德国",
}