in essence, an ebl system works by finding a way to deduce each training example from the system's existing database of domain theory. having a short proof of the training example extends the domain-theory database, enabling the ebl system to find and classify future examples that are similar to the training example very quickly.