Add the ability to annotate resolutions with a rule.

[McTano]

Graham's notes on the algorithm for checking a tree presuppose that a resolved node is marked with the rule that resolves it.

We should do this in a way that is agnostic to the particular abbreviations/names for rules in the current logic, but it may be worth cross-referencing this with the forall x textbook to make sure we're on the right track.

[drgilbert]

I think this is right. In general (there are exceptions to this that probably aren't worth worrying about too much), there will always be two rules per connective/operator/quantifier: a negated rule and a non-negated rule. So, for conjunction there will be a \land rule and a \neg \land rule. The obvious exception to this is the double negation elimination rule, which has no partner.

As a starting point, we can just use this as our naming convention. Something like: conj and neg-conj, for example.

[McTano]

This has been implemented, up to allowing the user to enter a rule. At this point, we're not doing anything to validate the rule that the user types in, but I think if we're going to check against a list of rules, the list should be passed from Carnap.