Testing

7/30/26

You can try some of the testing

The PLI rules have been tested and should be working.

The PME rules also should be working.

Testing the PME rules.

[When there is a suitable match, a rewrite rule can rewrite an entire formula or a subformula of a formula. This opens the way to a short cut when testing manually. For example, the entire formula P∨(Q.R) ≡(P∨Q).(P∨R) cannot be rewritten by a Dist rule p∨(q.r) :: (p∨q).(p∨r) but the left subformula of it can be rewritten to (P∨Q).(P∨R) ≡(P∨Q).(P∨R), alternatively the right subformula can be rewritten to P∨(Q.R) ≡P∨(Q.R). Checking that both these rewrites goes through gives an assurance that this Dist rule is working (left-to-right and right-to-left). This technique has little or no educational value. But it does speed up manual testing.]