Lab 3 assessment about uvasoftwaretesting15 HOT 7 CLOSED

Could you give us an example where the CNF fails?

from uvasoftwaretesting15.

I also take issue with point nr 3. If you look at wikipedia then it says:

"In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of clauses, where a clause is a disjunction of literals; otherwise put, it is an AND of ORs"

We even discussed the fact that a tautology could result in an empty conjunction with Bert Lisser and he said that an empty conjunction was perfectly valid. Therefore a conjunction or disjunction of one term also seems valid to me.

from uvasoftwaretesting15.

@jovanovski toCnf (Prop 1)

@mwijngaard empty conjunctions and disjunctions are somewhat awkward but valid encodings for true and false. There is no excuse for one-element conjunctions and disjunctions. How would you write them down?

from uvasoftwaretesting15.

How would you write an empty conjunction? They only make sense in a context
of computerised processing of formulas, and in that context a conjunction
of one term makes just as much sense. The fact is that we use these
specific datatypes for representing formulas and not standard mathematical
notation. Even the lecture notes directly mention that cnf form is
generally used in computer solvers. These solvers must internally work with
conjunctions of one term instead of a normalized version, since it's a more
general format, fit for computerised processing, and it doesn't make sense
to make the solver logic more complex just because we want it to be able to
be written down in standard mathematical notation.

And btw, the show function is perfectly capable of writing them down, just
not in standard mathematical notation :-).

@jovanovski https://github.com/jovanovski toCnf (Prop 1)

@mwijngaard https://github.com/mwijngaard empty conjunctions and
disjunctions are somewhat awkward but valid encodings for true and false.
There is no excuse for one-element conjunctions and disjunctions. How would
you write them down?

—
Reply to this email directly or view it on GitHub
#3 (comment)
.

from uvasoftwaretesting15.

You write an empty conjunction down as ⊤ and an empty disjunction as ⊥. This is why I said that they are encodings of the top and bottom elements.

And btw, the show function is perfectly capable of writing them down, just not in standard mathematical notation :-).

Just as I could have given you feedback faster in Russian — but after some consideration chose not to ;)

from uvasoftwaretesting15.

from uvasoftwaretesting15.

This is not a point reduction, you get full points — but no bonus point.

Please feel free to take it up to Jan: he has the last word, and if he looks at the code and deems it worthy of a bonus, so be it.

from uvasoftwaretesting15.