it would be good to keep notes of style discussions (what's bad, how to fix it) during the code cleaning spree.
write a small style guide for new code
for next IJCAR: write system description (with 2.0 release)
release 2.0 this year (including portfolio, no global state, maybe disable induction/arith by default, proof checking)
proof checking, presented by @Alexander Bentkamp at Daghstul.Some suggestions:
look at extension proofs (Dale Miller)
cost of unifiers
constraints in clauses (e.g. flex/flex pairs, AC unification constraints, etc.). These would be carried over in all inference rules, and need to have an associated decision procedure to check their satisfiability (trivial for flex/flex).