Abstract
Proof logging is one of the greatest things to come out of Boolean satisfiability solving: as well as producing an answer, solvers are expected to give an independently verifiable mathematical proof that their answer is correct. What would it take to bring this technology to other solving paradigms? By going from Boolean models to pseudo-Boolean models, and from extended resolution to extended cutting planes, we can provide proof logging for the state of the art in subgraph finding algorithms, and make a good start on proof logging for fully general constraint programming solvers with large domains and rich constraints.