The Rewrite Rules
11/17/06
Desiderata for rules in logical systems often pull in different directions. On the one hand, to prove meta-theorems about the logical system it is usually better to have a small number of fairly independent rules (but this will usually lengthen proofs in the system, proofs of the validity of arguments, for example). On the other, to prove theorems with the system or in the system it is usually better to have many rules, often with redundancies, (and this usually makes meta-theorems harder to prove).
Deriver tries to cater to both requirements. There is the plain vanilla system of Rules for Introducing and Removing Connectives. Then there is the Rule T which allows the introduction of any Theorem as a line of a proof. Thus, the first time you meet P∨∼P you can spend the seven lines that it takes to prove it; but the next time you meet the need to prove P∨∼P (perhaps as part of a longer proof), you can just use one line to assert P∨~P as a previously proved theorem. Finally there are the Rewrite Rules which can drastically shorten proofs.
Rewrite Rules allow the rewriting of a formula (or a subformula within a formula) into an equivalent but presumably more convenient form. Take for example, one of De Morgan's laws
∼(A∧B)≡(~A∨~B)
and one of its corresponding Rewrite Rules
∼(A∧B):-(∼A∨~B) ;
if you have proved, say, C∧∼(D∧E) and wish to prove C∧(~D∨~E) you can do so merely by rewriting the subformula ~(D∧E) to (~D∨~E).
As an argument in favour of the Rewrite Rules, consider the reduction of a complicated Predicate Calculus formula to Clausal Form where the resultant formula is to be Prenex Normal Form and the scope of the resultant formula is to be in Conjunctive Normal Form. This task is very important (and all students of Artificial Intelligence should know how to do it). It might take hundreds of lines if done by standard connective introduction and elimination; yet suitable Rewrite Rules will shorten the proof to about ten lines.
(Use of the Rewrite Rules is entirely optional: if you have some objection to them, don't use them.)
To invoke the Rules, select the formula under interest and click Rewrite Rules, this will open a Rewrite Panel containing the Rules and Instructions for their use. Basically, you select a subformula and a suitable Rule, this will display the tentative rewritten formula, if you are satisfied with this you click go and the line will be entered in the proof. (If what you select is ill-formed, or if the Rule does not apply, the program will beep and do nothing; for example, the Rule
~~P:-P
cannot be applied to the formula
A∧B
because the Rule removes double-negations and the formula A∧B is not a double-negation.)