RISC RISC Research Institute for Symbolic Computation  
  • @inproceedings{RISC3125,
    author = {Judit Robu},
    title = {{Automated Proof of Geometry Theorems Involving Order Relation in the Frame of the Theorema Project}},
    booktitle = {{Knowledge Engineering: Principles and Techniques}},
    language = {english},
    abstract = {Collins' Cylindrical Algebraic Decomposition method (CAD) can be used to prove geometry theorems that involve order relation (that is, the algebraic form consists of polynomial equalities and inequalities). Unfortu- nately only very simple geometric statements can be proved this way, as the method is very time consuming. To overcome the slowness of Collins' CAD method for complicated polynomials we propose a method (section 4) that combines the area method for computing geometric quantities and the CAD method. We present an implementation of this method as part of the Geom- etry Prover in the frame of the Theorema project.},
    series = {Studia Universitatis "Babes-Bolyai", Series Informatica},
    number = {Special Issue},
    pages = {307--315},
    isbn_issn = {ISSN: 1224-869x},
    year = {2007},
    editor = {Horia F. Pop},
    refereed = {yes},
    length = {9},
    conferencename = {Conference on Knowledge Engineering, Principles and Techniques, KEPT2007}