Implementations of Constraint Logic Programming (CLP) systems are often incomplete with respect to the theories they are intended to implement. This paper studies two issues that arise in dealing with these incomplete implementations. First, the notion of incomplete satisfiability function (the analogue of unification) is formally defined, and the question of which such functions are reasonable is studied. Second, techniques are given for formally (proof-theoretically) specifying an intended CLP theory or a characterizing an existing CLP system, for the purpose of proving soundness and completeness results. Notions from linear logic and the notion of Henkinness of the theory are shown to be important here.