Deduction systems for propositional logic ready to use with LogicUS.PL.Deduction, as text that can be edited:
rules can be removed, renamed or added before reading it with readSystem.
The systems of this module. LogicUS.FOL.DeductionSystems has their first-order versions, with the same names.
The system of a preset, by name.
Classical natural deduction: the intuitionistic and the classical rules.
The rules of natural deduction for the connectives that hold intuitionistically (introduction and elimination of ∧, ∨, →, ↔, ¬ and ⊥), and reiteration.
The classical rules: elimination of the double negation and reduction to the absurd.
Rules that can be derived from the others, for exercises that allow them: modus tollens, disjunctive and hypothetical syllogisms, introduction of the double negation, excluded middle and De Morgan laws.
An axiomatic system (Łukasiewicz): three axiom schemes and modus ponens.
A system with a name and a short description.