[SOUND] In our first approach, we'll forget about the context. and we’ll talk to an oracle that answers membership and equivalence queries with respect to some implication set L* (which may be the canonical basis of some formal context). The set of implications describes a set of models. A model of L* is an attribute combination that satisfies all the implications from L*. So, when we pose a membership query about an attribute set A and ask if A is a member of the set of models of L*, we actually ask if A satisfies all the implications from L*. In an equivalence query, we propose an implication set L, and we ask if this set has exactly the same models as L*. This is what we mean by the equivalence of two implication sets. If not, the oracle provides a positive or a negative counterexample. A positive counterexample, in this case, is a set that satisfies all the implications of L*, but violates one of the implications of L, one of those implications that we suggested as a hypothesis. And the negative counterexample, is a model of L that satisfies all implications from L, but, however, violates one of the... one or more of the implications from L*. Well, how do we handle these counterexamples? If a counterexample X is positive, this means it doesn't satisfy some implication A —> B from our hypothesis set L. So, we should weaken this implication by replacing it with another implication that is not violated by X. One way to do so is to replace the conclusion of this implication B by the intersection of B and X. So, we used to have an implication A implies B, and now we have an implication A implies B intersection X. A is a subset of X, but B intersection X is also a subset of X. So, this implication is no longer violated by X. Good, and we do this for every implication from L, for which X is a counterexample, for which X is not a model. If X is a negative counterexample, it means that our hypothesis is not strong enough. It allows X, X satisfies our implications, but it shouldn’t, because it doesn't satisfy implications from L*. So, we should pick one of the implications, A implies B, from our set L, and we'll try to strengthen it. We'll replace the premise of this implication A by the intersection of A and X. And then we'll get an implication A intersection X implies B. And if B is not a subset of X, then this new implication forbids X as a model. If we can't find an implication that we could strengthen so as to exclude X from the set of models, then we'll simply add a new implication, X implies M to the end of our list L. Okay, so this is the basic idea. Before looking at the pseudocode of the algorithm, let's first look how it works on an example. Suppose that we work with attribute set {a, b, c, d}. And the target implication set L* contains three implications, cd implies a, a implies c, and abc implies d. We don't know L*, our task is to compute it, all we know is M. The attributes are a, b, c, d. So, we're going to use queries to compute L*. We are going to use equivalence and membership queries. Let's start with the empty hypothesis. So, our hypothesis L initially contains no implications at all. And therefore every, attribute combination, every attribute subset is a model of L. We submit an equivalence query with this empty set of implications, and well, all possible counterexamples must be negative. Let's suppose, in this case, the counterexample is abc. Well, indeed, it satisfies our set of implications, because our set of implications is empty, so, any attribute combination satisfies it. But it doesn't satisfy L star. Well, we don't know L star, but suppose that we know, then we can check that abc fails to satisfy the third implication. It has, it contains abc, but it doesn't contain d. So, this is a negative counterexample. Well, looks like the only thing we can do at this point is to add the implication abc —> abcd to our hypothesis. It removes the counterexample abc from the set of models of L, but that's all it does. Okay. So, let's submit the second equivalence query, now using this set of implications with just one implication abc —> abcd. Suppose that, in return, we get a counterexample a. Now, let's check if it's positive or negative. Well, it doesn't violate our implication because {a} doesn't contain {a, b, c}, so this implication doesn't apply to it. And then, it must violate L*. So, it's a negative counterexample. Let's see what we can do about it. First of all, we can look at implications we already have an L, and we can try to strengthen one of them, so that it wouldn't exclude a from the set of models of L. Well, there's only one implication, abc —> abcd, and this is what we'll do. We'll compute the intersection of our counterexample and the premise of this implication, so as to make sure that the premise of the updated implication would apply to our counterexample, so we compute the intersection of a and abc. This is a, of course. And then one thing, what we would like to do is to replace abc in this implication by a. In this case, the resulting implication would exclude a. But to do this, we first need to check whether a is a model of L*. If it's a model of L*, or in other words, if it's closed in L*, then it's really not good to replace abc with a, because, if a is a model of L*, then a implies nothing: there's nothing that follows from a, well, except for a itself. Well, actually, in this particular case, we already know that a is not a model of L*, because we got it as a counterexample. But the algorithm would check this, nevertheless. So, we check if a is closed in L* by issuing a membership query about a. And the answer in this case will be no, so we know that a is not a member of L*, and thus it is safe to... well, maybe it's not completely safe, but at this point of our algorithm, we can remove b and c from the premise of this application and by doing so, we'll exclude a from our set of models. So now our hypothesis looks this: a —> abcd, and that's all. And we submit the third equivalence query. Suppose that we get the counterexample cd. Is it positive or negative? Well, cd doesn't contain a, so this implication doesn't apply to cd. And we have no other implications in L, so cd is a model for L. And then it must be a negative counterexample. So again, we are going through implications of L, and see if we can strengthen one of them, so as to include cd. So, the implication that we have here is a —> abcd. Now we compute the intersection of cd and a, this is empty, and we would like to replace a with the empty set here, but we don't do it immediately. First, we ask our oracle whether the empty set is a model of L*. And in this case, the oracle will say yes, because the empty set doesn't violate any of these implications. Because of this, we will not strengthen this implication, but we will instead add another implication, a separate implication, cd —> abcd. Now, this additional implication will remove cd from the set of models, but it will not remove the empty set from the set of models, whereas, if we replaced a by the empty set, we would lose the empty set as a model of L*. And we don't want that. Okay, so we submit the fourth equivalence query with the set L, which currently contains two implications: a —> abcd, and cd —> abcd. And in return, we get, well, let's say we get acd. Now, what kind of counterexample is it? Well, it doesn't satisfy this implication, because it contains a, but it doesn't contain b. So, this must be a positive counterexample. This is something that violates L, but it's compatible with L*. And positive examples are easy to handle. We check all the implications of L, find those that are violated by this counterexample, and correct this violation. So, this a —> abcd is violated by acd, and we correct this by removing b from its conclusion. And we do the same with this implication, because cd is also a subset of acd, but abcd is not a subset of acd. So, we compute the intersection of abcd and acd. We get acd, and that's the new conclusion of this second implication. So, we remove b from here. All right, so this is our new hypothesis. Now, acd is compatible with this set of implications. Okay, and we issue the fifth equivalence query. Now, suppose we got ac as a counterexample. And this one is also positive, because it violates our implication, so it's not a model of L. So, we correct this implication. Now, a is a subset of ac but acd is not a subset of ac. To correct this, we'll remove d from the first implication. And cd is not a subset of ac, so ac doesn't violate this implication. Okay, and now the sixth equavalence query gives us, let's say, counterexample abc. Note, by the way, that at some point we have already obtained this counterexample, and we added an implication that excluded this counterexample, abc —> abcd. But then something has happened to this implication, it has been modified quite a bit. So, at this point, this implication no longer forbids abc, because, well, abc is compatible with it: {a, b, c} contains a, but it also contains a and c. And {a, b, c} doesn't contain {c, d}, so it's also compatible with this implication. So, abc is a model of L, and this means it's not a model of L*, it's negative counterexample. Okay, so we'll look at these implications, and we try to see whether we can strengthen them in such a way that they exclude abc from the set of models. So, we compute the intersection of our counterexample abc with the premise of the first implication, a. Well, and what we get is a, but if we replace a by a, nothing changes, so this won’t help us. Let's look at the second implication and compute the intersection of abc and cd. The intersection of abc and cd is c, and it'll be okay to replace cd by c. This would indeed exclude abc from the set of models. But first, we check if c is a model of L*, in other words, if c = L*(c), using a membership query. And in this case, the answer is yes, because {c}, as a set, doesn't violate any of these three implications. So, the answer is yes. And we don't want to lose c as a model, that's why we don't replace cd by c here. Instead, we add a new implication, abc —> abcd, and issue the equivalence query, the seventh equivalence query. And in this case, let's look at these implications. a —> ac, it's this one. cd —> acd. Well, it's this one, we don't have cd here, but the premise is always implied by itself. So, I could write cd here as well. And abc —> abcd. It's this implication. So, in this case, the oracle says yes. And we have successfully computed our set L*. [MUSIC]