The Future

• Iíd like to fund Andrew Rowley to do a PhD on this

  • or failing that, get him to Glasgow to do one here

• We need to do non-clausal versions of the algorithms

  • fix asymmetry in CNF between " $

• Do variants of other algorithms like Stalmarckís

• Do nice theoretical work like Judithís TCS paper

• Develop applications, e.g. in hardware verification

Previous slide

Back to first slide

View graphic version