A Machine-Checked Implementation of Buchberger's Algorithm*
Computer-Aided Construction of Finite Geometric Spaces
Structured Theory Development for a Mechanized Logic*
The Warshall Algorithm and Dickson's Lemma