[TYPES] A geometry problem for proof systems

Yong Luo Y.Luo at kent.ac.uk
Wed Sep 21 08:02:53 EDT 2005


The following geometry problem might be interesting for those who develop
proof systems based on type theory.

Property:  A triangle with two internal angle bisectors of equal length is
an isosceles triangle.

 More precisely, in a triangle ABC, the point D is on the line segment BC
and E on AC, and the line segments AD and BE are internal angle bisectors
(i.e. the angle CAD is equal to the angle DAB, and the angle ABE is equal to
EBC). If AD and BE are of equal length (AD=BE), then AC=BC.

If this property is not true, can we have a counter example? Is there anyone
interested in proving it in Coq or other systems ?

I asked myself this question in 1991, but I am not able to prove it even



Dr. Yong Luo
Computing Laboratory
University of Kent

More information about the Types-list mailing list