Optimal Length Resolution Refutations of Difference Constraint Systems
A Formalization of Powerlist Algebra in ACL2
KBO Orientability
On Protocols for the Automated Discovery of Theorems in Elementary Geometry