Logic-based Truth Maintenance System, and the name of a C++ class that implements it. It is the propositional inference system of the Conflict Data Base.