Definition:Natural Deduction/Technical Note
Jump to navigation
Jump to search
Technical Note on Natural Deduction
In order to make the use of the proof rules of natural deduction in a tableau proof on $\mathsf{Pr} \infty \mathsf{fWiki}$, the following templates have been developed:
For convenience, other templates are also available, for the following derived rules:
Template:Commutation | to invoke | the Rule of Commutation | |||||||
Template:DeMorgan | to invoke | an instance of De Morgan's Laws | |||||||
Template:Idempotence | to invoke | the Rule of Idempotence | |||||||
Template:IdentityLaw | to invoke | the Law of Identity |
For the other general proof rules, there exist the following templates:
Template:SequentIntro | to invoke | the Rule of Sequent Introduction | |||||||
Template:TheoremIntro | to invoke | the Rule of Theorem Introduction | |||||||
Template:Substitution | to invoke | the Rule of Substitution |