×

Automated geometric inequalities discovering and proving. (Chinese. English summary) Zbl 0922.03018

Summary: The author offers a complete theory and an efficient algorithm for solving the system TSG. Based on these results, the author implemented a prover, EXPLORER, which has discovered many geometric inequalities automatically.

MSC:

03B35 Mechanization of proofs and logical operations
51M16 Inequalities and extremum problems in real or complex geometry
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

EXPLORER
PDFBibTeX XMLCite