Optimal Length Resolution Refutations of Difference Constraint Systems K. Subramani OriginalPaper 27 June 2009 Pages: 121 - 137
A Formalization of Powerlist Algebra in ACL2 Ruben A. Gamboa OriginalPaper 01 July 2009 Pages: 139 - 172
KBO Orientability Harald ZanklNao HirokawaAart Middeldorp OriginalPaper 23 April 2009 Pages: 173 - 201
On Protocols for the Automated Discovery of Theorems in Elementary Geometry G. DalzottoT. Recio OriginalPaper 24 June 2009 Pages: 203 - 236