Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method

Nicholas Freitag McPhee, Shang Ching Chou, Xiao Shan Gao

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    6 Scopus citations

    Abstract

    Wu’s method has been shown to be extremely successful in quickly proving large numbers of geomelxy theorems. However, it is not generally complete for real geomeu’y and is unable to handle inequality problems. Collins’ method is complete for real geometry and is able to handle inequality problems, but is not, at the moment, able to prove some of the more challenging theorems in a practical amount of time and space. This paper presents a combination that is capable of proving theorems beyond the theoretical reach of Wu’s method and the (current) practical reach of Collins’ method. A proof of Pompeiu’s theorem using this combination is given, as well as a list of several other challenging theorems proved using this combination.

    Original languageEnglish (US)
    Title of host publicationAutomated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings
    EditorsAlan Bundy
    PublisherSpringer Verlag
    Pages401-415
    Number of pages15
    ISBN (Print)9783540581567
    DOIs
    StatePublished - 1994
    Event12th International Conference on Automated Deduction, CADE-12 1994 - Nancy, France
    Duration: Jun 26 1994Jul 1 1994

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume814 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference12th International Conference on Automated Deduction, CADE-12 1994
    CountryFrance
    CityNancy
    Period6/26/947/1/94

    Fingerprint Dive into the research topics of 'Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method'. Together they form a unique fingerprint.

    Cite this