"Russian Killer'' No. 2: A Challenging Geometric Theorem with Human and Machine Proofs

Xiaorong Hou 1 Hongbo Li 1 Dongming Wang 2, 3 Lu Yang 1
2 CALFOR - Calcul formel
LIP6 - Laboratoire d'Informatique de Paris 6
3 SPACES - Solving problems through algebraic computation and efficient software
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This article presents one human proof and three machine proofs of a challenging geometric theorem that gives a beautiful representation of the area of an arbitrary quadrilateral in terms of its four sides and four internal angles. These proofs demonstrate the power, capability and features of automated deduction methods and tools, which reduce qualitative difficulty to quantitative complexity versus traditional methods with individual ingenious ideas, for mathematical theorem proving. The present case study not only results in four probably new proofs of a hard theorem but also contributes to understanding the significance of developing effective algorithms and software tools for automated theorem proving in mathematics using advanced computing technology.
Type de document :
Article dans une revue
The Mathematical Intelligencer, 2001, 23 (1), pp.9-15. 〈10.1007/BF03024512〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00100618
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:48:24
Dernière modification le : mercredi 21 mars 2018 - 18:58:14

Lien texte intégral

Identifiants

Collections

Citation

Xiaorong Hou, Hongbo Li, Dongming Wang, Lu Yang. "Russian Killer'' No. 2: A Challenging Geometric Theorem with Human and Machine Proofs. The Mathematical Intelligencer, 2001, 23 (1), pp.9-15. 〈10.1007/BF03024512〉. 〈inria-00100618〉

Partager

Métriques

Consultations de la notice

195