Twelf(Q) Architecture
Constraint Solver (CS)
- should be able to solve constraints for the types it defines
- may invoke other CSs
Constraint Solver Manager (CSM)
- installs CS modules in the system
- dispatches a constraint to the right CS during proof search
- synchronizes the internal state of all the CSs during backtracking