The framework of learning from entailment introduced by Angluin (1988) and Frazier and Pitt (1993) allows the following types of queries. Through an entailment equivalence queryEQUIV(H), the learner asks the teacher whether his theory (a set of first-order formulas) H is logically equivalent to the target theory H * or not. The teacher answers ‘yes’ to this query if H and H * are equivalent, i.e., H⊧H * and H *⊧H. Otherwise, the teacher produces a formula C such that H *⊧C but or but H⊧C. The request-for-hint query REQ(C) returns (1) an answer ‘not-entailed’ if , or (2) an answer ‘subsumed’ if C is subsumed by a formula in H *, or (3) a formula (hint) B in the proof of H *⊧C if C is not subsumed by any formula in H * but H *⊧C.