Catalogue of propositional logic laws I have searched for it in Wikipedia and this site and I haven't found it yet. What I have found isn't complete enough -maybe a short list of ten or so equivalence laws, perhaps forgetting all together laws related to other connectors different from the disjunction or conjunction. I am interested in all logic laws, inference rules too and in general all relevant tautologies which I can use in my deductions in the framework of propositional logic.
I'm looking for an organised, logical and neat catalogue of derivation rules. Biconditional tautologies or equivalence laws, conditional tautologies or inference rules, maybe the law of excluded middle should have a special place in this assortment since it is a disjunction tautology, and the law of non contradiction because it is a negation tautology, I'm not sure. Another criteria which can be taken into account to put order in the catalogue could be the number of propositions to which the logic law is applied. For example, the double negation law is only applied to one proposition but Modus Ponens to two of them.
Could anybody point me to a good resource where I can find this kind of list? My textbook has got a list of this kind with about 40 or so of these laws but I would like a different resource to check it and improve it before memorising it. I don't trust it that much!
 A: Laws of Logic (Biconditional Tautologies)
Law of Double Negation or Negation Elimination $$ \lnot(\lnot p) \equiv p $$ DeMorgan's Laws $$ \lnot (p \land q) \equiv (\lnot p) \lor (\lnot q) $$ $$ \lnot (p \lor q) \equiv (\lnot p) \land (\lnot q) $$ Commutative Laws for Conjunction, Disjunction and Biconditional $$ p \land q \equiv q \land p $$ $$ p \lor q \equiv q \lor p $$ $$ p \leftrightarrow q \equiv q \leftrightarrow p $$ Associative Laws for Conjunction, Disjunction and Bicondional $$ (p \land q) \land r \equiv p \land (q \land r) $$ $$ (p \lor q) \lor r \equiv p \lor (q \lor r) $$ $$ (p \leftrightarrow q) \leftrightarrow r \equiv p \leftrightarrow (q \leftrightarrow r) $$ Distributive Laws $$ p \lor (q \land r) \equiv (p \lor q) \land (p \lor r)$$ $$ p \land (q \lor r) \equiv (p \land q) \lor (p \land r)$$ $$ p \rightarrow (q \land r) \equiv (p \rightarrow q) \land (p \rightarrow r)$$ $$ p \rightarrow (q \lor r) \equiv (p \rightarrow q) \lor (p \rightarrow r)$$ Idempotent Laws $$ p \lor p \equiv p$$ $$ p \land p \equiv p$$ Identity Laws $$ p \lor F \equiv p $$ $$ p \land T \equiv p $$ $$ T \rightarrow p \equiv p$$ Inverse Laws $$ p \lor (\lnot p) \equiv T$$ $$ p \land (\lnot p) \equiv F$$ Domination Laws $$ p \lor T \equiv T$$ $$ p \land F \equiv F$$ Absortion Laws $$ p \lor (p \land q) \equiv p $$ $$ p \land (p \lor q) \equiv p $$ The "Switcheroo" Law$^{(2)}$ $$ p \rightarrow q \equiv (\lnot p) \lor q $$ Equivalence of the Contrapositive of a Conditional Statement $$ p \rightarrow q \equiv (\lnot q) \rightarrow (\lnot p)$$ Meaning of Biconditional $$ p \leftrightarrow q \equiv (p \rightarrow q) \land (q \rightarrow p)$$ Iteration Rule$^{ (3)} $ $$ p \equiv p $$ Conditional Expansion Laws$^{ (4)} $ $$ p \rightarrow q \equiv p \leftrightarrow (p \land q)$$ $$ p \rightarrow q \equiv q \leftrightarrow (p \lor q)$$
Rules of Inference (Conditional Tautologies)
Rule of Detachment (Modus Ponens) (Elimination of conditional) (Direct Reasoning) $$ (p \rightarrow q) \land p \vDash q$$ Law of Syllogism or Transitivity $$ ( p \rightarrow q) \land (q \rightarrow r) \vDash p \rightarrow r $$ Modus Tollens (Indirect Reasoning) $$ (p \rightarrow q) \land (\lnot q) \vDash \lnot p $$ Rule of Conjunction Introduction $$ (p) \land (q) \vDash p \land q $$ Rule of Disjunctive Syllogism $$ (p \lor q) \land (\lnot p) \vDash q$$ Rule of Contradiction or Negation Introduction $$ (\lnot p) \rightarrow F \vDash p$$ Rule of Simplification or Conjunction Elimination $$ p \land q \vDash p$$ Rule of Addition or Disjunctive Amplification/Introduction $$ p \vDash p \lor q$$ Rule of Conditional Proof $$ (p \land q) \land [p \rightarrow (q \rightarrow r)] \vDash r $$ Rule for Proof by Cases or Disjunction Elimination $$ (p \lor q) \land (p \rightarrow r) \land (q \rightarrow r) \vDash r$$ Rule of the Constructive Dilemma $$ (p \lor r) \land (p \rightarrow q) \land (r \rightarrow s) \vDash q \lor s $$ Rule of Destructive Dilemma $$ (p \rightarrow q) \land (r \rightarrow s) \land ((\lnot q) \lor (\lnot s)) \vDash (\lnot p) \lor (\lnot r) $$ Resolution Law$^{ (4)} $ $$ ((\lnot p) \lor q) \land (p \lor r) \vDash q \lor r$$ Sylogism Law$^{ (4)} $ $$ p \rightarrow q \vDash (q \rightarrow r) \rightarrow (p \rightarrow r)$$ NOTE: Main source by (1)Grimaldi, Ralph P., “Discrete and Combinatorial Mathematics”, 4th ed (I will be modifying and improving it the following days with additional sources). Other sources: (2)Waner S. and Costenoble S.R., Finite Mathematics, 2nd ed (3)Clemente Laboreo D., Introduction to Natural Deduction, 2005 (4)Delgado Pineda, M & Muñoz Bouzo, MJ, Lenguage Matemátio, Conjuntos y Números, 2nd ed, 2015
A: There is no such complete catalogue of all propositional logic lawd and inference rules, and there can't exist such a catalogue either.
There exist infinitely many tautologies which are not substitution instances of other tautologies.  Each such tautology consists of a logical law.  There also exists infinitely many tautologies which only have conditional symbols, have more than one conditional symbol, and variable symbols which are not substitution instances of other tautologies.  Each of those corresponds to more than one derivable inference rule, because of the nature of modus ponens.
A: You might want to check:
193 propositional logic test cases from Principia
https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-principia-pl
They can be proved by various methods:
Prolog Tautology Checking, who does it better?
https://qiita.com/j4n_bur53/items/28d667cf3412fa950bc7
