Автоматизация доказательства и открытия геометрических теорем и генерации диаграмм
Часто говорят, что "один рисунок несет в себе больше информации, чем тысяча слов". Однако в жизни генерировать рисунки с помощью компьютерных программ все еще намного более обременительно (если вообще возможно) по сравнению с обработкой текстов: особенно, в тех случаях, когда рисунки включают в себя точные геометрические отношения. Еще более сложной является автоматизация доказательства геометрических теорем, что всегда рассматривалось как тяжелый интеллектуальный труд. В нашем докладе мы представим некоторые эффективные методы автоматического доказательства и формулирования геометрических теорем, также метод генерации геометрических диаграмм, включая метод области, метод дедуктивной базы данных, метод оптимизации, и метод декомпозиции c-дерева. Мы также обсудим реализацию и приложение этих методов к интеллектуальным системам автоматизированного проектирования и обучения, системам компьютерного зрения, робототехнике, и к проектированию сборки.
Профессор Сяо-Шань Гао родился в 1963 году в Китае. В 1988 году он получил научную степень доктора философии от Китайской академии наук и в настоящее время является директором Института Исследований Систем (Institute of Systems Science) АН КНР. Его исследовательские интересы включают геометрические вычисления и доказательства, символьные вычисления, робототехнику, САПР и системы автоматизации геометрического проектирования (CAGD). Профессором Гао опубликовано около 90 научных статей и две монографии, а также осуществлено редактирование четырех изданий трудов конференций.