Rules to convert logical expressions to CNF (Issue 152)

[gskorokhod]

Basic rules to simplify logical expressions (e.g. unwrap nested AND and nested OR, distribute NOT over an expression, etc)

See: #152

Depends on PR #83

[gskorokhod]

This is not ready to merge yet, just putting it out there :)

[gskorokhod]

One problem I've encountered so far is this:

This thread suggests using distributive laws:

1. (P⋁(Q⋀R))↔(P⋁Q)⋀(P⋁R)

2. (P⋀(Q⋁R))↔(P⋀Q)⋁(P⋀R)

However, these would cause a loop (see attached image)

Not sure what to do about this yet..

[ozgurakgun]

I like the look of these rules! We can talk about the looping behaviour.

[gskorokhod]

I think that's it in terms of rules actually!
(I have De Morgan's Law and one of the 2 distributive rules)

Might be better to wait for Kieran's PR to get merged, then rebase and test the rules before we merge though?