Automatic theorem proving in nelementary geometry

In the last 20 years several efficient methods for automatic theorem proving in elementary geometry have been developed. First we will introduce some standard notions from automatic proving theorems. Then we will present the methods on the example of the Simson theorem and its generalization. The demonstration is accompanied by the use of dynamie geometry system Cabri II.

---

W ostatnich 20 latach rozwinięto kilka skutecznych metod automatycznego dowodzenia twierdzeń geometrii elementarnej. Najpierw przedstawiono pewne standardowe nazwy dla automatycznie dowodzonych twierdzeń. Następnie przedstawiono metody oparte na twierdzeniu Simsona i jego uogólnieniach. Do prezentacji wykorzystano dynamiczny system geometryczny Cabri.