# Rules of Inference

Standard rules:

* [Implication introduction](logic-inference/implication-introduction)
* [Implication elimination](logic-inference/implication-elimination)
* [Conjunction introduction](logic-inference/conjunction-introduction)
* [Conjunction elimination](logic-inference/conjunction-elimination)
* [Disjunction introduction](logic-inference/disjunction-introduction)
* [Disjunction elimination](logic-inference/disjunction-elimination)
* [Universal generalization](https://github.com/mandober/debrief.math/tree/1303f9c4d1763e93618e71cea4b00554bb65a514/300-logic/logic-inference/universal-generalization/README.md)
* [Universal instantiation](https://github.com/mandober/debrief.math/tree/1303f9c4d1763e93618e71cea4b00554bb65a514/300-logic/logic-inference/universal-instantiation/README.md)
* [Existential generalization](https://github.com/mandober/debrief.math/tree/1303f9c4d1763e93618e71cea4b00554bb65a514/300-logic/logic-inference/existential-generalization/README.md)
* [Existential instantiation](https://github.com/mandober/debrief.math/tree/1303f9c4d1763e93618e71cea4b00554bb65a514/300-logic/logic-inference/existential-instantiation/README.md)

Classical (more)

* [Exportation](logic-inference/exportation)
* [Negation introduction](https://github.com/mandober/debrief.math/tree/1303f9c4d1763e93618e71cea4b00554bb65a514/300-logic/logic-inference/negation-introduction.md)
* [Negation elimination](https://github.com/mandober/debrief.math/tree/1303f9c4d1763e93618e71cea4b00554bb65a514/300-logic/logic-inference/negation-elimination.md)
* [Disjunctive syllogism](logic-inference/disjunctive-syllogism)

List

* [Assumption](https://github.com/mandober/debrief.math/tree/1303f9c4d1763e93618e71cea4b00554bb65a514/300-logic/logic-inference/assumption.md)
* Conjunction
  * and-introduction
  * and-elimination (conjunction elimination, simplification)
* Disjunction
  * disjunction introduction
  * disjunction elimination
* Implication
  * implication introduction, conditional proof
  * implication elimination (modus ponens)
* Biconditional
  * biconditional introduction
  * biconditional elimination
* Negation
  * negation introduction
  * negation elimination
* Double negation
  * double negation introduction
  * double negation elimination

## Pile of terms

* Transformation rules
* Rules of inference
* Propositional calculus
  * Implication introduction / elimination (modus ponens)
  * Biconditional introduction / elimination
  * Conjunction introduction / elimination
  * Disjunction introduction / elimination
  * Disjunctive / hypothetical syllogism
  * Constructive / destructive dilemma
  * Absorption / modus tollens / modus ponendo tollens
  * Rules of replacement
  * Associativity
  * Commutativity
  * Distributivity
  * Double negation
  * De Morgan's laws
  * Transposition
  * Material implication
  * Exportation
  * Tautology
  * Negation introduction
* Predicate logic
  * Universal generalization / instantiation
  * Existential generalization / instantiation
