Mikito Harakiri wrote: > Jan Hidders wrote: > > I'm asking the question for a specific model, not in general as you > > did. For example, boolean algebra for boolean value *is* complete.
> According to Matt all that I have to do to prove incompleteness is to > find 2 nonisomorphic relational lattices with the same cardinality...
Mikito Harakiri wrote: > Mikito Harakiri wrote: > > Jan Hidders wrote: > > > I'm asking the question for a specific model, not in general as you > > > did. For example, boolean algebra for boolean value *is* complete.
> > According to Matt all that I have to do to prove incompleteness is to > > find 2 nonisomorphic relational lattices with the same cardinality...
That is under the assumption you are asking whether you are complete for all models of that cardinality. But here we only have *one* model, namely the (infinite) lattice over all relations as defined by the two operations. So, since there is only one, all the models you are considering are isomorphic.
Jan Hidders wrote: > That is under the assumption you are asking whether you are complete > for all models of that cardinality. But here we only have *one* model, > namely the (infinite) lattice over all relations as defined by the two > operations. So, since there is only one, all the models you are > considering are isomorphic.
> Sorry for asking such hard questions.
AFIR you mentioned long time ago that there is some kind of incompleteness result for RA. Do you have any reference? (Then it would be clear for me what kind of completeness you have in mind.)
Mikito Harakiri wrote: > Jan Hidders wrote: > > That is under the assumption you are asking whether you are complete > > for all models of that cardinality. But here we only have *one* model, > > namely the (infinite) lattice over all relations as defined by the two > > operations. So, since there is only one, all the models you are > > considering are isomorphic.
> > Sorry for asking such hard questions.
> AFIR you mentioned long time ago that there is some kind of > incompleteness result for RA. Do you have any reference? (Then it would > be clear for me what kind of completeness you have in mind.)
I'm not sure I said that, but there is a strongly related result about the undecidability of equivalence of two relational algebra expressions. But I suspect that is not going to help you much. I already gave an almost formal description of the problem in sci.math so I'm not sure what more there is to explain. I will elaborate that a bit:
We are talking about expressions as described by the following syntax (where R is assumed to be the set of relation variables):
E ::= R | (E /\ E) | (E \/ E)
We define a database as a tuple D = (S, f) where S is called the schema of D and a finite set of relation variables and f a function that maps each element in R to a relation. Clearly if an expression e contains only variables from S then it defines a query over D and its result is denoted as e(D).
Now we define two expressions e1 and e2 as query equivalent if (1) they contain the same set of relation variables, denoted as S, and (2) for every database D with schema S it holds that e1(D) = e2(D). We denote this fact as e1 =q= e2.
I think it is also clear that a set of algebraic identities of the form e1 == e2 defines an equivalence relationship over expressions as defined above by defining two expressions as equivalent iff we can rewrite one to the other with these identities. By rewriting I mean simply that if we apply e1 == e2 to e3 then we try to match e1 with a subexpression in e3 and replace it with e2 while replacing in e2 the variables with the subexpressions to wich they were mapped in e3 when matching e1. We denote this equivalence relation as e1 =a= e2.
We now call a set of algebraic identities *complete* if ifor all two expressions e1 and e2 that contain the same set of relation variables it holds that e1 =q= e2 iff e1 =a= e2.
If this holds then you can be sure that you have all the rewrite rules you need to do query optimization. That's why this is an interesting question. It would also establish that your set of operations is really interesting as it describes a large class of queries but allows to do something that is not possble for the full relational algebra.
Jan Hidders wrote: > Mikito Harakiri wrote: > > Jan Hidders wrote: > > > That is under the assumption you are asking whether you are complete > > > for all models of that cardinality. But here we only have *one* model, > > > namely the (infinite) lattice over all relations as defined by the two > > > operations. So, since there is only one, all the models you are > > > considering are isomorphic.
> > > Sorry for asking such hard questions.
> > AFIR you mentioned long time ago that there is some kind of > > incompleteness result for RA. Do you have any reference? (Then it would > > be clear for me what kind of completeness you have in mind.)
> I'm not sure I said that, but there is a strongly related result about > the undecidability of equivalence of two relational algebra > expressions. But I suspect that is not going to help you much. I > already gave an almost formal description of the problem in sci.math so > I'm not sure what more there is to explain. I will elaborate that a > bit:
> We are talking about expressions as described by the following syntax > (where R is assumed to be the set of relation variables):
> E ::= R | (E /\ E) | (E \/ E)
> We define a database as a tuple D = (S, f) where S is called the schema > of D and a finite set of relation variables and f a function that maps > each element in R to a relation. Clearly if an expression e contains > only variables from S then it defines a query over D and its result is > denoted as e(D).
> Now we define two expressions e1 and e2 as query equivalent if (1) they > contain the same set of relation variables, denoted as S, and (2) for > every database D with schema S it holds that e1(D) = e2(D). We denote > this fact as e1 =q= e2.
> I think it is also clear that a set of algebraic identities of the form > e1 == e2 defines an equivalence relationship over expressions as > defined above by defining two expressions as equivalent iff we can > rewrite one to the other with these identities. By rewriting I mean > simply that if we apply e1 == e2 to e3 then we try to match e1 with a > subexpression in e3 and replace it with e2 while replacing in e2 the > variables with the subexpressions to wich they were mapped in e3 when > matching e1. We denote this equivalence relation as e1 =a= e2.
> We now call a set of algebraic identities *complete* if ifor all two > expressions e1 and e2 that contain the same set of relation variables > it holds that e1 =q= e2 iff e1 =a= e2.
> If this holds then you can be sure that you have all the rewrite rules > you need to do query optimization. That's why this is an interesting > question. It would also establish that your set of operations is really > interesting as it describes a large class of queries but allows to do > something that is not possble for the full relational algebra.
> Does that clear some things up?
> -- Jan Hidders
I am still not entirely sure what 'completeness' you have in mind. Simplifying a bit, the relational calculus/algebra are a FOL dialect. As such, it is complete in the context of the Godel completeness theorem and trivially incomplete in the context of the Godel first incompleteness theorem, if treated as a theory with an empty axiom set. The 'completeness' terminology is unfortunate but that's life.
Now, using Codd's classification of what 'complete' means in the context of query languages, the RA/RC are 'complete' by Codd's definition (as far as I remember) as a standard agains which other query languages should be measured (despite the well-known facts about inexpressibility of certain questions).
Speaking of the OP question, is he trying to show that his query language is as expressive/'complete' as RA/RC, more expressive/'complete', or his question is about something completely different ?
What's confusing, to me at least, is that in another thread you said that the question was about complete theories, that is about completeness in the context of the first incompleteness theorem.
vc wrote: > Speaking of the OP question, is he trying to show that his query > language is as expressive/'complete' as RA/RC, more > expressive/'complete', or his question is about something completely > different ?
It's not clear who you assume the Delphi is. Jan asked about the completeness first. After the round of exchanges I once again think that speaking about completeness of axiom system is premature until we establish the axiom system in the first place
> I am still not entirely sure what 'completeness' you have in mind.
I gave a full formal definition of what I meant, so, just to be sure, did you understand this definition of completeness that I gave? Or is it that you don't see what it intuitively means?
Roughly, you can summarize it as saying that you have all the algebraic identities that hold, either directly, or indirectly in the sense that that they can be derived from the given list by applying them to each other.
> Simplifying a bit, the relational calculus/algebra are a FOL dialect. > As such, it is complete in the context of the Godel completeness > theorem and trivially incomplete in the context of the Godel first > incompleteness theorem, if treated as a theory with an empty axiom > set. The 'completeness' terminology is unfortunate but that's life.
Indeed.
> Now, using Codd's classification of what 'complete' means in the > context of query languages, the RA/RC are 'complete' by Codd's > definition (as far as I remember) as a standard agains which other > query languages should be measured (despite the well-known facts about > inexpressibility of certain questions).
Yes, but that is not the kind of completeness we are talking about here.
> Speaking of the OP question, is he trying to show that his query > language is as expressive/'complete' as RA/RC, more > expressive/'complete', or his question is about something completely > different ?
Since this was originally my question and the OP indicated that he not yet fully understands what I meant, I'm going to answer this for my question: it is about something completely different.
> What's confusing, to me at least, is that in another thread you said > that the question was about complete theories, that is about > completeness in the context of the first incompleteness theorem.
It is. Because we talking about a system where we have a semantical notion of truth for algebraic identities and a syntactical one (derivation from the set of given algebraic identies by applying them to each other) and the question is if these two are the same.
Jan Hidders wrote: > It is. Because we talking about a system where we have a semantical > notion of truth for algebraic identities and a syntactical one > (derivation from the set of given algebraic identies by applying them > to each other) and the question is if these two are the same.
What makes your question hard is that the idea of formal derivation of algebraic identities is not mature enough yet.
Consider the chain of rewritings for push-select-through-project on page 7. On step 8 the Spight criteria is applied. It's highly informal. We looked on the set of attributes of the each relation, check that they meet the condition, then apply the distributivity law. This step is highly informal. It has to be be broken down to a series of smaller steps which are simple applications of aximoatic equalities.
Next, consider the step #13 in push-cross-through-project rewritings on page 8. Informally, it is obvious that
`x` /\ B(z) = `xz`
(cross product of the empty relation `x` with the other relation is empty) but what axiom identity were appied on this step exactly?
Mikito Harakiri wrote: > vc wrote: > > Speaking of the OP question, is he trying to show that his query > > language is as expressive/'complete' as RA/RC, more > > expressive/'complete', or his question is about something completely > > different ?
> It's not clear who you assume the Delphi is. Jan asked about the > completeness first.
Which completeness did he ask about ?
>After the round of exchanges I once again think > that speaking about completeness of axiom system is premature until we > establish the axiom system in the first place
Mikito Harakiri wrote: > Next, consider the step #13 in push-cross-through-project rewritings on > page 8. Informally, it is obvious that
> `x` /\ B(z) = `xz`
> (cross product of the empty relation `x` with the other relation is > empty) > but what axiom identity were appied on this step exactly?
This step may indeed require some formal clarification, which might be helpful in identifying additional axiom identities. There is no complexity here from the RDBMS implementation perspective however. This is supposed to be a step in query optimization phase. Let me put query optimization into the bigger perspective of query evaluation, which consists of the two phases: static analysis (aka query compilation, aka query optimization) and dynamic execution. On step #13 the optimizer notices that there is a special identity that one of the relations in the expression `x` /\ B(z) meet
`x` /\ 00 = `x`
In this situation the optimizer is allowed to perform full evaluation of the expression `x` /\ B(z). (The general principle is that we can do full evaluation of static compilation phase if we guarantee that the dynamic execution of the query is fast). The query evaluation results in the empty relation `xz`.
> > I am still not entirely sure what 'completeness' you have in mind.
> I gave a full formal definition of what I meant, so, just to be sure, > did you understand this definition of completeness that I gave? Or is > it that you don't see what it intuitively means?
No, I was not sure what kind of completeness we were talking about since the word is abused so much. Intuitive meaning would be helpful for sure.
> Roughly, you can summarize it as saying that you have all the algebraic > identities that hold, either directly, or indirectly in the sense that > that they can be derived from the given list by applying them to each > other.
OK.
[...]
> the RA/RC are 'complete' by Codd's > > definition (as far as I remember) as a standard agains which other > > query languages should be measured (despite the well-known facts about > > inexpressibility of certain questions).
> Yes, but that is not the kind of completeness we are talking about > here.
OK.
> > Speaking of the OP question, is he trying to show that his query > > language is as expressive/'complete' as RA/RC, more > > expressive/'complete', or his question is about something completely > > different ?
> Since this was originally my question
I apologize for the misattribution.
> and the OP indicated that he not > yet fully understands what I meant, I'm going to answer this for my > question: it is about something completely different.
> > What's confusing, to me at least, is that in another thread you said > > that the question was about complete theories, that is about > > completeness in the context of the first incompleteness theorem.
> It is. Because we talking about a system where we have a semantical > notion of truth for algebraic identities and a syntactical one > (derivation from the set of given algebraic identies by applying them > to each other) and the question is if these two are the same.
They would be the same for a complete (in the sense of the first incompletenes theorem) system so finding out whether this is the case would amount to showing if the system in question is complete or not. However, I am not sure why that may be practically important. Arithmetic incompleteness does not prevent anyone from balancing one's checkbook.
vc wrote: > Arithmetic incompleteness does not prevent anyone from balancing one's > checkbook.
I'll add that before arithmetics axiomatization questions were asked, there was a wealth of results in different direction. Negative, rational, algebraic, real and complex were discovered -- these are several centuries of accumulated results, as opposed to metamathematics which is only a century old. How about "extraordinary relations"?
Mikito Harakiri wrote: > vc wrote: > > Arithmetic incompleteness does not prevent anyone from balancing one's > > checkbook.
> I'll add that before arithmetics axiomatization questions were asked, > there was a wealth of results in different direction. Negative, > rational, algebraic, real and complex were discovered -- these are > several centuries of accumulated results, as opposed to metamathematics > which is only a century old.
Tarski relation algebra appears not to have the union operator. Perhaps this may explain why the emphasis is on the relational division and "rational" aka "extraordinary" relations. One part which seems obviously missing is the introduction of negative relations. The equation with union operator
P \/ X = Q
has solutions only if P <= Q. Unlike equations in integers there has to be a second equation that would guarantee uniqueness of the solution
> Tarski relation algebra appears not to have the union operator. Perhaps > this may explain why the emphasis is on the relational division and > "rational" aka "extraordinary" relations. One part which seems > obviously missing is the introduction of negative relations. The > equation with union operator
> P \/ X = Q
> has solutions only if P <= Q. Unlike equations in integers there has to > be a second equation that would guarantee uniqueness of the solution
Mikito Harakiri wrote: > Jan Hidders wrote: > > It is. Because we talking about a system where we have a semantical > > notion of truth for algebraic identities and a syntactical one > > (derivation from the set of given algebraic identies by applying them > > to each other) and the question is if these two are the same.
> What makes your question hard is that the idea of formal derivation of > algebraic identities is not mature enough yet.
I gave a nearly formal definition of what I meant with that term. I don't see how it can get more mature.
> Consider the chain of rewritings for push-select-through-project on > page 7. On step 8 the Spight criteria is applied.
For the fragment that I asked about (look at the definition expression) the Spight rule is irrelevant.
> > > What's confusing, to me at least, is that in another thread you said > > > that the question was about complete theories, that is about > > > completeness in the context of the first incompleteness theorem.
> > It is. Because we talking about a system where we have a semantical > > notion of truth for algebraic identities and a syntactical one > > (derivation from the set of given algebraic identies by applying them > > to each other) and the question is if these two are the same.
> They would be the same for a complete (in the sense of the first > incompletenes theorem) system so finding out whether this is the case > would amount to showing if the system in question is complete or not.
Not necessarily because the syntactical notion of truth is not the usual one. It's related but not the same.
> However, I am not sure why that may be practically important. > Arithmetic incompleteness does not prevent anyone from balancing one's > checkbook.
Having a full and simple axiomatization makes it possible to write query optimizers that do a more thorough search of the "optimization space", and if you know you are complete then you are sure that you need not look further for any other rules.
Jan Hidders wrote: > vc wrote: > > Jan Hidders wrote: > > > vc wrote:
> > > > What's confusing, to me at least, is that in another thread you said > > > > that the question was about complete theories, that is about > > > > completeness in the context of the first incompleteness theorem.
> > > It is. Because we talking about a system where we have a semantical > > > notion of truth for algebraic identities and a syntactical one > > > (derivation from the set of given algebraic identies by applying them > > > to each other) and the question is if these two are the same.
> > They would be the same for a complete (in the sense of the first > > incompletenes theorem) system so finding out whether this is the case > > would amount to showing if the system in question is complete or not.
> Not necessarily because the syntactical notion of truth is not the > usual one. It's related but not the same.
I let it slip the first time because I thought you'd used the expression metaphorically, but now I am curious as to what exactly you meant. The 1st incompleteness theorem talks about provability, not truth. The notion of truth is not used in either the formulation or proof.
Let's assume that by 'syntactical notion of truth; you've meant in fact derivation. If so, what did you mean by " because the syntactical notion of truth is not the usual one. It's related but not the same" ?
> > However, I am not sure why that may be practically important. > > Arithmetic incompleteness does not prevent anyone from balancing one's > > checkbook.
> Having a full and simple axiomatization makes it possible to write > query optimizers that do a more thorough search of the "optimization > space", and if you know you are complete then you are sure that you > need not look further for any other rules.
If you have a bunch of axioms/derivation rules, you can transform an expression to your heart content regardless of whether the theory is complete or not. It's highly unlikely that you will all of a sudden come up with a formula which turns out to be unprovable in your hypothetical incomplete theory -- such formula is underivable from the theory axioms (unless the formula somehow magically appears in your mind). So I am puzzled by your thinking that a theory completeness in the sense of the 1st incompletness theorem may have any practical implications for the query language.
> > > > > What's confusing, to me at least, is that in another thread you said > > > > > that the question was about complete theories, that is about > > > > > completeness in the context of the first incompleteness theorem.
> > > > It is. Because we talking about a system where we have a semantical > > > > notion of truth for algebraic identities and a syntactical one > > > > (derivation from the set of given algebraic identies by applying them > > > > to each other) and the question is if these two are the same.
> > > They would be the same for a complete (in the sense of the first > > > incompletenes theorem) system so finding out whether this is the case > > > would amount to showing if the system in question is complete or not.
> > Not necessarily because the syntactical notion of truth is not the > > usual one. It's related but not the same.
> I let it slip the first time because I thought you'd used the > expression metaphorically, but now I am curious as to what exactly you > meant. The 1st incompleteness theorem talks about provability, not > truth. The notion of truth is not used in either the formulation or > proof.
It also doesn't mention completeness, so I thought you meant the notion of completeness that it is usually assumed to say something about. But this is all detracting form the main point. I gave an exact and, I think, very simple definition in:
> Let's assume that by 'syntactical notion of truth; you've meant in fact > derivation. If so, what did you mean by " because the syntactical > notion of truth is not the usual one. It's related but not the same" ?
We have different derivation rules.
> > Having a full and simple axiomatization makes it possible to write > > query optimizers that do a more thorough search of the "optimization > > space", and if you know you are complete then you are sure that you > > need not look further for any other rules.
> If you have a bunch of axioms/derivation rules, you can transform an > expression to your heart content regardless of whether the theory is > complete or not.
But you are not sure that you can find all possible query evaluation plans, so you migh miss an optimization opportunity.
> > > Having a full and simple axiomatization makes it possible to write > > > query optimizers that do a more thorough search of the "optimization > > > space", and if you know you are complete then you are sure that you > > > need not look further for any other rules.
> > If you have a bunch of axioms/derivation rules, you can transform an > > expression to your heart content regardless of whether the theory is > > complete or not.
> But you are not sure that you can find all possible query evaluation > plans, so you migh miss an optimization opportunity.
The set of transformation rules ('algebraic identities') defines the optimization space also called 'algebraic space' which is enormous in a general case even with reltive simple queries. None of the existing relational database optimizers traverses the entire algebraic space because of the combinatorial explosion and therefore none is capable of producing an otimal query, only a good enough one. Various heuristics are used in order to prune the algebraic space and manual query rewriting and tuning is a fact of life.
In light of the above, the axiom completenes issue is really a non-issue.
> > > > Having a full and simple axiomatization makes it possible to write > > > > query optimizers that do a more thorough search of the "optimization > > > > space", and if you know you are complete then you are sure that you > > > > need not look further for any other rules.
> > > If you have a bunch of axioms/derivation rules, you can transform an > > > expression to your heart content regardless of whether the theory is > > > complete or not.
> > But you are not sure that you can find all possible query evaluation > > plans, so you migh miss an optimization opportunity.
> The set of transformation rules ('algebraic identities') defines the > optimization space also called 'algebraic space' which is enormous in a > general case even with reltive simple queries. None of the existing > relational database optimizers traverses the entire algebraic space > because of the combinatorial explosion and therefore none is capable of > producing an otimal query, only a good enough one. Various heuristics > are used in order to prune the algebraic space and manual query > rewriting and tuning is a fact of life.
Of course.
> In light of the above, the axiom completenes issue is really a > non-issue.
That conclusion is far too hasty. If you have a better grasp on what the total optimization-landscape is and looks like you might possibly be able to come up with better heuristics. Moreover, we are looking here at a small subset of the queries that can be expressed with relational algebra, and an algebra that is in some respects more "algebra friendly" so things might be simpeler here. In some sense that is the whole raison d'etre of Vadim's algebra, so such a result would seriously strengthen his case. Until we have actually looked, it is simply too early to tell. Finally, trying to prove completeness is simply a good way of checking if there are no obvious algebraic identities still missing.
Jan Hidders wrote: > Finally, trying to prove completeness is > simply a good way of checking if there are no obvious algebraic > identities still missing.
It seems a very interesting question. But I haven't been able to come up with an idea of how to approach it. I was thinking I'd try to understand some simpler cases first. For example, one can construct every possible boolean function with only NAND (or NOR), but the only proof of this I'm aware of is simply one by demonstration. There are only 16 possible boolean functions, so it's quite to simply build them all with NAND and there's your proof.
So, how would one go about proving that any boolean expression with the grammar
E :== v | E && E | E || E
could be transformed into any equivalent expression, using only some fixed set of transformations. (That is the basic idea, right?) What is the smallest set of transformations necessary?
Any pointers to further reading appreciated; I'm completely uninformed on this topic.
> So, how would one go about proving that any boolean expression > with the grammar
> E ::= V > | E && E > | E || E
> could be transformed into any equivalent expression, using only > some fixed set of transformations. (That is the basic idea, > right?) What is the smallest set of transformations necessary?
Often it is shown that you can use the rewrite rules to rewrite the expression to some normal form and then it is shown that for this normal form it holds that expressions are sementically equivalent iff they are syntactically equivalent. I'll give the example for the boolean case you presented.
You need to show that if you have two equivalent expressions you can rewrite one to the other. What is often a good idea for showing equivalence is to rewrite them to some normal form. For the disjunctive normal form you need:
Which essentially means that we can view the expression as a set of sets of variables, e.g., (v1 || (v2 && v3)) || ((v2 && v4) && v5) can be thought of as { {v1}, {v2, v3}, {v2, v4, v5} }. I will call this a set representation of a DNF expression.
Note that we can now also drop rule (1') because it follows from (1), (4) and (5).
If we add the following rule
(8) (v1 && v2) || v2 == v1 && v2
then we can always rewrite to a DNF such that it holds for its set version {C1, ..., Cn} that there are no Ci and Cj such that Ci is a subset of Cj. I will call set-representations with that property subset-free.
We now set out to show that if two expressions e1 and e2 are rewritten to DNF expressions with subset-free set-representions s1 and s2, respectively, and e1 and e2 are semantically equivalent then s1 = s2. We proof this by contradiction:
We begin with assuming that two expressions e1 and e2 are rewritten to DNF expressions with subset-free set-representations s1 and s2, respectively, and e1 and e2 are semantically equivalent. Let us now also assume that s1 <> s2. Let s1 = {B1, ..., Bn} and s2 = {C1, ..., Cm}. Now there is some Bi that is not a superset of any of C1, ..., Cm or there is a Cj that is not a superset of any of B1, ..., Bn. Note that this is true because s1 and s2 are different, finite and subset-free. (Proof of that is left to the reader as an exercise.) Let us assume that such a Bi exists. (The case for Cj is symmetric.) Let M(Bi) be the model that assigns all variables in Bi to TRUE and all other variables to FALSE. Then clearly M(B_i) is a model for which e1 evaluates to TRUE, but e2 evaluates to FALSE, since none of C1, ..., Cm is a subset of Bi. It follows that e1 and e2 are semantically different, which contradicts the assumption that e1 and e2 are semantically equivalent.
So we know that if two expressions e1 and e2 are semantically equivalent then there is a a subset-free set-representation s' such that both e1 and e2 can be rewritten to e1' and e2' with s' as their set-version. Clearly since e1' and e2' have the same set-representation they can be rewritten to each other, and so we can rewrite e1 to e1' to e2' to e2.
QED
So the conclusion is that the set of rules (1), ..., (8) are indeed complete in the sense that we talked about. Note that the dual of (1), i.e.,
(v1 && v2) || v3 == (v1 || v3) && (v2 || v3)
is missing but that indeed we can prove it from the other rules by algebraic rewriting. That's also left to the reader as an exercise. :-)
> > So, how would one go about proving that any boolean expression > > with the grammar
> > E ::= V > > | E && E > > | E || E
> > could be transformed into any equivalent expression, using only > > some fixed set of transformations. (That is the basic idea, > > right?) What is the smallest set of transformations necessary?
> Often it is shown that you can use the rewrite rules to rewrite the > expression to some normal form and then it is shown that for this > normal form it holds that expressions are sementically equivalent iff > they are syntactically equivalent. I'll give the example for the > boolean case you presented.
> You need to show that if you have two equivalent expressions you can > rewrite one to the other. What is often a good idea for showing > equivalence is to rewrite them to some normal form. For the disjunctive > normal form you need:
> Which essentially means that we can view the expression as a set of > sets of variables, e.g., (v1 || (v2 && v3)) || ((v2 && v4) && v5) can > be thought of as { {v1}, {v2, v3}, {v2, v4, v5} }. I will call this a > set representation of a DNF expression.
> Note that we can now also drop rule (1') because it follows from (1), > (4) and (5).
