Автоматическое доказательство и анализ геометрических теорем, заданных в бескоординатной форме, с помощью метода антикоммутативных базисов Грёбнера

Некоторые геометрические теоремы можно задавать в бескоординатной форме как полиномы алгебры Грассмана и доказывать с помощью метода антикоммутативных базисов Грёбнера. В данной статье анализируются некоторые свойства как набора посылок теоремы, так и совокупности посылок и заключений теоремы.