|
Автоматизация доказательства и открытия геометрических теорем и генерации диаграмм
Часто говорят, что "один рисунок несет в себе больше информации, чем тысяча
слов". Однако в жизни генерировать рисунки с помощью компьютерных программ
все еще намного более обременительно (если вообще возможно) по сравнению с
обработкой текстов: особенно, в тех случаях, когда рисунки включают в себя
точные геометрические отношения. Еще более сложной является автоматизация
доказательства геометрических теорем, что всегда рассматривалось как тяжелый
интеллектуальный труд. В нашем докладе мы представим некоторые
эффективные методы автоматического доказательства и
формулирования геометрических теорем, также метод генерации геометрических
диаграмм, включая метод области, метод дедуктивной базы данных, метод
оптимизации, и метод декомпозиции c-дерева. Мы также обсудим реализацию и
приложение этих методов к интеллектуальным системам автоматизированного
проектирования и обучения, системам компьютерного зрения, робототехнике, и к
проектированию сборки.
|
