People have been asking me about what starting inferences you can use in natural deduction proofs. Besides things in the knowledge base, one that I forget to mention that you can include is @BT@neg A or A@BT@ (excluded middle). I've adjusted my slide on propositional natural deduction proofs now to mention this. I've also added to the end of the Nov 6 slides, some remarks on how equality can be handled in first-order natural deduction and in first order resolution proofs. Best, Chris